{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":546038076,"defaultBranch":"coq-8.19","name":"logrel-coq","ownerLogin":"CoqHott","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2022-10-05T12:17:36.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/16703934?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1710354508.0","currentOid":""},"activityList":{"items":[{"before":"fdd1064b3e2668ff981057aedbc2f9c605beb1c0","after":"4cf01dc06cd8dc60e4b7786b030f9ed9715fb181","ref":"refs/heads/untyped-algo","pushedAt":"2024-09-24T12:41:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"full negative soundness!","shortMessageHtmlLink":"full negative soundness!"}},{"before":"11b3eb9c768f562a87b03698ac3a4b5e12c27679","after":"fdd1064b3e2668ff981057aedbc2f9c605beb1c0","ref":"refs/heads/untyped-algo","pushedAt":"2024-09-23T18:11:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"declarative neutral conversion","shortMessageHtmlLink":"declarative neutral conversion"}},{"before":"afb09ec984e7190246c6fb64e67db73555b8fb5f","after":"11b3eb9c768f562a87b03698ac3a4b5e12c27679","ref":"refs/heads/untyped-algo","pushedAt":"2024-09-18T17:02:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"filling in the id head mismatches","shortMessageHtmlLink":"filling in the id head mismatches"}},{"before":"b58022fab84ae05cbf008ea1360803b34b5fb8bd","after":"afb09ec984e7190246c6fb64e67db73555b8fb5f","ref":"refs/heads/untyped-algo","pushedAt":"2024-09-06T13:37:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"injectivity of universe constructors\n\nthat escape at level zero is a terrible hack :(","shortMessageHtmlLink":"injectivity of universe constructors"}},{"before":"00983d6720f0667fe87351cdd9a7da008015368d","after":"b58022fab84ae05cbf008ea1360803b34b5fb8bd","ref":"refs/heads/untyped-algo","pushedAt":"2024-09-04T19:23:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"first jab at negative soundness\n\nmissing neutral cases + unproven injectivities in the universe","shortMessageHtmlLink":"first jab at negative soundness"}},{"before":"7d3b7ba5ccade55316fb8c7f8d2668cab2a7f692","after":"00983d6720f0667fe87351cdd9a7da008015368d","ref":"refs/heads/untyped-algo","pushedAt":"2024-07-10T17:32:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"QED","shortMessageHtmlLink":"QED"}},{"before":"7eb40e746d0b49069ff226d5510709688ee3eeb1","after":"7d3b7ba5ccade55316fb8c7f8d2668cab2a7f692","ref":"refs/heads/untyped-algo","pushedAt":"2024-07-08T16:46:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"untyped termination\n\nadmitted lemma for strengthening – for now","shortMessageHtmlLink":"untyped termination"}},{"before":"3921321036f65c851a8317c5830eefb7b87960eb","after":"7eb40e746d0b49069ff226d5510709688ee3eeb1","ref":"refs/heads/untyped-algo","pushedAt":"2024-07-01T17:21:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"completeness","shortMessageHtmlLink":"completeness"}},{"before":"1dcdadd6c773ae011d7105e664958528aaae4bc6","after":"3921321036f65c851a8317c5830eefb7b87960eb","ref":"refs/heads/untyped-algo","pushedAt":"2024-06-28T13:28:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"updated algo conversion","shortMessageHtmlLink":"updated algo conversion"}},{"before":"8246811f52bb28530db1a81b1abc3aecf1781a27","after":"1dcdadd6c773ae011d7105e664958528aaae4bc6","ref":"refs/heads/untyped-algo","pushedAt":"2024-06-27T12:10:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"finalise the move of typed conversion","shortMessageHtmlLink":"finalise the move of typed conversion"}},{"before":"90004a2d3ef488cff40447162449ce789ff6feae","after":"8246811f52bb28530db1a81b1abc3aecf1781a27","ref":"refs/heads/untyped-algo","pushedAt":"2024-06-26T14:52:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"finish new lemmas + clean-up until completeness","shortMessageHtmlLink":"finish new lemmas + clean-up until completeness"}},{"before":"b945fed94649b3ba8ddfa9ad758f4ce2b9d1af17","after":"90004a2d3ef488cff40447162449ce789ff6feae","ref":"refs/heads/untyped-algo","pushedAt":"2024-06-25T17:13:21.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"moving to the new lemmas – type and neutral conversion","shortMessageHtmlLink":"moving to the new lemmas – type and neutral conversion"}},{"before":"3863962f91bfae59f36b5e8733131aeb5ab1651e","after":"17bf5ddef2a7ac7ed8473f73aa6b470396ee5803","ref":"refs/heads/parallel-red","pushedAt":"2024-06-11T06:55:58.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"more WIP","shortMessageHtmlLink":"more WIP"}},{"before":"a2bf20c9bfc7fcea9627bb34883922e8edb34a8d","after":"3863962f91bfae59f36b5e8733131aeb5ab1651e","ref":"refs/heads/parallel-red","pushedAt":"2024-06-11T06:51:26.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"more WIP","shortMessageHtmlLink":"more WIP"}},{"before":"39214eccae9a0e4ec398853703d4cb3c755bab9c","after":"a2bf20c9bfc7fcea9627bb34883922e8edb34a8d","ref":"refs/heads/parallel-red","pushedAt":"2024-03-15T10:48:32.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"definition of parallel reduction","shortMessageHtmlLink":"definition of parallel reduction"}},{"before":null,"after":"39214eccae9a0e4ec398853703d4cb3c755bab9c","ref":"refs/heads/parallel-red","pushedAt":"2024-03-13T18:28:28.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"definition of parallel reduction","shortMessageHtmlLink":"definition of parallel reduction"}},{"before":"ac4da1860eb30c02219c64d830ce1019e4956ca2","after":"b945fed94649b3ba8ddfa9ad758f4ce2b9d1af17","ref":"refs/heads/untyped-algo","pushedAt":"2024-03-08T16:33:24.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"function update","shortMessageHtmlLink":"function update"}},{"before":"cffedd1d7d0b9d3bd66d84de70f0ae07221b9ac0","after":"ac4da1860eb30c02219c64d830ce1019e4956ca2","ref":"refs/heads/untyped-algo","pushedAt":"2024-03-08T16:32:44.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"function update","shortMessageHtmlLink":"function update"}},{"before":"8c2c6cbad2b3ec5cb26576202c0a987a80fccb39","after":"cffedd1d7d0b9d3bd66d84de70f0ae07221b9ac0","ref":"refs/heads/untyped-algo","pushedAt":"2024-02-29T11:25:24.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"untyped algorithm and soundness","shortMessageHtmlLink":"untyped algorithm and soundness"}},{"before":"f8a899d675e365952c7570717384d1e7a5dc7b33","after":"8c2c6cbad2b3ec5cb26576202c0a987a80fccb39","ref":"refs/heads/untyped-algo","pushedAt":"2024-02-26T11:56:13.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MevenBertrand","name":"Meven Lennon-Bertrand","path":"/MevenBertrand","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/58942857?s=80&v=4"},"commit":{"message":"everything builds again","shortMessageHtmlLink":"everything builds again"}},{"before":"1f29c2234d65ce9680fbce3cb629d8c779893c3c","after":"dc8cba9fc0c657b5c889ae7d44302982361f8c45","ref":"refs/heads/coq-8.19","pushedAt":"2024-01-31T10:14:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"kyoDralliam","name":"Kenji Maillard","path":"/kyoDralliam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/79955?s=80&v=4"},"commit":{"message":"update checkout v3 -> v4, try to fix pages deployment","shortMessageHtmlLink":"update checkout v3 -&gt; v4, try to fix pages deployment"}},{"before":"d45166945b359522308e9f34a47990e33ee0e535","after":null,"ref":"refs/heads/master","pushedAt":"2024-01-30T10:23:14.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"kyoDralliam","name":"Kenji Maillard","path":"/kyoDralliam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/79955?s=80&v=4"}},{"before":null,"after":"d45166945b359522308e9f34a47990e33ee0e535","ref":"refs/heads/coq-8.16","pushedAt":"2024-01-30T10:23:13.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"kyoDralliam","name":"Kenji Maillard","path":"/kyoDralliam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/79955?s=80&v=4"},"commit":{"message":"Merge pull request #62 from CoqHott/better-autosubst\n\nBetter AutoSubst","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2096318360\" data-permission-text=\"Title is private\" data-url=\"https://github.com/CoqHott/logrel-coq/issues/62\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/CoqHott/logrel-coq/pull/62/hovercard\" href=\"https://github.com/CoqHott/logrel-coq/pull/62\">#62</a> from CoqHott/better-autosubst"}},{"before":"de550efcd9c74723b5c3d71cc6f7e29767b7a65d","after":"1f29c2234d65ce9680fbce3cb629d8c779893c3c","ref":"refs/heads/coq-8.19","pushedAt":"2024-01-30T10:22:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"kyoDralliam","name":"Kenji Maillard","path":"/kyoDralliam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/79955?s=80&v=4"},"commit":{"message":"change deploy pages to default branch instead of master","shortMessageHtmlLink":"change deploy pages to default branch instead of master"}},{"before":"95a405c4057756151e7040b61e1eadc79999cba6","after":"98969e42e72520530d6d1d42ed0ff1bbc62afcb1","ref":"refs/heads/DigammaTTPshfConditions","pushedAt":"2024-01-29T15:30:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Baillon-M","name":null,"path":"/Baillon-M","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/119693584?s=80&v=4"},"commit":{"message":"New notations + Monad definition","shortMessageHtmlLink":"New notations + Monad definition"}},{"before":null,"after":"de550efcd9c74723b5c3d71cc6f7e29767b7a65d","ref":"refs/heads/coq-8.19","pushedAt":"2024-01-29T10:17:17.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"kyoDralliam","name":"Kenji Maillard","path":"/kyoDralliam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/79955?s=80&v=4"},"commit":{"message":"Adapt to coq 8.19","shortMessageHtmlLink":"Adapt to coq 8.19"}},{"before":"5a6610f9fac2c60e37fdf8caae6b3f06ace91a50","after":"f4575da5733d294cf4388872549b8acab4b42598","ref":"refs/heads/coq-8.18","pushedAt":"2024-01-26T10:38:07.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"kyoDralliam","name":"Kenji Maillard","path":"/kyoDralliam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/79955?s=80&v=4"},"commit":{"message":"adapt renaming in coq-partialfun","shortMessageHtmlLink":"adapt renaming in coq-partialfun"}},{"before":"63e070e7e3f3dddc20d819d0acc769687240807d","after":"5a6610f9fac2c60e37fdf8caae6b3f06ace91a50","ref":"refs/heads/coq-8.18","pushedAt":"2024-01-25T10:46:24.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"kyoDralliam","name":"Kenji Maillard","path":"/kyoDralliam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/79955?s=80&v=4"},"commit":{"message":"update readme, opam and workflow for coq 8.18","shortMessageHtmlLink":"update readme, opam and workflow for coq 8.18"}},{"before":"d116cf723ba361c52f251b3487efbfe5d5d07452","after":null,"ref":"refs/heads/better-autosubst","pushedAt":"2024-01-25T10:26:00.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"kyoDralliam","name":"Kenji Maillard","path":"/kyoDralliam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/79955?s=80&v=4"}},{"before":"fcbc9d0317f10d1ca3cfa0090c994083a2d2bc01","after":"d45166945b359522308e9f34a47990e33ee0e535","ref":"refs/heads/master","pushedAt":"2024-01-25T10:25:59.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"kyoDralliam","name":"Kenji Maillard","path":"/kyoDralliam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/79955?s=80&v=4"},"commit":{"message":"Merge pull request #62 from CoqHott/better-autosubst\n\nBetter AutoSubst","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2096318360\" data-permission-text=\"Title is private\" data-url=\"https://github.com/CoqHott/logrel-coq/issues/62\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/CoqHott/logrel-coq/pull/62/hovercard\" href=\"https://github.com/CoqHott/logrel-coq/pull/62\">#62</a> from CoqHott/better-autosubst"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yNFQxMjo0MTozMC4wMDAwMDBazwAAAAS_IyDU","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wMS0yNVQxMDoyNTo1OS4wMDAwMDBazwAAAAPozIPR"}},"title":"Activity · CoqHott/logrel-coq"}