{"push_id":2681062298,"size":240,"distinct_size":1,"ref":"refs/heads/master+fix-7712-anomaly-bad-rec-notation-format","head":"1ec901c49dad299bd087447251717c10e7f867eb","before":"ff55bce0d25200bfee6dc9c023b704673b559f09","commits":[{"sha":"cf44127379de49770232d6956b0455f92d6d6323","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Fixing #5500 (missing test in return clause of match leading to anomaly).\n\nThis is a quick fix to check in nested pattern-matching that the\nreturn clause is typed by an arity (there was already a check when the\nreturn clause was given explicitly - in the 3rd section of\nprepare_predicate -; it was automatically typed by a sort when the\nreturn clause was coming by pattern-matching with the type constraint,\nsince the type constraint is a type; but it was not done when the\npredicate was derived from a former predicate in nested\npattern-matching).\n\nIndeed, in nested pattern-matching, we know that the return predicate\nhas the form λy1..yn.λx:I(y1,..,yn).T(y1,..,yn,x) and we know that\nT(v1,...,vn,u) : Type for the effective u:I(v1,..,vn) we are matching\non, but we don't know if T(y1,..,yn,x) is itself a sort (e.g. it can\nbe a \"match\" which reduces to a sort when instantiated with v1..vn,\nbut whose evaluation remains blocked when the y1..yn are variables).\n\nNote that in the bug report, the incorrect typing is produced by small\ninversion. In practice, we can raise the anomaly also without small\ninversion, so we fix it in the general case. See file 5500.v for\ndetails.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/cf44127379de49770232d6956b0455f92d6d6323"},{"sha":"414e4ea9f226ade9686da28ebee39cd1b93f42a6","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Fixing #5547 (typability of return predicate in nested pattern-matching).\n\nAnswering to commit about #5500: we don't know in general if the\nreturn predicate T(y1,..,yn,x) in the intermediate step of a nested\npattern-matching is a sort, but we don't even know if it is\nwell-typed: retyping is not enough, we need full typing.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/414e4ea9f226ade9686da28ebee39cd1b93f42a6"},{"sha":"f1eac254c130af383587455876b4000fe0cdf957","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Adding a fiat-parser overlay","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/f1eac254c130af383587455876b4000fe0cdf957"},{"sha":"277d5c0d56e7ba79bd338e50e15bc3c6cb62fb65","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Getting rid of some false \"collision between bound variable names\" warnings.\n\n- In a situation like \"match x with ... end\" with no \"return\" clause\n  we don't warn for the implicit \"as x\" coming from repeating \"x\"\n- In a multiple fixpoint, we don't warn for the recursive context\n  being distributed several times over the different mutual\n  components.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/277d5c0d56e7ba79bd338e50e15bc3c6cb62fb65"},{"sha":"1522b9899b669f4fdd0fc9be1963c5e96d81a13f","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Fixes #7192 (Print Assumptions does not enter implementation of submodules).\n\nWe fix it by looking manually for the implementation at each level of\nnesting rather than using the signature for the n first levels and\nlooking for the implementation only in the n+1-th level.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/1522b9899b669f4fdd0fc9be1963c5e96d81a13f"},{"sha":"46a9d3a4430dc262f78596b4030d6195194c6aee","author":{"name":"Enrico Tassi","email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr"},"message":"[coq_makefile] COQMF_WINDRIVE is empty on linux (fix #7233)","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/46a9d3a4430dc262f78596b4030d6195194c6aee"},{"sha":"8d02e52f9d3e19453a2c4d56185758cf86119564","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove unused Deque files","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/8d02e52f9d3e19453a2c4d56185758cf86119564"},{"sha":"dc14c5132d2e7578f0677ec0202308a38da0b1cd","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Fix #7214: install knows which ml files do not get compiled to cmx.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/dc14c5132d2e7578f0677ec0202308a38da0b1cd"},{"sha":"cdae19b9eeb82f979c38de0047cdb4c5c2466e0c","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Simplify the code that handles trust of side-effects in kernel typing.\n\nFor some reason the code was returning int option when only the value of\nthe integer was relevant.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/cdae19b9eeb82f979c38de0047cdb4c5c2466e0c"},{"sha":"14352537ee96958913823ad1b8865a21f0b6ad3a","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"[sphinx] Start fixing SSR chapter.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/14352537ee96958913823ad1b8865a21f0b6ad3a"},{"sha":"0e48f50f2c84bafc410097bd67fab66b10947bf3","author":{"name":"Enrico Tassi","email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr"},"message":"[ssr] some fixes to the documentation markup","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/0e48f50f2c84bafc410097bd67fab66b10947bf3"},{"sha":"efd0d33dac811c06412926445e28c2158f7ee1d3","author":{"name":"Enrico Tassi","email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr"},"message":"[ssr] index entry for \"without loss\", \"suffices\" and \"generally have\"","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/efd0d33dac811c06412926445e28c2158f7ee1d3"},{"sha":"7b5107c4cf47dfb6f4747a4cb3cb524ff2ae466f","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"[sphinx] Fix missing indices warnings.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/7b5107c4cf47dfb6f4747a4cb3cb524ff2ae466f"},{"sha":"ce9833937ea609ae83d1ff981a21291170fa86c5","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"A few additional small fixes.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/ce9833937ea609ae83d1ff981a21291170fa86c5"},{"sha":"2ee47cd259a912196b9e4a03412f5d786380d29c","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"Remove many abusive .. coqtop in SSR chapter.\n\nMany still remain.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/2ee47cd259a912196b9e4a03412f5d786380d29c"},{"sha":"22b4d8c5b410e82f4bd1a78947d26e9dd4a3a6e3","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"Workaround a weird error of .. coqtop::","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/22b4d8c5b410e82f4bd1a78947d26e9dd4a3a6e3"},{"sha":"b0dee52bfa97405adc7c0dbffa0f3558f349659e","author":{"name":"SimonBoulier","email":"64eafac2ce5ac21efb3d10c2bc0713fe3aa70f05@ens-rennes.fr"},"message":"Define rec_declaration in terms of prec_declaration.\nAnd similarly for fixpoint and cofixpoint.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/b0dee52bfa97405adc7c0dbffa0f3558f349659e"},{"sha":"140af328cd53789a9efb822406bc2d4443c1bdb9","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"Improve links to SSR tactics, and some other improvements.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/140af328cd53789a9efb822406bc2d4443c1bdb9"},{"sha":"e398b8b5dadb0cd75cd6cfb86525ccb039d75d49","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Fix #7615: Functor inlining drops universe substitution.\n\nWe store the universe context in the inlined terms and apply it to\nthe instance provided to the substitution function. Technically the\ncontext is not needed, but we use it to assert that the length of the\ninstance corresponds, just in case.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/e398b8b5dadb0cd75cd6cfb86525ccb039d75d49"},{"sha":"45e1e0dcba3101b6a9e096f18c28da899615af7f","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Fix the checker by merely adapting the data structure.\n\nUnluckily, this is completely wrong as we trust the inlined term to be\nwell-typed in some unavailable environment. To start with, the checker\nshould not even rely on substitutions as it does not trust functors,\nbut it does anyways. I have thus commented this code as a useful backdoor\nfor when Coq is used to implement the next blockchain Ponzi scheme.\n\nWe really need to sort this out though.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/45e1e0dcba3101b6a9e096f18c28da899615af7f"}]}
{"actor":{"display_login":"herbelin"}}