{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":821198520,"defaultBranch":"master","name":"coq","ownerLogin":"stepbrobd","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2024-06-28T03:01:03.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/81826728?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1719543670.958785","currentOid":""},"activityList":{"items":[{"before":"f9d9e518a4dd59bdbbc20087147ba9a3def2261a","after":"48db2360c32d779f948e110fdfbaae3d99c03fa3","ref":"refs/heads/master","pushedAt":"2024-09-14T00:20:49.000Z","pushType":"push","commitsCount":9,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19542: Fix all uses of instantiate_context\n\nReviewed-by: SkySkimmer\nReviewed-by: mattam82\nCo-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2524417610\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19542\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19542/hovercard\" href=\"https://github.com/coq/coq/pull/19542\">coq#19542</a>: Fix all uses of instantiate_context"}},{"before":"44155b062e6c384cc3ca36293b99dcd13f9cb085","after":"f9d9e518a4dd59bdbbc20087147ba9a3def2261a","ref":"refs/heads/master","pushedAt":"2024-09-13T00:20:09.000Z","pushType":"push","commitsCount":11,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19475: Add example of \"discriminate\" limitation (it doesn't handle impossible equations such as n = (S n)\n\nReviewed-by: proux01\nAck-by: JasonGross\nAck-by: herbelin\nAck-by: silene\nAck-by: SkySkimmer\nCo-authored-by: proux01 <proux01@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2487959770\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19475\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19475/hovercard\" href=\"https://github.com/coq/coq/pull/19475\">coq#19475</a>: Add example of \"discriminate\" limitation (it does…"}},{"before":"ce1cbe6dd1f7a61861e80d9dfdeaf5e98cb83abb","after":"44155b062e6c384cc3ca36293b99dcd13f9cb085","ref":"refs/heads/master","pushedAt":"2024-09-12T00:20:35.000Z","pushType":"push","commitsCount":11,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19525: template_polymorphism_candidate: forbid levels appearing in indices\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2516498330\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19525\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19525/hovercard\" href=\"https://github.com/coq/coq/pull/19525\">coq#19525</a>: template_polymorphism_candidate: forbid levels ap…"}},{"before":"cc6786a62853030e0b48be5c5debb4f2efe24c44","after":"ce1cbe6dd1f7a61861e80d9dfdeaf5e98cb83abb","ref":"refs/heads/master","pushedAt":"2024-09-11T00:19:56.000Z","pushType":"push","commitsCount":10,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19509: Compare projections by repr name in RRs\n\nReviewed-by: SkySkimmer\nCo-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2508088122\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19509\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19509/hovercard\" href=\"https://github.com/coq/coq/pull/19509\">coq#19509</a>: Compare projections by repr name in RRs"}},{"before":"1b98a2ff7b606fdfd5f70fbf602af80c2b5652ed","after":"cc6786a62853030e0b48be5c5debb4f2efe24c44","ref":"refs/heads/master","pushedAt":"2024-09-10T00:20:24.000Z","pushType":"push","commitsCount":18,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19516: [CI] FCSL-pcm now depends on MathComp 2\n\nReviewed-by: SkySkimmer\nCo-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2513715232\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19516\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19516/hovercard\" href=\"https://github.com/coq/coq/pull/19516\">coq#19516</a>: [CI] FCSL-pcm now depends on MathComp 2"}},{"before":"9c1e8bd203e52ac907d3057ec83c6c027b9c1d00","after":"1b98a2ff7b606fdfd5f70fbf602af80c2b5652ed","ref":"refs/heads/master","pushedAt":"2024-09-06T19:31:47.000Z","pushType":"push","commitsCount":19,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19501: Ncring_tac: avoid generating temporary pairs in main loop\n\nReviewed-by: ppedrot\nAck-by: silene\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2503157388\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19501\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19501/hovercard\" href=\"https://github.com/coq/coq/pull/19501\">coq#19501</a>: Ncring_tac: avoid generating temporary pairs in m…"}},{"before":"fa5011da397885dd0d0e257f0ba3d4069af110ad","after":"9c1e8bd203e52ac907d3057ec83c6c027b9c1d00","ref":"refs/heads/master","pushedAt":"2024-09-05T19:33:16.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19031: A common execution path for universe restriction + universe declaration check\n\nReviewed-by: SkySkimmer\nCo-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2297952851\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19031\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19031/hovercard\" href=\"https://github.com/coq/coq/pull/19031\">coq#19031</a>: A common execution path for universe restriction …"}},{"before":"43cec4686b29d200c404661211b2782fb09406d3","after":"fa5011da397885dd0d0e257f0ba3d4069af110ad","ref":"refs/heads/master","pushedAt":"2024-09-05T00:20:11.000Z","pushType":"push","commitsCount":10,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19441: coqchk accept absolute vo paths\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2442631068\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19441\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19441/hovercard\" href=\"https://github.com/coq/coq/pull/19441\">coq#19441</a>: coqchk accept absolute vo paths"}},{"before":"914a38a12e7b055cfaa1dca69d74bb8ebbca7e3b","after":"43cec4686b29d200c404661211b2782fb09406d3","ref":"refs/heads/master","pushedAt":"2024-09-04T00:22:06.000Z","pushType":"push","commitsCount":14,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19437: Reduce the amount of typechecking in Ssrequality.\n\nReviewed-by: gares\nCo-authored-by: gares <gares@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2440372880\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19437\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19437/hovercard\" href=\"https://github.com/coq/coq/pull/19437\">coq#19437</a>: Reduce the amount of typechecking in Ssrequality."}},{"before":"9ed5a0f0cec89ec78aa6406dfae19dcb1bb85e6c","after":"914a38a12e7b055cfaa1dca69d74bb8ebbca7e3b","ref":"refs/heads/master","pushedAt":"2024-09-03T00:19:52.000Z","pushType":"push","commitsCount":19,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19492: votour add vmlibrary to known segments\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2500596606\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19492\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19492/hovercard\" href=\"https://github.com/coq/coq/pull/19492\">coq#19492</a>: votour add vmlibrary to known segments"}},{"before":"3421892334d38a5fbeb2bea0a25a71508a2de994","after":"9ed5a0f0cec89ec78aa6406dfae19dcb1bb85e6c","ref":"refs/heads/master","pushedAt":"2024-08-28T00:19:41.000Z","pushType":"push","commitsCount":14,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19474: Tweak formatting of \"Print HintDb\" output\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2487857859\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19474\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19474/hovercard\" href=\"https://github.com/coq/coq/pull/19474\">coq#19474</a>: Tweak formatting of \"Print HintDb\" output"}},{"before":"d6550d16f01d39dee97f7e645e415de51725fd2e","after":"3421892334d38a5fbeb2bea0a25a71508a2de994","ref":"refs/heads/master","pushedAt":"2024-08-23T00:19:01.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19409: Bench: don't print CPU cycles in table\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2423033441\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19409\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19409/hovercard\" href=\"https://github.com/coq/coq/pull/19409\">coq#19409</a>: Bench: don't print CPU cycles in table"}},{"before":"827f3de61d7be0cc7bdad9589af564f3cd2826e5","after":"d6550d16f01d39dee97f7e645e415de51725fd2e","ref":"refs/heads/master","pushedAt":"2024-08-15T09:44:39.000Z","pushType":"push","commitsCount":33,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19463: [CI] Revert \"Mark jasmin as allow_failure\"\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2463728947\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19463\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19463/hovercard\" href=\"https://github.com/coq/coq/pull/19463\">coq#19463</a>: [CI] Revert \"Mark jasmin as allow_failure\""}},{"before":"e49d818b874db795f167da93b395a143a23988c1","after":"827f3de61d7be0cc7bdad9589af564f3cd2826e5","ref":"refs/heads/master","pushedAt":"2024-08-07T10:41:46.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19388: Printing tweaks: use format \"compacting box\" instead of hovbox + tweak `fun =>` break hint\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2413831986\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19388\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19388/hovercard\" href=\"https://github.com/coq/coq/pull/19388\">coq#19388</a>: Printing tweaks: use format \"compacting box\" inst…"}},{"before":"aaa0c139a1a117fca1b8a47508acd1ae01ecc2cd","after":"e49d818b874db795f167da93b395a143a23988c1","ref":"refs/heads/master","pushedAt":"2024-08-06T08:00:17.000Z","pushType":"push","commitsCount":83,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19438: Local bench download opam after user interaction (asking for commits)\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2440703614\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19438\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19438/hovercard\" href=\"https://github.com/coq/coq/pull/19438\">coq#19438</a>: Local bench download opam after user interaction …"}},{"before":"b5e1e1057c8b37ccd22a6a2a7d0653d95dad469d","after":"aaa0c139a1a117fca1b8a47508acd1ae01ecc2cd","ref":"refs/heads/master","pushedAt":"2024-07-20T09:16:49.000Z","pushType":"push","commitsCount":70,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19382: [ssr] Remove no longer used not_locked_false_eq_true\n\nReviewed-by: gares\nCo-authored-by: gares <gares@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2412866940\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19382\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19382/hovercard\" href=\"https://github.com/coq/coq/pull/19382\">coq#19382</a>: [ssr] Remove no longer used not_locked_false_eq_true"}},{"before":"e564bef2404475ec83061cf7bf4b0759d58aca85","after":"b5e1e1057c8b37ccd22a6a2a7d0653d95dad469d","ref":"refs/heads/master","pushedAt":"2024-07-15T07:24:38.000Z","pushType":"push","commitsCount":22,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19341: Allow eliminating sort poly inductive instantiated to Type at sort poly types\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2395191733\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19341\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19341/hovercard\" href=\"https://github.com/coq/coq/pull/19341\">coq#19341</a>: Allow eliminating sort poly inductive instantiate…"}},{"before":"ace46ff41dd77c969339379eac89fbcf1169a011","after":"e564bef2404475ec83061cf7bf4b0759d58aca85","ref":"refs/heads/master","pushedAt":"2024-07-10T11:14:21.000Z","pushType":"push","commitsCount":27,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19340: Simplify memprof_coq.std.ml\n\nReviewed-by: ejgallego\nReviewed-by: gadmm\nCo-authored-by: ejgallego <ejgallego@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2395112740\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19340\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19340/hovercard\" href=\"https://github.com/coq/coq/pull/19340\">coq#19340</a>: Simplify memprof_coq.std.ml"}},{"before":"1c256e62d726f3b04db86af5c0d1770f2aaaeeaf","after":"ace46ff41dd77c969339379eac89fbcf1169a011","ref":"refs/heads/master","pushedAt":"2024-07-07T06:40:55.000Z","pushType":"push","commitsCount":86,"pusher":{"login":"stepbrobd","name":"StepBroBD","path":"/stepbrobd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/81826728?s=80&v=4"},"commit":{"message":"Merge PR #19328: Fix double substitution of relevance annotations in cclosure\n\nReviewed-by: ppedrot\nCo-authored-by: ppedrot <ppedrot@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2392263333\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19328\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19328/hovercard\" href=\"https://github.com/coq/coq/pull/19328\">coq#19328</a>: Fix double substitution of relevance annotations …"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xNFQwMDoyMDo0OS4wMDAwMDBazwAAAAS1-QjH","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xNFQwMDoyMDo0OS4wMDAwMDBazwAAAAS1-QjH","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNy0wN1QwNjo0MDo1NS4wMDAwMDBazwAAAAR4uqNB"}},"title":"Activity · stepbrobd/coq"}