{"push_id":2686027958,"size":203,"distinct_size":1,"ref":"refs/heads/ocaml+update_to_4.05","head":"278497956a91ddb681f5984b8bde363b6210cb4b","before":"9ca6470fbc6420a19a170c10e33bb4cf0b96f526","commits":[{"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/ejgallego/coq/commits/cdae19b9eeb82f979c38de0047cdb4c5c2466e0c"},{"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/ejgallego/coq/commits/b0dee52bfa97405adc7c0dbffa0f3558f349659e"},{"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/ejgallego/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/ejgallego/coq/commits/45e1e0dcba3101b6a9e096f18c28da899615af7f"},{"sha":"2369b095a38f08e7c28e8a5dc2591476986e89c0","author":{"name":"Clément Pit-Claudel","email":"29eb7083085630ded4c2f914c70334cd49eb7bb3@live.com"},"message":"[doc] Disable smartquotes conversion\n\nCloses GH-7742.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/2369b095a38f08e7c28e8a5dc2591476986e89c0"},{"sha":"c15880e6fe79f1d746f47deb22549518f1333c8a","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Existing Class noop when already a class + warning.\n\nFix #5012.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/c15880e6fe79f1d746f47deb22549518f1333c8a"},{"sha":"a070ba052dd097f6fdb433e8f74b8bdd90d3d7c4","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"[merge script] Check if the CI that was run is outdated.\n\n[ci skip]","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/a070ba052dd097f6fdb433e8f74b8bdd90d3d7c4"},{"sha":"a6d137969a2ddf44f2a51b3465dc62584ca1c026","author":{"name":"Maxime Dénès","email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr"},"message":"[native_compute] Delay computations with toplevel match\n\nThis is an easy improvement on examples like:\n\nFixpoint zero (n : nat) :=\n  match n with\n  | O => O\n  | S p => zero p + zero p\n  end.\n\nDefinition foo := if true then zero 100 else 0.\n\nEval native_compute in if true then 0 else foo.\n\nI didn't add a test case, because our current testing infrastructure is too\nfragile for that.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/a6d137969a2ddf44f2a51b3465dc62584ca1c026"},{"sha":"ec741e8bb1bdf69f0be4bb6b594560af57f8811c","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[build] Fix checks and notes noting 4.02.1 instead of 4.02.3\n\nBumping to 4.02.3 was decided some time ago in the WG, however a\ncouple of places escaped updating.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/ec741e8bb1bdf69f0be4bb6b594560af57f8811c"},{"sha":"0daa84151fbd7d6e2646a76b7ff0e6c4fce3bdca","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Simplify the cooking of primitive projections.\n\nThere is no need to expand a primitive projection with the section\nparameters and universes, for one good reason: they are never applied\nneither to parameters nor universe instances.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/0daa84151fbd7d6e2646a76b7ff0e6c4fce3bdca"},{"sha":"0ec228dba23e24465e92f874f7d841a4bcaa3fbb","author":{"name":"whitequark","email":"b4701ebf9366004900e8211cdb469ccf92f5074c@whitequark.org"},"message":"doc: fix typo.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/0ec228dba23e24465e92f874f7d841a4bcaa3fbb"},{"sha":"e0a0159d7219a3d7e81f46001dcb2fdf1b466f8f","author":{"name":"Matthieu Sozeau","email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org"},"message":"[vernac] Add option to force building really mutual induction schemes\n\nCurrently, if one of the inductives is non recursive, it defaults to a\ncase analysis schems taking fewer predicates and methods just for that\ninductive. This irregularity prevents doing a combined scheme afterwards\nto gather all eliminators into one, as combined scheme expects all the\neliminators to have the same predicates and methods. I have a use case\nin building function graphs in Equations where some of the inductives\nmight not be recursive but I expect many other use cases could exist.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/e0a0159d7219a3d7e81f46001dcb2fdf1b466f8f"},{"sha":"2a239725f493e643d0f26455293e6ca295f4dc92","author":{"name":"Cyprien Mangin","email":"4a8224c8b25d9efb39cff9eccc753acf1b1de4ff@m4x.org"},"message":"Workaround to handle non-value arguments in tactics.\n\nAlthough the fix is not a proper one, it seems to solve\nevery instance of #2800 that could be tested.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/2a239725f493e643d0f26455293e6ca295f4dc92"},{"sha":"0419c41d8338c622a7b17dd055dfcc701c65739a","author":{"name":"Matthieu Sozeau","email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr"},"message":"cArray: proper invalid_arg exceptions","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/0419c41d8338c622a7b17dd055dfcc701c65739a"},{"sha":"994f869496b3edd76a903cac16b13e8b6f247d63","author":{"name":"Matthieu Sozeau","email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org"},"message":"evd/evarutil: safe [add_unification_pb] interface, taking EConstr's\n\nAvoid adding the same unification problem twice, module evar instantiation.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/994f869496b3edd76a903cac16b13e8b6f247d63"},{"sha":"8ab4f8f76958d2603858ad3e4073be61ad38d113","author":{"name":"Matthieu Sozeau","email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org"},"message":"evd: restrict_evar with candidates, can raise NoCandidatesLeft\n\nWhen restricting an evar with candidates, raise an exception if this\nrestriction would leave the evar without candidates, i.e. unsolvable.\n\n- evarutil: mark restricted evars as \"cleared\"\n\nThey would otherwise escape being catched by the [advance] function\nof clenv, and result in dangling evars not being registered to the shelf.\n\n- engine: restrict_evar marks it cleared, update the future goals\n\nWe make the new evar a future goal and remove the old one.\nIf we did nothing, [unshelve tac] would work correctly as it\nuses [Proofview.advance] to find the shelved goals, going through\nthe cleared evar. But [Unshelve] would fail as it expects only\nundefined evars on the shelf and throws away the defined ones.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/8ab4f8f76958d2603858ad3e4073be61ad38d113"},{"sha":"8d8200d4bff3ffc44efc51ad44dccee9eb14ec6a","author":{"name":"Matthieu Sozeau","email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org"},"message":"Do not allow spliting in res_pf, this is reserved for pretyping","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/8d8200d4bff3ffc44efc51ad44dccee9eb14ec6a"},{"sha":"b75eba7b7e2b80ca59ff94397ee28fa951c173a9","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Very first try at listing the critical bugs of the history of Coq.\n\nI let open several questions about fixes to the kernel which maybe\nwere not critical.\n\nI skipped what seemed to have been bugs in beta-releases.\n\nNeed double-checks, decision about the format, etc.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/b75eba7b7e2b80ca59ff94397ee28fa951c173a9"},{"sha":"f2e2d1d9f00ab731bd2bbe1dd57d685ac5024204","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Merge PR #7813: Workaround for #2800: handling non-value arguments in tactics.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/f2e2d1d9f00ab731bd2bbe1dd57d685ac5024204"},{"sha":"e82e8e216c4955db58255062fb5c61c7b2aa3c2a","author":{"name":"Matthieu Sozeau","email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr"},"message":"Better elaboration of pattern-matchings on primitive projections\n\nThis ensures that computations are shared as much as possible, mimicking\nthe \"positive\" records computational behavior if possible.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/e82e8e216c4955db58255062fb5c61c7b2aa3c2a"}]}
{"actor":{"display_login":"ejgallego"}}