| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Change OCAMLRUNPARAM warning to mention OCaml 4.06 |  Paul Steckler | 2017-11-13 |
| | | |||
| * | Merge PR #6098: [api] Move structures deprecated in the API to the core. |  Maxime Dénès | 2017-11-13 |
| |\ | |||
| * \ | Merge PR #6136: Update and simplify README. | Maxime Dénès | 2017-11-13 |
| |\ \ | |||
| * \ \ | Merge PR #6126: Fix ci-bignums.sh "missing ]" error. | Maxime Dénès | 2017-11-13 |
| |\ \ \ | |||
| * \ \ \ | Merge PR #6124: Adding a debugging printer for ident maps whose codomain ↵ | Maxime Dénès | 2017-11-13 |
| |\ \ \ \ | | | | | | | | | | | | | | | | type is unknown | ||
| * \ \ \ \ | Merge PR #6117: Fix printing anomaly in conv | Maxime Dénès | 2017-11-13 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge PR #6103: Hack to restore printing of glob_constr in debugger. | Maxime Dénès | 2017-11-13 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #6088: Remove packaging scripts while waiting for a fix to #5998. | Maxime Dénès | 2017-11-13 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6071: [ci] Add Ltac2 | Maxime Dénès | 2017-11-13 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #6065: [api] Deprecate all legacy uses of Names in core. | Maxime Dénès | 2017-11-13 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6052: [general] Move Tactypes to `interp` + API reordering. | Maxime Dénès | 2017-11-13 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac. | Maxime Dénès | 2017-11-13 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | * | | Update and simplify README. |  Théo Zimmermann | 2017-11-10 |
| | |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | |||
| | | | | | | | | | * | | Fix ci-bignums.sh "missing ]" error. |  Gaëtan Gilbert | 2017-11-09 |
| | |_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It made the test always fail so ci-common was always sourced. It's not quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure. | ||
| | | | | | | | | * | | Adding a debugging printer for ident maps whose codomain type is unknown. |  Hugo Herbelin | 2017-11-08 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Actually, ocaml is apparently doing well. If there is a printer for 'a Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined existing ones, so, it is apparently not a problem to have overlapping printer. | ||
| * | | | | | | | | | | Merge PR #6100: [api] Remove 8.7 ML-deprecated functions. | Maxime Dénès | 2017-11-08 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6096: Documentation: "tac1 || tac2" means "first [ progress tac1 | ↵ | Maxime Dénès | 2017-11-08 |
| |\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | tac2 ]" | ||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6087: [feedback] Helper to print feedback messages in the console. | Maxime Dénès | 2017-11-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6086: [ci] Switch VST back to upstream. | Maxime Dénès | 2017-11-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #922: New beta-iota compatibility refinements | Maxime Dénès | 2017-11-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | | Fixing missing separator in an error message. | Hugo Herbelin | 2017-11-08 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The message is the "Conversion test raised an anomaly" one. | ||
| | | | | | | | | | | | | * | | Fixing an (apparently misplaced) spc in anomaly reporting message. | Hugo Herbelin | 2017-11-08 |
| | |_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | |||
| | | | | | | | | | | | * | | Hack to restore printing of glob_constr in debugger. | Hugo Herbelin | 2017-11-07 |
| | |_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | |||
| | | | | | * | | | | | | | [api] Remove 8.7 ML-deprecated functions. |  Emilio Jesus Gallego Arias | 2017-11-07 |
| | |_|_|_|/ / / / / / / |/| | | | | | | | | | | |||
| | | | | | | | | | | * | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | 2017-11-06 |
| | | | | | | | | |_|/ | | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | We do up to `Term` which is the main bulk of the changes. | ||
| | | | | | | | * | | | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias | 2017-11-06 |
| | |_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | This will allow to merge back `Names` with `API.Names` | ||
| * | | | | | | | | | Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core. | Maxime Dénès | 2017-11-06 |
| |\ \ \ \ \ \ \ \ \ | |||
| | | | | | * | | | | | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]", |  Samuel Gruetter | 2017-11-06 |
| | |_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | not "first [ progress tac1 | progress tac2 ]". And add a missing backslash. | ||
| | | | | | | | | * | Remove packaging scripts while waiting for a fix to #5998. | Théo Zimmermann | 2017-11-06 |
| | |_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | This is a temporary commit which should be reverted once the issue is fixed. | ||
| | | | | * | | | | [feedback] Helper to print feedback messages in the console. | Emilio Jesus Gallego Arias | 2017-11-06 |
| | |_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | This is useful for tools such as `coqchk` or `coq_makefile` that want to handle feedback on their own. | ||
| * | | | | | | | Merge PR #6072: Protecting evar map printer | Maxime Dénès | 2017-11-06 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to ↵ | Maxime Dénès | 2017-11-06 |
| |\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | alphabet). | ||
| * \ \ \ \ \ \ \ \ | Merge PR #6085: Update .mailmap with a jkloos alias | Maxime Dénès | 2017-11-06 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6063: Finish removing Show Goal uid | Maxime Dénès | 2017-11-06 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ↵ | Maxime Dénès | 2017-11-06 |
| |\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | rules | ||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1139: Add a linter. | Maxime Dénès | 2017-11-06 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | | | | | Update .mailmap with a jkloos alias |  Jason Gross | 2017-11-05 |
| | |_|_|/ / / / / / / / / |/| | | | | | | | | | | | |||
| | | | | * | | | | | | | | Refining PR#924 (insensitivity of projection heuristics to alphabet). | Hugo Herbelin | 2017-11-05 |
| | |_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed). | ||
| | | | | * | | | | | | | Cosmetic changes in evar_map printer. | Hugo Herbelin | 2017-11-05 |
| | | | | | | | | | | | | |||
| | | | | * | | | | | | | Preventively protect locally against failures of evar_map printer. | Hugo Herbelin | 2017-11-05 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It is not clear that this is really needed, but in case it happens, one will at least have a partial result available rather than an unexploitable global failure of the parser. | ||
| | | | | * | | | | | | | Fixing a cause of failure of evar_map printer in debugger. | Hugo Herbelin | 2017-11-05 |
| | |_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Indeed, the debugger debugs coqtop but it is itself just an ocaml runtime extended with the coq printers. It does not know the environment, so, looking in the Global.env() for the printers can only fail. | ||
| | | | | | | | | | * | [ci] Add Ltac2 | Jason Gross | 2017-11-04 |
| | |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||
| | | | | * | | | | | [api] Deprecate all legacy uses of Name.Id in core. | Emilio Jesus Gallego Arias | 2017-11-04 |
| | |_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | This is a first step towards some of the solutions proposed in #6008. | ||
| | | | * | | | | | Finish removing Show Goal uid | Gaëtan Gilbert | 2017-11-04 |
| | |_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6 | ||
| | | | | | * | | Adding support for syntax "let _ := e in e'" in Ltac. | Hugo Herbelin | 2017-11-04 |
| | |_|_|_|/ / |/| | | | | | | | | | | | | | | | | | Adding a file fixing #5996 and which uses this feature. | ||
| * | | | | | | Merge PR #6060: Improve error message and fix #6055 (spelling mistake). | Maxime Dénès | 2017-11-03 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available. | Maxime Dénès | 2017-11-03 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6047: A generic printer for ltac values | Maxime Dénès | 2017-11-03 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵ | Maxime Dénès | 2017-11-03 |
| |\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | variables). | ||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6036: [toplevel] Export the last document seen after `Drop`. | Maxime Dénès | 2017-11-03 |
| |\ \ \ \ \ \ \ \ \ \ | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |