{"push_id":821182475,"size":22,"distinct_size":1,"ref":"refs/heads/trunk","head":"eb7da0d0a02a406c196214ec9d08384385541788","before":"84add29c036735ceacde73ea98a9a5a454a5e3a0","commits":[{"sha":"d37aab528dca587127b9f9944e1521e4fc3d9cc7","author":{"email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org","name":"Matthieu Sozeau"},"message":"Univs: add Strict Universe Declaration option (on by default)\n\nThis option disallows \"declare at first use\" semantics for universe\nvariables (in @{}), forcing the declaration of _all_ universes appearing\nin a definition when introducing it with syntax Definition/Inductive\nfoo@{i j k} .. The bound universes at the end of a definition/inductive\nmust be exactly those ones, no extras allowed currently.\nTest-suite files using the old semantics just disable the option.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/d37aab528dca587127b9f9944e1521e4fc3d9cc7"},{"sha":"8a7f111ad5ce35e183016a2a968d19f29b7622c5","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Record fields accept an optional final semicolon separator.\n\nThere is no such thing as the OPTSEP macro in Camlp4 so I had\nto expand it by hand.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/8a7f111ad5ce35e183016a2a968d19f29b7622c5"},{"sha":"27492a7674587e1a3372cd7545e056e2775c69b3","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Test for record syntax parsing.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/27492a7674587e1a3372cd7545e056e2775c69b3"},{"sha":"08a0c44e3525d1f0c7303d189e826e25c3e3d914","author":{"email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org","name":"Matthieu Sozeau"},"message":"Univs: fix FingerTree contrib.\n\nLet merge_context_set be lenient when merging the context of side\neffects of an entry from solve_by_tac.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/08a0c44e3525d1f0c7303d189e826e25c3e3d914"},{"sha":"e26b4dbedd29acbfb9cbf2320193cc68afa60cf3","author":{"email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org","name":"Matthieu Sozeau"},"message":"Fix bug #4069: f_equal regression.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/e26b4dbedd29acbfb9cbf2320193cc68afa60cf3"},{"sha":"27d4a636cb7f1fbdbced1980808a9b947405eeb5","author":{"email":"43f1ac15e1612ec31474d70389158936df20a6d4@inria.fr","name":"Guillaume Melquiond"},"message":"Remove the \"exists\" overrides from Program. (Fix bug #4360)","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/27d4a636cb7f1fbdbced1980808a9b947405eeb5"},{"sha":"ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"Goptions: new value type: optional string\n\nThese options can be set to a string value, but also unset.\nInternal data is of type string option.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1"},{"sha":"0de499ab4702708ddfae162389617869b170c7d7","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"STM: fix backtrace handling","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/0de499ab4702708ddfae162389617869b170c7d7"},{"sha":"173f07a8386bf4d3d45b49d3dc01ab047b3ad4f9","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"Future: make not-here/not-ready messages customizable","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/173f07a8386bf4d3d45b49d3dc01ab047b3ad4f9"},{"sha":"f7e9e6428842dd80549a0dcd20bf872c2dd7fa8c","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"STM: for PIDE based UIs, edit_at requires no Reach.known_state","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/f7e9e6428842dd80549a0dcd20bf872c2dd7fa8c"},{"sha":"188ab7f76459ab46e0ea139da8b4331d958c7102","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"Spawn: use each socket exclusively for writing or reading\n\nAccording to http://caml.inria.fr/mantis/view.php?id=5325\nyou can't use the same socket for both writing and reading.\nThe result is lockups (may be fixed in 4.03).","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/188ab7f76459ab46e0ea139da8b4331d958c7102"},{"sha":"27bad55f6f87af2ae3ad7921d71c02e333a853bb","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"CThread: blocking read + threads now works","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/27bad55f6f87af2ae3ad7921d71c02e333a853bb"},{"sha":"0f706b470c83a957b600496c2bca652c2cfe65e3","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"term_typing: strengthen discharging code\n\nGiven the way Lib.extract_hyps is coded if the const_hyps field\nof a constant declaration contains a named_context that does not\nhave the same order of the one in Environment.env, discharging is\nbroken (as in some section variables are not discharged).\nIf const_hyps is computed by the kernel, then the order is correct by\nconstruction.  If such list is provided by the user, the order is not\ngranted.\n\nWe now systematically sort the list of user provided section hyps.\n\nThe code of Proof using is building the named_context in the right\norder, but the API was not enforcing/checking it.  Now it does.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/0f706b470c83a957b600496c2bca652c2cfe65e3"},{"sha":"9ea8867a0fa8f2a52df102732fdc1a931c659826","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"Proof using: let-in policy, optional auto-clear, forward closure*\n\n- \"Proof using p*\" means: use p and any section var about p.\n- Simplify the grammar/parser for proof using <expression>.\n- Section variables with a body (let-in) are pulled in automatically\n  since they are safe to be used (add no extra quantification)\n- automatic clear of \"unused\" section variables made optional:\n    Set Proof Using Clear Unused.\n  since clearing section hypotheses does not \"always work\" (e.g. hint\n  databases are not really cleaned)\n- term_typing: trigger a \"suggest proof using\" message also for Let\n  theorems.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/9ea8867a0fa8f2a52df102732fdc1a931c659826"},{"sha":"4a0fd14dcae807e0e681cfc14daca978cb4a36e9","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"aux_file: export API to ease writing of a Proof Using annotator.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/4a0fd14dcae807e0e681cfc14daca978cb4a36e9"},{"sha":"479d45e679e8486c65b77f2ddfa8718c24778a75","author":{"email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr","name":"Matthieu Sozeau"},"message":"f_equal fix continued: do a refresh_universes as before.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/479d45e679e8486c65b77f2ddfa8718c24778a75"},{"sha":"33d153a01f2814c6e5486c07257667254b91fa0c","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Axioms now support the universe binding syntax.\n\nWe artificially restrict the syntax though, because it is unclear of\nwhat the semantics of several axioms in a row is, in particular about the\nresolution of remaining evars.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/33d153a01f2814c6e5486c07257667254b91fa0c"},{"sha":"d6ff0fcefa21bd2c6424627049b0f5e49ed4df12","author":{"email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr","name":"Matthieu Sozeau"},"message":"Univs: fix bug #4161.\n\nRetypecheck abstracted infered predicate to register the right\nuniverse constraints.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/d6ff0fcefa21bd2c6424627049b0f5e49ed4df12"},{"sha":"dbdef043ea143f871a3710bae36dfc45fd815835","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Allowing empty bound universe variables.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/dbdef043ea143f871a3710bae36dfc45fd815835"},{"sha":"b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc","author":{"email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr","name":"Matthieu Sozeau"},"message":"Univs: fix bug #3807\n\nAdd a flag to disallow minimization to set","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc"}]}