{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":107535901,"defaultBranch":"coq-8.19","name":"metacoq","ownerLogin":"MetaCoq","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2017-10-19T11:10:54.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/32929165?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1726478006.0","currentOid":""},"activityList":{"items":[{"before":"ac6100ebdc75b433d040c7cef3525b78450faf5a","after":"d4a0fffb6dad46e6c69c2eb993ceee17fee66671","ref":"refs/heads/coq-8.19","pushedAt":"2024-09-16T09:15:49.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Merge pull request #1086 from MevenBertrand/correct-noccur\n\nCorrect noccur for Template","shortMessageHtmlLink":"Merge pull request #1086 from MevenBertrand/correct-noccur"}},{"before":"1d547dfac520941f353d7c4e7666532829d832d8","after":"b5c0239a0e6389cbec731f28a3fc7282d230be65","ref":"refs/heads/main","pushedAt":"2024-09-16T09:15:28.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Merge pull request #1087 from MevenBertrand/correct-noccur-main\n\nCorrecting the definition of noccur_between in Template – main branch","shortMessageHtmlLink":"Merge pull request #1087 from MevenBertrand/correct-noccur-main"}},{"before":"734acd2b70528a6a7dcf33ac2edf3996bc50636a","after":"ac6100ebdc75b433d040c7cef3525b78450faf5a","ref":"refs/heads/coq-8.19","pushedAt":"2024-09-16T09:14:49.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Point 'index' in CoqDocJS header to index.html (#1094)","shortMessageHtmlLink":"Point 'index' in CoqDocJS header to index.html (#1094)"}},{"before":"a586da203ef8fbdefeee6836495b76edaadc56e5","after":null,"ref":"refs/heads/dependabot/github_actions/coq-8.16/cachix/install-nix-action-V28","pushedAt":"2024-09-16T09:13:26.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"}},{"before":"2f51e64e8c6a39454466edb819a0fef2e0f02a61","after":"7943c6d9bf4a0c7586ab87a14cf80603a8a85b89","ref":"refs/heads/coq-8.16","pushedAt":"2024-09-16T09:13:23.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Bump cachix/install-nix-action from V27 to 28 (#1100)\n\nBumps [cachix/install-nix-action](https://github.com/cachix/install-nix-action) from V27 to 28. This release includes the previously tagged commit.\r\n- [Release notes](https://github.com/cachix/install-nix-action/releases)\r\n- [Commits](https://github.com/cachix/install-nix-action/compare/V27...V28)\r\n\r\n---\r\nupdated-dependencies:\r\n- dependency-name: cachix/install-nix-action\r\n dependency-type: direct:production\r\n...\r\n\r\nSigned-off-by: dependabot[bot] \r\nCo-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>","shortMessageHtmlLink":"Bump cachix/install-nix-action from V27 to 28 (#1100)"}},{"before":null,"after":"a586da203ef8fbdefeee6836495b76edaadc56e5","ref":"refs/heads/dependabot/github_actions/coq-8.16/cachix/install-nix-action-V28","pushedAt":"2024-09-12T16:23:41.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"dependabot[bot]","name":null,"path":"/apps/dependabot","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/29110?s=80&v=4"},"commit":{"message":"Bump cachix/install-nix-action from V27 to 28\n\nBumps [cachix/install-nix-action](https://github.com/cachix/install-nix-action) from V27 to 28. This release includes the previously tagged commit.\n- [Release notes](https://github.com/cachix/install-nix-action/releases)\n- [Commits](https://github.com/cachix/install-nix-action/compare/V27...V28)\n\n---\nupdated-dependencies:\n- dependency-name: cachix/install-nix-action\n dependency-type: direct:production\n...\n\nSigned-off-by: dependabot[bot] ","shortMessageHtmlLink":"Bump cachix/install-nix-action from V27 to 28"}},{"before":"3067209cece44b18c834add334bc9b6629274c1e","after":"1d547dfac520941f353d7c4e7666532829d832d8","ref":"refs/heads/main","pushedAt":"2024-09-10T07:03:26.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 #1093 from proux01/coq_19310\n\nAdapt to https://github.com/coq/coq/pull/19310","shortMessageHtmlLink":"Merge pull request #1093 from proux01/coq_19310"}},{"before":"c8e165840a0b90e78f1d3f9adb2fe11974ef95ad","after":"b59ea922a0cd2985f62fb7cac00334054df166ef","ref":"refs/heads/coq-8.20","pushedAt":"2024-09-03T11:46:56.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Update make-opam-files script","shortMessageHtmlLink":"Update make-opam-files script"}},{"before":"b1b6be23e00fefba6a03c153a458e72acb463daa","after":"734acd2b70528a6a7dcf33ac2edf3996bc50636a","ref":"refs/heads/coq-8.19","pushedAt":"2024-09-03T11:44:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Remove unneeded problematic universe constraints","shortMessageHtmlLink":"Remove unneeded problematic universe constraints"}},{"before":"a08708bc2228c0dda0978f45cbe6160202435840","after":"3067209cece44b18c834add334bc9b6629274c1e","ref":"refs/heads/main","pushedAt":"2024-08-30T17:05:26.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 #1098 from ppedrot/typecheck-unquote\n\nTypecheck the result of term unquotation.","shortMessageHtmlLink":"Merge pull request #1098 from ppedrot/typecheck-unquote"}},{"before":"6670cb34af22ef86263f2bb665c76a6f59b93109","after":"b66e834a43982f874c35e4e774412aab4475cec9","ref":"refs/heads/fix-standardization","pushedAt":"2024-08-29T10:47:06.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"yforster","name":"Yannick Forster","path":"/yforster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4191846?s=80&v=4"},"commit":{"message":"fix statement of wcbv standardization","shortMessageHtmlLink":"fix statement of wcbv standardization"}},{"before":null,"after":"6670cb34af22ef86263f2bb665c76a6f59b93109","ref":"refs/heads/fix-standardization","pushedAt":"2024-08-29T10:45:54.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"yforster","name":"Yannick Forster","path":"/yforster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4191846?s=80&v=4"},"commit":{"message":"fix statement of wcbv standardization","shortMessageHtmlLink":"fix statement of wcbv standardization"}},{"before":"a40e80779212e6fbeed392f7717ca1848b756ec6","after":"a08708bc2228c0dda0978f45cbe6160202435840","ref":"refs/heads/main","pushedAt":"2024-08-23T15:53:32.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Merge branch 'coq-8.20'","shortMessageHtmlLink":"Merge branch 'coq-8.20'"}},{"before":"4676c4736864e1ca7ccd1da9766473a72518443a","after":"c8e165840a0b90e78f1d3f9adb2fe11974ef95ad","ref":"refs/heads/coq-8.20","pushedAt":"2024-08-23T15:53:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Fix erasure_live_test","shortMessageHtmlLink":"Fix erasure_live_test"}},{"before":"1d5976a7457fbac0c64e7837d3e2d4811867386d","after":"a40e80779212e6fbeed392f7717ca1848b756ec6","ref":"refs/heads/main","pushedAt":"2024-08-23T15:43:04.000Z","pushType":"push","commitsCount":48,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Merge branch 'coq-8.20'","shortMessageHtmlLink":"Merge branch 'coq-8.20'"}},{"before":"b5bd6e5e81ca233dab6b863aada623a4628ec204","after":"4676c4736864e1ca7ccd1da9766473a72518443a","ref":"refs/heads/coq-8.20","pushedAt":"2024-08-23T15:14:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Fixes after merge","shortMessageHtmlLink":"Fixes after merge"}},{"before":"13a68523f688faa040263929e6cd11dcb7c11970","after":"b5bd6e5e81ca233dab6b863aada623a4628ec204","ref":"refs/heads/coq-8.20","pushedAt":"2024-08-23T14:22:11.000Z","pushType":"push","commitsCount":42,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Merge branch 'coq-8.19' into coq-8.20","shortMessageHtmlLink":"Merge branch 'coq-8.19' into coq-8.20"}},{"before":"52fda991e207560dcfe916fb98c7a71cd4f2d65b","after":"1d5976a7457fbac0c64e7837d3e2d4811867386d","ref":"refs/heads/main","pushedAt":"2024-07-24T12:20:48.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 #1096 from SkySkimmer/more-demote\n\nAdapt to coq/coq#19384 (add_global_univ -> add_forgotten_univ)","shortMessageHtmlLink":"Merge pull request #1096 from SkySkimmer/more-demote"}},{"before":"462f3abaab68e5ca3fd861fcee29c660a2570b5b","after":"b1b6be23e00fefba6a03c153a458e72acb463daa","ref":"refs/heads/coq-8.19","pushedAt":"2024-07-22T14:24:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"make-opam-files now computes the appropriate ci-skip line","shortMessageHtmlLink":"make-opam-files now computes the appropriate ci-skip line"}},{"before":"37d26b580805b10be73ed4a0480d4c2527d88fbc","after":null,"ref":"refs/heads/reorder-proof","pushedAt":"2024-07-22T12:46:52.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"}},{"before":"13dc7ce5b1526ee783722ff4985249951704116d","after":"462f3abaab68e5ca3fd861fcee29c660a2570b5b","ref":"refs/heads/coq-8.19","pushedAt":"2024-07-22T12:46:51.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Proof that reordering of constructors is correct (#1095)\n\n* WIP on reordering constructors\r\n\r\n* New/old tag reasoning\r\n\r\n* WIP correctness of constructor reordering. main lemma proven\r\n\r\n* Reordering preserves well-formedness\r\n\r\n* Reorderin\r\n\r\n* Admit free proofs of preservation for wf and substitution\r\n\r\n* WIP adapting to an additional mapping argument for transforms and stronger wellformedness property on extracted terms\r\n\r\n* Full composed pipeline with mapping of constructors\r\n\r\n* Fixes due to removal of useless -fast flag and change for reordering of constructors, now verified\r\n\r\n* Remove option to reorder constructors, now safely done always\r\n\r\n* Fix metacoq_tour\r\n\r\n* Fix a remaining todo\r\n\r\n* Remove generated files","shortMessageHtmlLink":"Proof that reordering of constructors is correct (#1095)"}},{"before":"b1514251837f59a28ea522ecdf5442faee8839e1","after":"37d26b580805b10be73ed4a0480d4c2527d88fbc","ref":"refs/heads/reorder-proof","pushedAt":"2024-07-22T11:17:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Remove generated files","shortMessageHtmlLink":"Remove generated files"}},{"before":"c6180f0c2771bfd6bf3ab32c5c1ae1198118485b","after":"b1514251837f59a28ea522ecdf5442faee8839e1","ref":"refs/heads/reorder-proof","pushedAt":"2024-07-22T11:14:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Fix a remaining todo","shortMessageHtmlLink":"Fix a remaining todo"}},{"before":"67ee744b66091df8161fdac458c4d2ff7ac04ef4","after":"c6180f0c2771bfd6bf3ab32c5c1ae1198118485b","ref":"refs/heads/reorder-proof","pushedAt":"2024-07-22T11:03:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Fix metacoq_tour","shortMessageHtmlLink":"Fix metacoq_tour"}},{"before":"2c201c5ca89c50edf1fb8cd8e1fa78be30df801d","after":"67ee744b66091df8161fdac458c4d2ff7ac04ef4","ref":"refs/heads/reorder-proof","pushedAt":"2024-07-19T17:17:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Remove option to reorder constructors, now safely done always","shortMessageHtmlLink":"Remove option to reorder constructors, now safely done always"}},{"before":"75f368bc38caf5f6df29c944bd83c507233a067a","after":"2c201c5ca89c50edf1fb8cd8e1fa78be30df801d","ref":"refs/heads/reorder-proof","pushedAt":"2024-07-19T16:40:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Fixes due to removal of useless -fast flag and change for reordering of constructors, now verified","shortMessageHtmlLink":"Fixes due to removal of useless -fast flag and change for reordering …"}},{"before":"9ecc7b5ee70b9222dcff6a168c22ffd7eb106a44","after":"75f368bc38caf5f6df29c944bd83c507233a067a","ref":"refs/heads/reorder-proof","pushedAt":"2024-07-19T15:59:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Full composed pipeline with mapping of constructors","shortMessageHtmlLink":"Full composed pipeline with mapping of constructors"}},{"before":"4a2c169063bac857d3383d2fd146e15cb13cfdc4","after":"9ecc7b5ee70b9222dcff6a168c22ffd7eb106a44","ref":"refs/heads/reorder-proof","pushedAt":"2024-07-18T16:11:44.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"WIP adapting to an additional mapping argument for transforms and stronger wellformedness property on extracted terms","shortMessageHtmlLink":"WIP adapting to an additional mapping argument for transforms and str…"}},{"before":null,"after":"4a2c169063bac857d3383d2fd146e15cb13cfdc4","ref":"refs/heads/reorder-proof","pushedAt":"2024-07-17T09:43:45.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Reordering preserves well-formedness","shortMessageHtmlLink":"Reordering preserves well-formedness"}},{"before":null,"after":"13a68523f688faa040263929e6cd11dcb7c11970","ref":"refs/heads/coq-8.20","pushedAt":"2024-07-09T12:50:48.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/98373?s=80&v=4"},"commit":{"message":"Update opam file dependencies for 8.20 version","shortMessageHtmlLink":"Update opam file dependencies for 8.20 version"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xNlQwOToxNTo0OS4wMDAwMDBazwAAAAS3OLFv","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xNlQwOToxNTo0OS4wMDAwMDBazwAAAAS3OLFv","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNy0wOVQxMjo1MDo0OC4wMDAwMDBazwAAAAR6qvVh"}},"title":"Activity · MetaCoq/metacoq"}