Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | | | | | | | Merge PR #6436: Fix #5368: Canonical structure unification fails. | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6447: [make] More build fixes for static plugins and ocamlfind. | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6284: Warning for absolute name masking (deprecated, should become ... | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6381: A version of [time] that works on constr evaluation | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6406: Make [abstract] nodes show up in the Ltac profile | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6380: Add tactics to reset and display the Ltac profile | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra... | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6305: Build with windows line endings | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | * | | | [vernac] Cleanup of do_definition. | 2017-12-18 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | Merge PR #6217: Do dependencies in 1 command per file class. | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | * | | | | | | Removing the FAQ, which has been moved to the GitHub wiki for this | 2017-12-18 | ||
* | | | | | | | | | | | | | | | | | | | Merge PR #6453: [doc] Nit on the manual. | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6419: [vernac] Split `command.ml` into separate files. | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6413: [econstr] Switch constrintern API to non-imperative style. | 2017-12-18 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | | | | | | | | | | [flags] Make program_mode a parameter for commands in vernac. | 2017-12-17 | ||
| | * | | | | | | | | | | | | | | | | | | | | | [vernac] Split `command.ml` into separate files. | 2017-12-17 | ||
| |/ / / / / / / / / / / / / / / / / / / / / | ||||
| | | * / / / / / / / / / / / / / / / / / / | [doc] Nit on the manual. | 2017-12-17 | ||
| |_|/ / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | | | | | | | | Fix build file | 2017-12-16 | ||
| | | | * | | | | | | | | | | | | | | | | | For bug 6249, Segmentation fault when building Coq on Windows 10. | 2017-12-16 | ||
| | | | | | | | | | | | | | * | | | | | | | Let definitions must not contain side-effects when reaching the kernel. | 2017-12-16 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | | | | [make] More build fixes for static plugins and ocamlfind. | 2017-12-16 | ||
| |_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | | | | [stm] [ide protocol] Allow to include several commands on query. | 2017-12-16 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | ||||
| | | * | | | | | | | | | | | | | | | Overlay for unimath. | 2017-12-15 | ||
| | | * | | | | | | | | | | | | | | | Do dependencies in 1 command per file class. | 2017-12-15 | ||
* | | | | | | | | | | | | | | | | | | Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml` | 2017-12-15 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6431: Compatibility of the Coq macOS package with OS X 10.11. | 2017-12-15 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6219: Document undocumented options | 2017-12-15 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6429: 8.7.1 CHANGES. | 2017-12-15 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | | | | | | | [econstr] Switch constrintern API to non-imperative style. | 2017-12-15 | ||
| | | | | | | | | | | | | | * | | | | | | | Fix #5368: Canonical structure unification fails. | 2017-12-15 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | ||||
| | | * | | | | | | | | | | | | | | | | | Compatibility of the Coq macOS package with OS X 10.11. | 2017-12-15 | ||
| |_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | | | Pass a ghost location for abstract | 2017-12-14 | ||
| | | | | | | | | | * | | | | | | | | | Make [abstract] nodes show up in the Ltac profile | 2017-12-14 | ||
| |_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | | Add documentation for time_constr | 2017-12-14 | ||
| | * | | | | | | | | | | | | | | | | Deprecate dead option Match Strict (ssr). | 2017-12-14 | ||
| | * | | | | | | | | | | | | | | | | Deprecate dead code option Congruence Depth. | 2017-12-14 | ||
| | | | | | | | | | * | | | | | | | | Add named timers to LtacProf | 2017-12-14 | ||
| | | | | | | | | |/ / / / / / / / | ||||
| | | | | | | | | * | | | | | | | | Add doc+changelog entries for new LtacProf tactics | 2017-12-14 | ||
| | | | | | | | | * | | | | | | | | Add tactics to reset and display the Ltac profile | 2017-12-14 | ||
| |_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | Merge PR #6386: Catch errors while coercing 'and' intro patterns | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (... | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6379: Fix profiling plugin | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6422: [meta] Minor linking fix. | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6264: [kernel] Patch allowing to disable VM reduction. | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #978: In printing, experimenting factorizing "match" clauses with sa... | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume... | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6169: Clean up/deprecated options | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | * | | | | | | | | | | | | | | | 8.7.1 CHANGES. | 2017-12-14 | ||
| |_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | | | | | | | | | Document Short Module Printing. | 2017-12-14 |