{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":1743368,"defaultBranch":"master","name":"math-classes","ownerLogin":"coq-community","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2011-05-13T13:18:32.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/34452610?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1713876910.0","currentOid":""},"activityList":{"items":[{"before":"7b7e3a0320eef1c024eb9088ffe7f0bd1eb60f5f","after":null,"ref":"refs/heads/coq_18880","pushedAt":"2024-04-11T13:10:37.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"}},{"before":"17b7a3178ef14ce2e9f767d227b386aaf530c55b","after":"2a8e12360cceee510f39e3ef4d0a7472d70fa684","ref":"refs/heads/master","pushedAt":"2024-04-11T13:10:33.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Merge pull request #127 from coq-community/coq_18880\n\nAdapt to https://github.com/coq/coq/pull/18880","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2237673606\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq-community/math-classes/issues/127\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq-community/math-classes/pull/127/hovercard\" href=\"https://github.com/coq-community/math-classes/pull/127\">#127</a> from coq-community/coq_18880"}},{"before":null,"after":"7b7e3a0320eef1c024eb9088ffe7f0bd1eb60f5f","ref":"refs/heads/coq_18880","pushedAt":"2024-04-11T12:59:39.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Adapt to https://github.com/coq/coq/pull/18880","shortMessageHtmlLink":"Adapt to <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2220462199\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18880\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18880/hovercard\" href=\"https://github.com/coq/coq/pull/18880\">coq/coq#18880</a>"}},{"before":"278a15ada865ccabfe0e190f3ef7a6b3b805b95c","after":"17b7a3178ef14ce2e9f767d227b386aaf530c55b","ref":"refs/heads/master","pushedAt":"2024-04-07T19:22:37.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"spitters","name":"Bas Spitters","path":"/spitters","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/210638?s=80&v=4"},"commit":{"message":"Merge pull request #126 from ppedrot/rm-hint-constr\n\nRemove the few instances of non-global hint declarations.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2229740052\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq-community/math-classes/issues/126\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq-community/math-classes/pull/126/hovercard\" href=\"https://github.com/coq-community/math-classes/pull/126\">#126</a> from ppedrot/rm-hint-constr"}},{"before":"b295176134cd220714bd894d583cf5d594f871d6","after":null,"ref":"refs/heads/coq_18590","pushedAt":"2024-02-01T12:51:14.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"}},{"before":"f9712ba67b59c90446522e102c87200c7da756ec","after":"278a15ada865ccabfe0e190f3ef7a6b3b805b95c","ref":"refs/heads/master","pushedAt":"2024-02-01T10:26:50.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Merge pull request #123 from coq-community/coq_18590\n\nAdapt to https://github.com/coq/coq/pull/18590","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2110241517\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq-community/math-classes/issues/123\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq-community/math-classes/pull/123/hovercard\" href=\"https://github.com/coq-community/math-classes/pull/123\">#123</a> from coq-community/coq_18590"}},{"before":"1cac8961a3d55dda3e44d753711e6e932eb33514","after":"b295176134cd220714bd894d583cf5d594f871d6","ref":"refs/heads/coq_18590","pushedAt":"2024-01-31T14:36:36.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Adapt to https://github.com/coq/coq/pull/18590","shortMessageHtmlLink":"Adapt to <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2108207360\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18590\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18590/hovercard\" href=\"https://github.com/coq/coq/pull/18590\">coq/coq#18590</a>"}},{"before":null,"after":"1cac8961a3d55dda3e44d753711e6e932eb33514","ref":"refs/heads/coq_18590","pushedAt":"2024-01-31T14:33:26.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Adapt to https://github.com/coq/coq/pull/18590","shortMessageHtmlLink":"Adapt to <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2108207360\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18590\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18590/hovercard\" href=\"https://github.com/coq/coq/pull/18590\">coq/coq#18590</a>"}},{"before":"6ad1db9fbd646f8daf1568afef230a76a9f58643","after":"f9712ba67b59c90446522e102c87200c7da756ec","ref":"refs/heads/master","pushedAt":"2023-11-06T19:46:13.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"spitters","name":"Bas Spitters","path":"/spitters","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/210638?s=80&v=4"},"commit":{"message":"Merge pull request #122 from herbelin/master+adapting-coq-pr17832-choice-stronger-precedence-rewstrategy\n\nAdapt to Coq PR #17832: syntax of choice in rewstrategy expects arguments at atomic level","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1977210017\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq-community/math-classes/issues/122\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq-community/math-classes/pull/122/hovercard\" href=\"https://github.com/coq-community/math-classes/pull/122\">#122</a> from herbelin/master+adapting-coq-pr17832-cho…"}},{"before":"83822dea52b674051d58a9056e3ccc3c1e26e708","after":"6ad1db9fbd646f8daf1568afef230a76a9f58643","ref":"refs/heads/master","pushedAt":"2023-10-16T11:27:48.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"spitters","name":"Bas Spitters","path":"/spitters","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/210638?s=80&v=4"},"commit":{"message":"Merge pull request #50 from tymmym/master\n\nAdd Module instance for polynomials","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"312982275\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq-community/math-classes/issues/50\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq-community/math-classes/pull/50/hovercard\" href=\"https://github.com/coq-community/math-classes/pull/50\">#50</a> from tymmym/master"}},{"before":"fbb6ebe5aee8f17cc526a0afffb766c8afeb87e2","after":"83822dea52b674051d58a9056e3ccc3c1e26e708","ref":"refs/heads/master","pushedAt":"2023-10-16T11:26:52.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"spitters","name":"Bas Spitters","path":"/spitters","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/210638?s=80&v=4"},"commit":{"message":"Merge pull request #78 from JasonGross/fix-for-more-rapply-10760\n\nFix for a new rapply tactic","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"494852030\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq-community/math-classes/issues/78\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq-community/math-classes/pull/78/hovercard\" href=\"https://github.com/coq-community/math-classes/pull/78\">#78</a> from JasonGross/fix-for-more-rapply-10760"}},{"before":"aaaf68fca837effde7d2a7f17b3e52455fadd08a","after":"fbb6ebe5aee8f17cc526a0afffb766c8afeb87e2","ref":"refs/heads/master","pushedAt":"2023-10-16T11:25:17.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"spitters","name":"Bas Spitters","path":"/spitters","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/210638?s=80&v=4"},"commit":{"message":"Merge pull request #121 from Villetaneuse/rm_arith_files\n\nRemove deprecated files in Coq.Arith","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1944964107\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq-community/math-classes/issues/121\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq-community/math-classes/pull/121/hovercard\" href=\"https://github.com/coq-community/math-classes/pull/121\">#121</a> from Villetaneuse/rm_arith_files"}},{"before":"2f6d4dabeab21223155aa960c72a0907f9ffb66c","after":null,"ref":"refs/heads/master+adapting-cast-using-scope-bound-to-type","pushedAt":"2023-10-05T14:22:53.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"}},{"before":"d3fdd9a8b39d96760bb349813b8a498841603071","after":"aaaf68fca837effde7d2a7f17b3e52455fadd08a","ref":"refs/heads/master","pushedAt":"2023-10-05T14:22:48.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Merge pull request #118 from coq-community/master+adapting-cast-using-scope-bound-to-type\n\nAdapt to https://github.com/coq/coq/pull/6134","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1913076254\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq-community/math-classes/issues/118\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq-community/math-classes/pull/118/hovercard\" href=\"https://github.com/coq-community/math-classes/pull/118\">#118</a> from coq-community/master+adapting-cast-using…"}},{"before":"7a57556e489989cb38899decf61ea66f4394c60f","after":"d3fdd9a8b39d96760bb349813b8a498841603071","ref":"refs/heads/master","pushedAt":"2023-09-29T08:41:17.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Zimmi48","name":"Théo Zimmermann","path":"/Zimmi48","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1108325?s=80&v=4"},"commit":{"message":"Merge pull request #119 from Zimmi48/test-coq-8.18\n\nIntroducing CI for Coq 8.18.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1918844598\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq-community/math-classes/issues/119\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq-community/math-classes/pull/119/hovercard\" href=\"https://github.com/coq-community/math-classes/pull/119\">#119</a> from Zimmi48/test-coq-8.18"}},{"before":null,"after":"2f6d4dabeab21223155aa960c72a0907f9ffb66c","ref":"refs/heads/master+adapting-cast-using-scope-bound-to-type","pushedAt":"2023-09-26T09:19:59.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"proux01","name":"Pierre Roux","path":"/proux01","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15833376?s=80&v=4"},"commit":{"message":"Adapting to interpretation of (x:T) now activating scope for T if any.\n\nThese were situations where the cast was needed to hint type class\ninference but the body was expected to be interpreted in the\ntype-class (current) scope rather than in the more specialized scope\nbound to the cast type.\n\nWe add a \"%mc\" to force using the type-class based generic\ninterpretation.","shortMessageHtmlLink":"Adapting to interpretation of (x:T) now activating scope for T if any."}},{"before":"c11eb05a1e58a7293ef9a9a046ca02a9fd5b44bc","after":"7a57556e489989cb38899decf61ea66f4394c60f","ref":"refs/heads/master","pushedAt":"2023-05-04T14:50:01.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Merge pull request #117 from ppedrot/case-pf-pose-dependent-metas\n\nAdapt w.r.t. coq/coq#17564.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1695570540\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq-community/math-classes/issues/117\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq-community/math-classes/pull/117/hovercard\" href=\"https://github.com/coq-community/math-classes/pull/117\">#117</a> from ppedrot/case-pf-pose-dependent-metas"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAELh0RbQA","startCursor":null,"endCursor":null}},"title":"Activity · coq-community/math-classes"}