{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":351551,"defaultBranch":"main","name":"Coq-Equations","ownerLogin":"mattam82","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2009-10-27T16:20:28.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/98373?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1704817400.0","currentOid":""},"activityList":{"items":[{"before":"fbafc9b0eac465e0fef22fd45b0c2f26c51cd40b","after":"1f43b47c6158bc79fea7748d40d037e7f7f1ab42","ref":"refs/heads/main","pushedAt":"2024-04-23T17:15:10.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 #591 from SkySkimmer/erelevance\n\nAdapt to coq/coq#18938 (EConstr.ERelevance)","shortMessageHtmlLink":"Merge pull request #591 from SkySkimmer/erelevance"}},{"before":"76b505f1c6b51598b032b7c9bc5fd0a0ba489129","after":"fbafc9b0eac465e0fef22fd45b0c2f26c51cd40b","ref":"refs/heads/main","pushedAt":"2024-04-16T11:36:47.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 #590 from ppedrot/econstr-inductiveops-api\n\nAdapt w.r.t. coq/coq#18935.","shortMessageHtmlLink":"Merge pull request #590 from ppedrot/econstr-inductiveops-api"}},{"before":"60105628c4359d5bf2d22ac595a69c84fbbc93f9","after":"76b505f1c6b51598b032b7c9bc5fd0a0ba489129","ref":"refs/heads/main","pushedAt":"2024-04-15T14:05:30.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 #588 from ppedrot/econstr-einstance-api\n\nAdapt w.r.t. coq/coq#18911.","shortMessageHtmlLink":"Merge pull request #588 from ppedrot/econstr-einstance-api"}},{"before":"0f75fa9412fc7047d6f3c66fd01834e6d3f3a6d4","after":"60105628c4359d5bf2d22ac595a69c84fbbc93f9","ref":"refs/heads/main","pushedAt":"2024-04-05T09:19:21.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 #587 from SkySkimmer/check-guard-evars\n\nAdapt to coq/coq#18864 (search_guard can handle evars)","shortMessageHtmlLink":"Merge pull request #587 from SkySkimmer/check-guard-evars"}},{"before":"962c005c3c5230121501233948c4f257060a1c45","after":"0f75fa9412fc7047d6f3c66fd01834e6d3f3a6d4","ref":"refs/heads/main","pushedAt":"2024-04-03T10:40:12.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 #582 from rlepigre/br/evaluable_refactoring\n\nAdapt to coq/coq#18546.","shortMessageHtmlLink":"Merge pull request #582 from rlepigre/br/evaluable_refactoring"}},{"before":"e43c620f649709c390a1a2e11bdfa95b80895c8d","after":"962c005c3c5230121501233948c4f257060a1c45","ref":"refs/heads/main","pushedAt":"2024-03-22T13:38:49.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 #586 from SkySkimmer/indirect\n\nDon't pierce Qed in debug message (adapt to coq/coq#18422)","shortMessageHtmlLink":"Merge pull request #586 from SkySkimmer/indirect"}},{"before":"729693206a944461807a9f3f78398d27bffff1e4","after":"e43c620f649709c390a1a2e11bdfa95b80895c8d","ref":"refs/heads/main","pushedAt":"2024-03-14T16:05:02.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 #578 from proux01/coq_18224\n\nAdapt to https://github.com/coq/coq/pull/18224","shortMessageHtmlLink":"Merge pull request #578 from proux01/coq_18224"}},{"before":"9c346fc1e44a911547cf83ec467c2ab3bdc78d3d","after":"729693206a944461807a9f3f78398d27bffff1e4","ref":"refs/heads/main","pushedAt":"2024-02-04T11:12:43.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 #581 from SkySkimmer/temrops-use-evd\n\nAdapt to coq/coq#18603 (print_rel_context takes evar map)","shortMessageHtmlLink":"Merge pull request #581 from SkySkimmer/temrops-use-evd"}},{"before":"e80a8e68deac437667f66423e4063b45b44ef0ff","after":"9c346fc1e44a911547cf83ec467c2ab3bdc78d3d","ref":"refs/heads/main","pushedAt":"2024-01-24T07:58:20.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 #574 from rlepigre/br/fix-18281\n\nAdapt to coq/coq#18327 (projection opacity)","shortMessageHtmlLink":"Merge pull request #574 from rlepigre/br/fix-18281"}},{"before":"a517a3e128719b078397a415dc9ce6b856019245","after":"e80a8e68deac437667f66423e4063b45b44ef0ff","ref":"refs/heads/main","pushedAt":"2024-01-23T19:34:21.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 #579 from ppedrot/fix-nf-evars\n\nRemove a useless evar normalization in Equations.define_by_eqs.","shortMessageHtmlLink":"Merge pull request #579 from ppedrot/fix-nf-evars"}},{"before":"79d3a45d960f4210eeb322593d61c7020df99271","after":"a517a3e128719b078397a415dc9ce6b856019245","ref":"refs/heads/main","pushedAt":"2023-11-21T15:27:36.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 #570 from Villetaneuse/arith_files_examples\n\nModify examples and tests for Coq/Coq#18164","shortMessageHtmlLink":"Merge pull request #570 from Villetaneuse/arith_files_examples"}},{"before":"d913185b007831641912a3c6132781f846621577","after":"79d3a45d960f4210eeb322593d61c7020df99271","ref":"refs/heads/main","pushedAt":"2023-11-21T14:20:07.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 #566 from herbelin/master+adapt-coq-pr18190-whd-cbv\n\nAdapt to coq PR #18190 adding a whd form of the cbv reduction strategy","shortMessageHtmlLink":"Merge pull request #566 from herbelin/master+adapt-coq-pr18190-whd-cbv"}},{"before":"8a3ec7581529ea2be02442cc0e863541ecb02f8f","after":"d913185b007831641912a3c6132781f846621577","ref":"refs/heads/main","pushedAt":"2023-11-15T11:02:15.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 #560 from SkySkimmer/pattern-quotations\n\nAdapt to coq/coq#17667 (Genintern.register_subst0 moved to Gensubst)","shortMessageHtmlLink":"Merge pull request #560 from SkySkimmer/pattern-quotations"}},{"before":"91199e97212dcbbad8561876cd7aad14ec8b093d","after":"8a3ec7581529ea2be02442cc0e863541ecb02f8f","ref":"refs/heads/main","pushedAt":"2023-11-13T14:53:36.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 #568 from SkySkimmer/ci-relevance\n\nAdapt to coq/coq#18280 (case relevance outside case info)","shortMessageHtmlLink":"Merge pull request #568 from SkySkimmer/ci-relevance"}},{"before":"dbc5fbbd9cf4447e4d4a7ff6a6be1b44f1f3654a","after":"91199e97212dcbbad8561876cd7aad14ec8b093d","ref":"refs/heads/main","pushedAt":"2023-11-13T13:38:54.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 #569 from ppedrot/glob-evar-kinds\n\nAdapt w.r.t. coq/coq#18294.","shortMessageHtmlLink":"Merge pull request #569 from ppedrot/glob-evar-kinds"}},{"before":"154a9763db5c44bb714e0ab1a26fed61ec8f7e47","after":"dbc5fbbd9cf4447e4d4a7ff6a6be1b44f1f3654a","ref":"refs/heads/main","pushedAt":"2023-11-06T20:44:41.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 #562 from SkySkimmer/sort-poly\n\nAdapt to coq/coq#17836 (sort poly)","shortMessageHtmlLink":"Merge pull request #562 from SkySkimmer/sort-poly"}},{"before":"d52417b21e6d6a924da3f34c27d59b37d8aa3999","after":"154a9763db5c44bb714e0ab1a26fed61ec8f7e47","ref":"refs/heads/main","pushedAt":"2023-10-30T12:04:11.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 #567 from herbelin/master+address-warnings-decompose\n\nAddress warnings related to Coq PR #17947 (extra renamings about decompose_prod_* functions)","shortMessageHtmlLink":"Merge pull request #567 from herbelin/master+address-warnings-decompose"}},{"before":"11d836d97bd43e446b2f145951ebc2662c30d578","after":"d52417b21e6d6a924da3f34c27d59b37d8aa3999","ref":"refs/heads/main","pushedAt":"2023-10-28T23:26:16.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 #564 from proux01/coq_18014\n\nAdapt to https://github.com/mattam82/Coq-Equations","shortMessageHtmlLink":"Merge pull request #564 from proux01/coq_18014"}},{"before":"50115700a84663f6736d4a59f696530ac249e488","after":"11d836d97bd43e446b2f145951ebc2662c30d578","ref":"refs/heads/main","pushedAt":"2023-09-19T07:01:19.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 #561 from rlepigre/br/cleanup-cclosure\n\nAdapt to coq/coq#18023 (RedFlags moving out of CClosure)","shortMessageHtmlLink":"Merge pull request #561 from rlepigre/br/cleanup-cclosure"}},{"before":"3c2342f9b15e20c91d36293126123ea617c7a532","after":"50115700a84663f6736d4a59f696530ac249e488","ref":"refs/heads/main","pushedAt":"2023-09-05T11:43:57.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 #557 from ppedrot/hint-cut-static-globref\n\nAdapt w.r.t. coq/coq#17955.","shortMessageHtmlLink":"Merge pull request #557 from ppedrot/hint-cut-static-globref"}},{"before":"21a3306a7e13b3037d20492bfdb5da75463929fb","after":"bef9ac7f5ab5c6549c7203a999f18f9bc3429655","ref":"refs/heads/8.18","pushedAt":"2023-08-17T15:20:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1202327?s=80&v=4"},"commit":{"message":"Prepare for 8.18 release.","shortMessageHtmlLink":"Prepare for 8.18 release."}},{"before":null,"after":"21a3306a7e13b3037d20492bfdb5da75463929fb","ref":"refs/heads/8.18","pushedAt":"2023-08-17T15:08:47.000Z","pushType":"branch_creation","commitsCount":0,"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 #551 from SkySkimmer/depr-versions\n\nAdapt to coq/coq#17664 (goptions use Deprecation.t option instead of bool)","shortMessageHtmlLink":"Merge pull request #551 from SkySkimmer/depr-versions"}},{"before":"e8b90902acb978a00e42a293710cd401b71de780","after":"3c2342f9b15e20c91d36293126123ea617c7a532","ref":"refs/heads/main","pushedAt":"2023-07-07T14:48:41.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 #553 from ppedrot/split-tactics-induction\n\nAdapt w.r.t. coq/coq#17824.","shortMessageHtmlLink":"Merge pull request #553 from ppedrot/split-tactics-induction"}},{"before":"21a3306a7e13b3037d20492bfdb5da75463929fb","after":"e8b90902acb978a00e42a293710cd401b71de780","ref":"refs/heads/main","pushedAt":"2023-06-29T13:54: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 #552 from ppedrot/split-generalize-tactics\n\nAdapt w.r.t. coq/coq#17768.","shortMessageHtmlLink":"Merge pull request #552 from ppedrot/split-generalize-tactics"}},{"before":"8e17a7b2338891d2cc59d0213e7b5b4d30478af1","after":"21a3306a7e13b3037d20492bfdb5da75463929fb","ref":"refs/heads/main","pushedAt":"2023-06-06T08:16:45.073Z","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 #551 from SkySkimmer/depr-versions\n\nAdapt to coq/coq#17664 (goptions use Deprecation.t option instead of bool)","shortMessageHtmlLink":"Merge pull request #551 from SkySkimmer/depr-versions"}},{"before":"1acd30d564e183c9edfad3bf7b936b992fc3fbb5","after":"8e17a7b2338891d2cc59d0213e7b5b4d30478af1","ref":"refs/heads/main","pushedAt":"2023-05-30T16:44:59.003Z","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 #548 from SkySkimmer/warn-api\n\nAdapt to coq/coq#17585 (revised warning API)","shortMessageHtmlLink":"Merge pull request #548 from SkySkimmer/warn-api"}},{"before":"dc71264209a3ff6f66049a31b5b451c28dfe070b","after":"1acd30d564e183c9edfad3bf7b936b992fc3fbb5","ref":"refs/heads/main","pushedAt":"2023-05-30T08:57:25.598Z","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 #550 from SkySkimmer/app-head\n\nAdapt to coq/coq#17633 (decompose_app returns array not list)","shortMessageHtmlLink":"Merge pull request #550 from SkySkimmer/app-head"}},{"before":"f46a01277d225721c29fb3892cb049495ce418ea","after":"dc71264209a3ff6f66049a31b5b451c28dfe070b","ref":"refs/heads/main","pushedAt":"2023-05-25T13:12:58.110Z","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 #549 from SkySkimmer/typing-relevance\n\nAdapt to coq/coq#17466 (relevance_of_sort takes evar map)","shortMessageHtmlLink":"Merge pull request #549 from SkySkimmer/typing-relevance"}},{"before":"9671e1be8116f0f52331c76839fbeda955b63ff0","after":"f46a01277d225721c29fb3892cb049495ce418ea","ref":"refs/heads/main","pushedAt":"2023-05-11T11:34:44.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 #546 from SkySkimmer/deprecate-definitions\n\nAdapt to coq/coq#16890 (combined_scheme takes Constant.t list not Id.t list)","shortMessageHtmlLink":"Merge pull request #546 from SkySkimmer/deprecate-definitions"}},{"before":"ab788faeb06143a920e70c5ac3ec2c8509412c3b","after":"9671e1be8116f0f52331c76839fbeda955b63ff0","ref":"refs/heads/main","pushedAt":"2023-05-09T09:29:17.000Z","pushType":"pr_merge","commitsCount":4,"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 #547 from ppedrot/stop-checking-split\n\nStop checking the returned split well-typedness.","shortMessageHtmlLink":"Merge pull request #547 from ppedrot/stop-checking-split"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEOFPnpAA","startCursor":null,"endCursor":null}},"title":"Activity · mattam82/Coq-Equations"}