{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":1377159,"defaultBranch":"master","name":"coq","ownerLogin":"coq","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2011-02-17T05:49:37.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/621198?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1709556870.0","currentOid":""},"activityList":{"items":[{"before":"4b5d00c66bf14a2a426e0efcd24c64316f3b5843","after":"9e16bf8e51673db6ff0c735f4f2d399b53830dfa","ref":"refs/heads/master","pushedAt":"2024-06-02T13:37:05.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19112: dune-project: memtrace is a depopt\n\nReviewed-by: Alizter\nCo-authored-by: Alizter <Alizter@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2323473161\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19112\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19112/hovercard\" href=\"https://github.com/coq/coq/pull/19112\">#19112</a>: dune-project: memtrace is a depopt"}},{"before":"7ec2afddbe7d08988ca1836a7db132fd5d1a4a68","after":"4b5d00c66bf14a2a426e0efcd24c64316f3b5843","ref":"refs/heads/master","pushedAt":"2024-06-02T11:04:48.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19113: Do not store transitively required kernel libraries on disk.\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=\"2323606973\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19113\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19113/hovercard\" href=\"https://github.com/coq/coq/pull/19113\">#19113</a>: Do not store transitively required kernel libraries …"}},{"before":"7f437c3e7e1961c2215d9a7cd38b24c7baad5a8c","after":"7ec2afddbe7d08988ca1836a7db132fd5d1a4a68","ref":"refs/heads/master","pushedAt":"2024-06-01T15:40:07.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19119: Improve Ltac2 printing of glob exprs\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=\"2325885792\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19119\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19119/hovercard\" href=\"https://github.com/coq/coq/pull/19119\">#19119</a>: Improve Ltac2 printing of glob exprs"}},{"before":"df97595b637c81e0a1ed5ec223c031c786865d14","after":"7f437c3e7e1961c2215d9a7cd38b24c7baad5a8c","ref":"refs/heads/master","pushedAt":"2024-06-01T15:26:40.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19115: Use Coqlib for setoid_rewrite\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=\"2325156621\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19115\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19115/hovercard\" href=\"https://github.com/coq/coq/pull/19115\">#19115</a>: Use Coqlib for setoid_rewrite"}},{"before":"501a3cf63a6a82cd3dc341f0feb1ad72162f87c7","after":"df97595b637c81e0a1ed5ec223c031c786865d14","ref":"refs/heads/master","pushedAt":"2024-06-01T15:24:23.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19068: Move enforce_locality_exp definition and calling to DefAttributes\n\nReviewed-by: ppedrot\nReviewed-by: ejgallego\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=\"2310313629\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19068\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19068/hovercard\" href=\"https://github.com/coq/coq/pull/19068\">#19068</a>: Move enforce_locality_exp definition and calling to …"}},{"before":"89c971c739a8bcb39efb68087d5d4e981b46f83d","after":"501a3cf63a6a82cd3dc341f0feb1ad72162f87c7","ref":"refs/heads/master","pushedAt":"2024-06-01T15:22:42.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19116: Remove most deprecated coqlib.ml APIs\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=\"2325407583\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19116\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19116/hovercard\" href=\"https://github.com/coq/coq/pull/19116\">#19116</a>: Remove most deprecated coqlib.ml APIs"}},{"before":"4750d53f5438fa23e28690711ff13b0ae7329648","after":"89c971c739a8bcb39efb68087d5d4e981b46f83d","ref":"refs/heads/master","pushedAt":"2024-06-01T12:36:08.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19100: Fixes #19099: binders of universe polymorphic primitive constants treated as monomorphic\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=\"2319725784\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19100\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19100/hovercard\" href=\"https://github.com/coq/coq/pull/19100\">#19100</a>: <span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #19099.\">Fixes</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2319708250\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19099\" data-hovercard-type=\"issue\" data-hovercard-url=\"/coq/coq/issues/19099/hovercard\" href=\"https://github.com/coq/coq/issues/19099\">#19099</a>: binders of universe polymorphic primit…"}},{"before":"107788f92465a285c5ebc8d1b79b2b5f5b4febbc","after":"4750d53f5438fa23e28690711ff13b0ae7329648","ref":"refs/heads/master","pushedAt":"2024-05-31T17:18:28.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19049: [notations] Warn about incompatible prefixes\n\nReviewed-by: herbelin\nAck-by: jfehrle\nCo-authored-by: herbelin <herbelin@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2303200079\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19049\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19049/hovercard\" href=\"https://github.com/coq/coq/pull/19049\">#19049</a>: [notations] Warn about incompatible prefixes"}},{"before":"553f4540c8629d480ef69462c4cf2e939d585d5d","after":"107788f92465a285c5ebc8d1b79b2b5f5b4febbc","ref":"refs/heads/master","pushedAt":"2024-05-31T15:59:04.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19121: Move section about ltac1 defects to ltac.rst instead of ltac2.rst\n\nReviewed-by: proux01\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=\"2327784528\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19121\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19121/hovercard\" href=\"https://github.com/coq/coq/pull/19121\">#19121</a>: Move section about ltac1 defects to ltac.rst instead…"}},{"before":"19de84342f13da782772ad2d8b7bbc21a7571cae","after":"553f4540c8629d480ef69462c4cf2e939d585d5d","ref":"refs/heads/master","pushedAt":"2024-05-31T10:37:30.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #18602: Update of the doc of simpl and cbn, especially wrt \"simpl never\".\n\nReviewed-by: proux01\nAck-by: jfehrle\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=\"2112205069\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18602\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18602/hovercard\" href=\"https://github.com/coq/coq/pull/18602\">#18602</a>: Update of the doc of simpl and cbn, especially wrt \"…"}},{"before":"c67f36dc0d7954383cd9a6a03317ff0fd49aa590","after":"19de84342f13da782772ad2d8b7bbc21a7571cae","ref":"refs/heads/master","pushedAt":"2024-05-30T15:15:13.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19081: Use stages in gitlab-ci.yml\n\nReviewed-by: Zimmi48\nCo-authored-by: Zimmi48 <Zimmi48@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2315691866\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19081\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19081/hovercard\" href=\"https://github.com/coq/coq/pull/19081\">#19081</a>: Use stages in gitlab-ci.yml"}},{"before":"ac1e5ebd3f50a53b46cdb59225887841f5d24d02","after":"c67f36dc0d7954383cd9a6a03317ff0fd49aa590","ref":"refs/heads/master","pushedAt":"2024-05-30T11:01:54.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19084: A few renamings or documentation of code here and there to ease code understanding\n\nReviewed-by: SkySkimmer\nAck-by: ejgallego\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=\"2316863494\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19084\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19084/hovercard\" href=\"https://github.com/coq/coq/pull/19084\">#19084</a>: A few renamings or documentation of code here and th…"}},{"before":"f2dcd551be045bcd314e03915325662812709582","after":"ac1e5ebd3f50a53b46cdb59225887841f5d24d02","ref":"refs/heads/master","pushedAt":"2024-05-29T18:10:03.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19098: Use a structured type for Unification internal state.\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=\"2319692505\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19098\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19098/hovercard\" href=\"https://github.com/coq/coq/pull/19098\">#19098</a>: Use a structured type for Unification internal state."}},{"before":"1f6925d52f997e1e731253d4259d7792869ff316","after":"f2dcd551be045bcd314e03915325662812709582","ref":"refs/heads/master","pushedAt":"2024-05-29T10:35:24.000Z","pushType":"pr_merge","commitsCount":10,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #18989: Warn when automatically lowering an inductive declared with `: Type` to Prop\n\nReviewed-by: ppedrot\nAck-by: jfehrle\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=\"2269297531\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18989\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18989/hovercard\" href=\"https://github.com/coq/coq/pull/18989\">#18989</a>: Warn when automatically lowering an inductive declar…"}},{"before":"ca5c6337ec7ac5765feec01aee9ef59a7b638d2f","after":"1f6925d52f997e1e731253d4259d7792869ff316","ref":"refs/heads/master","pushedAt":"2024-05-29T09:54:53.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #18959: Compress the compiled bytecode.\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=\"2253436949\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18959\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18959/hovercard\" href=\"https://github.com/coq/coq/pull/18959\">#18959</a>: Compress the compiled bytecode."}},{"before":"2988866ad0d0a8cfcf1b17f15d021d250e188afc","after":"ca5c6337ec7ac5765feec01aee9ef59a7b638d2f","ref":"refs/heads/master","pushedAt":"2024-05-29T08:25:45.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19078: Add module types USetS UMapS for unordered maps\n\nReviewed-by: herbelin\nCo-authored-by: herbelin <herbelin@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2315382689\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19078\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19078/hovercard\" href=\"https://github.com/coq/coq/pull/19078\">#19078</a>: Add module types USetS UMapS for unordered maps"}},{"before":"8b5bff4dc3af4b26d79bc8e7a4d4f949e974b2a7","after":"2988866ad0d0a8cfcf1b17f15d021d250e188afc","ref":"refs/heads/master","pushedAt":"2024-05-29T07:58:29.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #18880: Clarify warning about Let/Variable/Hypothesis outside sections and turn it as error by default\n\nReviewed-by: herbelin\nAck-by: andres-erbsen\nAck-by: jfehrle\nAck-by: SkySkimmer\nCo-authored-by: herbelin <herbelin@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <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\">#18880</a>: Clarify warning about Let/Variable/Hypothesis outsid…"}},{"before":"fef831d81da502222ce58cd50981367d6d26a28e","after":"8b5bff4dc3af4b26d79bc8e7a4d4f949e974b2a7","ref":"refs/heads/master","pushedAt":"2024-05-29T07:54:38.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19094: Simplify declaremods internals\n\nReviewed-by: herbelin\nCo-authored-by: herbelin <herbelin@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2318987444\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19094\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19094/hovercard\" href=\"https://github.com/coq/coq/pull/19094\">#19094</a>: Simplify declaremods internals"}},{"before":"f7ecea960065cb7dae12d0c46cb322ed14f32005","after":"fef831d81da502222ce58cd50981367d6d26a28e","ref":"refs/heads/master","pushedAt":"2024-05-29T07:52:07.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #18588: [notation] Add warning for closed notations not at level 0\n\nReviewed-by: herbelin\nAck-by: SkySkimmer\nCo-authored-by: herbelin <herbelin@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2107961354\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18588\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18588/hovercard\" href=\"https://github.com/coq/coq/pull/18588\">#18588</a>: [notation] Add warning for closed notations not at l…"}},{"before":"7e92c036b9478c2e6d2654394d8fc24870f1edc6","after":"f7ecea960065cb7dae12d0c46cb322ed14f32005","ref":"refs/heads/master","pushedAt":"2024-05-29T06:23:47.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19052: coq_interp: squelch a incompatible-pointer warning\n\nReviewed-by: silene\nCo-authored-by: silene <silene@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2304590082\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19052\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19052/hovercard\" href=\"https://github.com/coq/coq/pull/19052\">#19052</a>: coq_interp: squelch a incompatible-pointer warning"}},{"before":"12ae6f264f8ab7d2c275984aa761bea544c045c7","after":"7e92c036b9478c2e6d2654394d8fc24870f1edc6","ref":"refs/heads/master","pushedAt":"2024-05-28T15:41:42.000Z","pushType":"pr_merge","commitsCount":13,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #18795: Towards a more uniform API for declare.ml (part declaring mutual statements)\n\nReviewed-by: ppedrot\nReviewed-by: ejgallego\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=\"2186423623\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18795\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/18795/hovercard\" href=\"https://github.com/coq/coq/pull/18795\">#18795</a>: Towards a more uniform API for declare.ml (part decl…"}},{"before":"9d772b51a43d40505a8f14abe6c4ebae7af0f966","after":"12ae6f264f8ab7d2c275984aa761bea544c045c7","ref":"refs/heads/master","pushedAt":"2024-05-28T15:21:26.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19093: Fix file extensions in CODEOWNERS.\n\nReviewed-by: silene\nCo-authored-by: silene <silene@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2318976850\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19093\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19093/hovercard\" href=\"https://github.com/coq/coq/pull/19093\">#19093</a>: Fix file extensions in CODEOWNERS."}},{"before":"00b1b52430e4a0b504e603838b1c1f5930e2f5b2","after":"9d772b51a43d40505a8f14abe6c4ebae7af0f966","ref":"refs/heads/master","pushedAt":"2024-05-28T12:04:53.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19096: Fix stage of ltac2 notation interp map (Tac2env.ltac_notations)\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=\"2319173094\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19096\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19096/hovercard\" href=\"https://github.com/coq/coq/pull/19096\">#19096</a>: Fix stage of ltac2 notation interp map (Tac2env.ltac…"}},{"before":"d4dfa2c69ee20b9e1d757f008b940d12f3ad4872","after":"00b1b52430e4a0b504e603838b1c1f5930e2f5b2","ref":"refs/heads/master","pushedAt":"2024-05-28T08:46:03.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19034: More efficient compilation of PArray blobs in the VM.\n\nReviewed-by: silene\nCo-authored-by: silene <silene@users.noreply.github.com>","shortMessageHtmlLink":"Merge PR <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2300348247\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19034\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19034/hovercard\" href=\"https://github.com/coq/coq/pull/19034\">#19034</a>: More efficient compilation of PArray blobs in the VM."}},{"before":"4d1f88853dc29c8604a92e77043eaaa38fca5490","after":"d4dfa2c69ee20b9e1d757f008b940d12f3ad4872","ref":"refs/heads/master","pushedAt":"2024-05-27T19:46:41.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19097: Avoid async proofs messing up test output/auto\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=\"2319210976\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19097\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19097/hovercard\" href=\"https://github.com/coq/coq/pull/19097\">#19097</a>: Avoid async proofs messing up test output/auto"}},{"before":"827020de1e79dee0c222525f31a485283473d45b","after":"4d1f88853dc29c8604a92e77043eaaa38fca5490","ref":"refs/heads/master","pushedAt":"2024-05-27T11:34:14.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19083: Various typos, as well as parentheses and spacing enhancement\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=\"2316849473\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19083\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19083/hovercard\" href=\"https://github.com/coq/coq/pull/19083\">#19083</a>: Various typos, as well as parentheses and spacing en…"}},{"before":"ed9fe8e2351ff59f662c3950c1cb07813db312bd","after":"827020de1e79dee0c222525f31a485283473d45b","ref":"refs/heads/master","pushedAt":"2024-05-27T09:30:15.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19086: A few complex guard condition tests found in CI\n\nReviewed-by: proux01\nAck-by: ppedrot\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=\"2316881434\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19086\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19086/hovercard\" href=\"https://github.com/coq/coq/pull/19086\">#19086</a>: A few complex guard condition tests found in CI"}},{"before":"21efd89d1c26ed8c744641eefe87d508b5bb118e","after":"ed9fe8e2351ff59f662c3950c1cb07813db312bd","ref":"refs/heads/master","pushedAt":"2024-05-26T13:01:30.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19089: Fixes #18914: check for overlap between notations was too confidently assuming being in the same entry\n\nReviewed-by: proux01\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=\"2317557421\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19089\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19089/hovercard\" href=\"https://github.com/coq/coq/pull/19089\">#19089</a>: <span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #18914.\">Fixes</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2232655206\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/18914\" data-hovercard-type=\"issue\" data-hovercard-url=\"/coq/coq/issues/18914/hovercard\" href=\"https://github.com/coq/coq/issues/18914\">#18914</a>: check for overlap between notations wa…"}},{"before":"466a853807cf44eaa40d7fd5a6d157aeafd2f3d0","after":"21efd89d1c26ed8c744641eefe87d508b5bb118e","ref":"refs/heads/master","pushedAt":"2024-05-26T11:47:56.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19080: include_constructor_argument don't ignore sort quality when not univ poly\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=\"2315449622\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19080\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19080/hovercard\" href=\"https://github.com/coq/coq/pull/19080\">#19080</a>: include_constructor_argument don't ignore sort quali…"}},{"before":"c4ae777b5971ba4595d44cd254d59c7d7b19aeba","after":"466a853807cf44eaa40d7fd5a6d157aeafd2f3d0","ref":"refs/heads/master","pushedAt":"2024-05-26T11:30:06.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"coqbot-app[bot]","name":null,"path":"/apps/coqbot-app","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/31373?s=80&v=4"},"commit":{"message":"Merge PR #19088: Fixes #19082: regression with primitive projections with defined fields\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=\"2317246840\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19088\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/coq/coq/pull/19088/hovercard\" href=\"https://github.com/coq/coq/pull/19088\">#19088</a>: <span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #19082.\">Fixes</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2316038608\" data-permission-text=\"Title is private\" data-url=\"https://github.com/coq/coq/issues/19082\" data-hovercard-type=\"issue\" data-hovercard-url=\"/coq/coq/issues/19082/hovercard\" href=\"https://github.com/coq/coq/issues/19082\">#19082</a>: regression with primitive projections …"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEWjEZzwA","startCursor":null,"endCursor":null}},"title":"Activity · coq/coq"}