{"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://github.com/avatars/u/98373?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1724755753.0","currentOid":""},"activityList":{"items":[{"before":null,"after":"f9f7d3cdf91bae89f255335e083e9ddd5325f8df","ref":"refs/heads/8.20","pushedAt":"2024-08-27T10:49:13.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Merge pull request #608 from ppedrot/enforce-more-static-typing\n\nEnforce more static typing","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2341247484\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/608\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/608/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/608\">#608</a> from ppedrot/enforce-more-static-typing"}},{"before":"abed6092520259b6d1a2995c69c031b76ee8fd02","after":"7863db39705298aeabfe6cc7f7518d30ec96b246","ref":"refs/heads/main","pushedAt":"2024-07-09T14:51:57.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://github.com/avatars/u/1202327?s=80&v=4"},"commit":{"message":"Merge pull request #612 from SkySkimmer/fix-congruence\n\nFix call to congruence after coq/coq#19032","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2398272698\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/612\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/612/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/612\">#612</a> from SkySkimmer/fix-congruence"}},{"before":"6dd638397cdc8c8a98513e269a0f85c8e3c20cf6","after":"abed6092520259b6d1a2995c69c031b76ee8fd02","ref":"refs/heads/main","pushedAt":"2024-07-08T13:14:32.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://github.com/avatars/u/1202327?s=80&v=4"},"commit":{"message":"Merge pull request #610 from gares/quickfix-deprecated\n\nadapt to coq/coq#19300","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2390071783\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/610\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/610/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/610\">#610</a> from gares/quickfix-deprecated"}},{"before":"f9f7d3cdf91bae89f255335e083e9ddd5325f8df","after":"6dd638397cdc8c8a98513e269a0f85c8e3c20cf6","ref":"refs/heads/main","pushedAt":"2024-07-05T12:34:06.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://github.com/avatars/u/1202327?s=80&v=4"},"commit":{"message":"Merge pull request #611 from ppedrot/ltac1-split-some-plugins\n\nAdapt w.r.t. coq/coq#19313.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2390232369\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/611\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/611/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/611\">#611</a> from ppedrot/ltac1-split-some-plugins"}},{"before":"d23be2cf35634b3b60fe73e818c6e3e982f0b616","after":"2183ceb722f6e9957043d7a120c584c71bf4a848","ref":"refs/heads/universes-clauses","pushedAt":"2024-06-21T13:17:22.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Adapt to PR#18903","shortMessageHtmlLink":"Adapt to PR#18903"}},{"before":"cb55e63700b511083d71b9e09a0e05b83ba15aea","after":"f9f7d3cdf91bae89f255335e083e9ddd5325f8df","ref":"refs/heads/main","pushedAt":"2024-06-09T09:40:13.000Z","pushType":"pr_merge","commitsCount":6,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://github.com/avatars/u/1202327?s=80&v=4"},"commit":{"message":"Merge pull request #608 from ppedrot/enforce-more-static-typing\n\nEnforce more static typing","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2341247484\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/608\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/608/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/608\">#608</a> from ppedrot/enforce-more-static-typing"}},{"before":"9a8afc2bcc8a325ecbb35de456af5ff93f3cffe3","after":"cb55e63700b511083d71b9e09a0e05b83ba15aea","ref":"refs/heads/main","pushedAt":"2024-06-07T13:51:03.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://github.com/avatars/u/1202327?s=80&v=4"},"commit":{"message":"Merge pull request #607 from ppedrot/untuplify-context-map\n\nTurn context_map into a record.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2340501023\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/607\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/607/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/607\">#607</a> from ppedrot/untuplify-context-map"}},{"before":"a8d8f443376b54c2bfe66563ab49fde56bfff607","after":"9a8afc2bcc8a325ecbb35de456af5ff93f3cffe3","ref":"refs/heads/main","pushedAt":"2024-06-06T09:13:59.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://github.com/avatars/u/1202327?s=80&v=4"},"commit":{"message":"Merge pull request #606 from ppedrot/enforce-static-typing\n\nRemove a good part of the sources of abusive typing","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2329398949\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/606\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/606/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/606\">#606</a> from ppedrot/enforce-static-typing"}},{"before":"abf3cdf0e74224f0f45a03c21781be3e516a2a12","after":"a8d8f443376b54c2bfe66563ab49fde56bfff607","ref":"refs/heads/main","pushedAt":"2024-06-01T13:35:03.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://github.com/avatars/u/1202327?s=80&v=4"},"commit":{"message":"Merge pull request #605 from ppedrot/conversion-no-inner-exception-api\n\nAdapt w.r.t. coq/coq#19120.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2329147064\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/605\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/605/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/605\">#605</a> from ppedrot/conversion-no-inner-exception-api"}},{"before":null,"after":"bdf39fff47346a9006cd87c778d3fc91d8c7d528","ref":"refs/heads/origin/universes-clauses","pushedAt":"2024-05-29T07:25:56.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Adapt to PR#18903","shortMessageHtmlLink":"Adapt to PR#18903"}},{"before":"fec3cbb7be4136446d5d0c5f6bb869bf206eae5b","after":"abf3cdf0e74224f0f45a03c21781be3e516a2a12","ref":"refs/heads/main","pushedAt":"2024-05-28T15:41:53.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://github.com/avatars/u/1202327?s=80&v=4"},"commit":{"message":"Merge pull request #599 from herbelin/main+adapt-coq-pr18795-more-uniform-declare.ml\n\nAdapt to Coq PR #18795 (more uniform API for declare.ml)","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2305745117\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/599\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/599/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/599\">#599</a> from herbelin/main+adapt-coq-pr18795-more-uni…"}},{"before":"4817188347e04f4f5fb78c840b4086318c715315","after":"d23be2cf35634b3b60fe73e818c6e3e982f0b616","ref":"refs/heads/universes-clauses","pushedAt":"2024-05-25T09:35:10.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Adapt to PR#18903","shortMessageHtmlLink":"Adapt to PR#18903"}},{"before":"959759858cfbe82b3cf1669a3b4588f1923cd99c","after":"fec3cbb7be4136446d5d0c5f6bb869bf206eae5b","ref":"refs/heads/main","pushedAt":"2024-05-23T10:10:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Restrict the \"simp\" hint database to not unfold constants by default, for efficiency and backward compatibility.","shortMessageHtmlLink":"Restrict the \"simp\" hint database to not unfold constants by default,…"}},{"before":"ccfdcea4149e2b7a3e18248be20a05ebb3f429f5","after":null,"ref":"refs/heads/remove-below-db-use-rec_decision","pushedAt":"2024-05-22T13:37:43.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"}},{"before":"c9a9d444000b64adc6114d44859d59254f3dde76","after":"959759858cfbe82b3cf1669a3b4588f1923cd99c","ref":"refs/heads/main","pushedAt":"2024-05-22T13:37:43.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Merge pull request #602 from mattam82/remove-below-db-use-rec_decision\n\nReplace the outdated \"Below\" hint database with a `rec_decision` data…","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2308085716\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/602\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/602/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/602\">#602</a> from mattam82/remove-below-db-use-rec_decision"}},{"before":"98f94377f3341ab8f6ecce35c705baa8ab46a53e","after":null,"ref":"refs/heads/fix-funelim-add-nosimp","pushedAt":"2024-05-22T12:17:34.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"}},{"before":"f53c8cc804ea01deab9ed6faaba186a3014031de","after":"c9a9d444000b64adc6114d44859d59254f3dde76","ref":"refs/heads/main","pushedAt":"2024-05-22T12:17:33.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Merge pull request #604 from mattam82/fix-funelim-add-nosimp\n\nFix funelim and add a `funelim_nosimp` variant which does not try to …","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2310092052\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/604\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/604/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/604\">#604</a> from mattam82/fix-funelim-add-nosimp"}},{"before":"5e5f44d452d12bc5a62820bc4c1cbcf52d6d1b85","after":"98f94377f3341ab8f6ecce35c705baa8ab46a53e","ref":"refs/heads/fix-funelim-add-nosimp","pushedAt":"2024-05-22T12:06:20.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Fix funelim and add a `funelim_nosimp` variant which does not try to simplify heuristically the induction hypotheses.","shortMessageHtmlLink":"Fix funelim and add a <code>funelim_nosimp</code> variant which does not try to …"}},{"before":null,"after":"5e5f44d452d12bc5a62820bc4c1cbcf52d6d1b85","ref":"refs/heads/fix-funelim-add-nosimp","pushedAt":"2024-05-22T09:53:27.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Fix funelim and add a `funelim_nosimp` variant which does not try to simplify heuristically the induction hypotheses.","shortMessageHtmlLink":"Fix funelim and add a <code>funelim_nosimp</code> variant which does not try to …"}},{"before":"3d4839baf943abc73ee9a5317b3edc3881cb7b38","after":null,"ref":"refs/heads/revert-593-fix-simplify-opacity-and-funelim","pushedAt":"2024-05-21T15:19:46.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"}},{"before":"ab076874f490d886e90f15772592ed23c7f82dba","after":"f53c8cc804ea01deab9ed6faaba186a3014031de","ref":"refs/heads/main","pushedAt":"2024-05-21T15:19:45.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Merge pull request #603 from mattam82/revert-593-fix-simplify-opacity-and-funelim\n\nRevert \"Fix `simplify` breaking the transparency/opaque status of constants a…\"","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2308551592\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/603\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/603/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/603\">#603</a> from mattam82/revert-593-fix-simplify-opacity…"}},{"before":null,"after":"3d4839baf943abc73ee9a5317b3edc3881cb7b38","ref":"refs/heads/revert-593-fix-simplify-opacity-and-funelim","pushedAt":"2024-05-21T15:19:17.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Revert \"Fix `simplify` breaking the transparency/opaque status of constants a…\"","shortMessageHtmlLink":"Revert \"Fix <code>simplify</code> breaking the transparency/opaque status of con…"}},{"before":null,"after":"ccfdcea4149e2b7a3e18248be20a05ebb3f429f5","ref":"refs/heads/remove-below-db-use-rec_decision","pushedAt":"2024-05-21T11:36:37.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Replace the outdated \"Below\" hint database with a `rec_decision` database that tries to automatically solve recursive call obligations","shortMessageHtmlLink":"Replace the outdated \"Below\" hint database with a <code>rec_decision</code> data…"}},{"before":"efa3ddcfeaf8abe3b7d727951669781983c4f99c","after":"ab076874f490d886e90f15772592ed23c7f82dba","ref":"refs/heads/main","pushedAt":"2024-05-21T10:13:04.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"ppedrot","name":"Pierre-Marie Pédrot","path":"/ppedrot","primaryAvatarUrl":"https://github.com/avatars/u/1202327?s=80&v=4"},"commit":{"message":"Merge pull request #601 from ppedrot/centralize-assert-replacing\n\nCentralize the use of Tactics.assert_before_replacing.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2307891913\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/601\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/601/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/601\">#601</a> from ppedrot/centralize-assert-replacing"}},{"before":"a51b4f21b93dbc68c805af3eadb69cd84cf041a1","after":null,"ref":"refs/heads/fix-simplify-opacity-and-funelim","pushedAt":"2024-05-21T09:57:02.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"}},{"before":"d24e3ece4180b389d0efb016eb2dd02c770355b5","after":"efa3ddcfeaf8abe3b7d727951669781983c4f99c","ref":"refs/heads/main","pushedAt":"2024-05-21T09:57:02.000Z","pushType":"pr_merge","commitsCount":7,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Merge pull request #593 from mattam82/fix-simplify-opacity-and-funelim\n\nFix `simplify` breaking the transparency/opaque status of constants a…","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2283530612\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mattam82/Coq-Equations/issues/593\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mattam82/Coq-Equations/pull/593/hovercard\" href=\"https://github.com/mattam82/Coq-Equations/pull/593\">#593</a> from mattam82/fix-simplify-opacity-and-funelim"}},{"before":"2fab4b72eecd3816b360d4c8307f8aac500b839a","after":"a51b4f21b93dbc68c805af3eadb69cd84cf041a1","ref":"refs/heads/fix-simplify-opacity-and-funelim","pushedAt":"2024-05-21T09:50:42.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Update to latest HoTT library","shortMessageHtmlLink":"Update to latest HoTT library"}},{"before":"f9b911a135134e2a1d595dbf7cbc09fd59c02e64","after":"2fab4b72eecd3816b360d4c8307f8aac500b839a","ref":"refs/heads/fix-simplify-opacity-and-funelim","pushedAt":"2024-05-17T20:20:39.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Fix notation","shortMessageHtmlLink":"Fix notation"}},{"before":"05651e15d51cc9c8380a857cd47996dda4e74030","after":"f9b911a135134e2a1d595dbf7cbc09fd59c02e64","ref":"refs/heads/fix-simplify-opacity-and-funelim","pushedAt":"2024-05-17T20:17:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Fix notation declarations","shortMessageHtmlLink":"Fix notation declarations"}},{"before":"4c725ec0143f9e0e30dea39aedc839473a416d7b","after":"05651e15d51cc9c8380a857cd47996dda4e74030","ref":"refs/heads/fix-simplify-opacity-and-funelim","pushedAt":"2024-05-17T20:10:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mattam82","name":"Matthieu Sozeau","path":"/mattam82","primaryAvatarUrl":"https://github.com/avatars/u/98373?s=80&v=4"},"commit":{"message":"Fix the hott build","shortMessageHtmlLink":"Fix the hott build"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEpT5zTwA","startCursor":null,"endCursor":null}},"title":"Activity · mattam82/Coq-Equations"}