Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | | | | | | | | | | | | 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 | ||
| | | | | | | | | * | | | | | | | | | | | | Document Rewriting Schemes (quickly). | 2017-12-14 | ||
| | | | | | | | | * | | | | | | | | | | | | Document Record Elimination Schemes. | 2017-12-14 | ||
| | | | | | | | | * | | | | | | | | | | | | Document Asymmetric Patterns. | 2017-12-14 | ||
| | | | | | | | | * | | | | | | | | | | | | Document some omega options (missing Omega Oldstyle). | 2017-12-14 | ||
| | | | | | | | | | | | | | | | | * | | | | Circle CI: add badge to README. | 2017-12-14 | ||
| | | | | | | | | * | | | | | | | | | | | | Add doc for Set Debug RAKAM. | 2017-12-14 | ||
| | | | | | | | | * | | | | | | | | | | | | Add doc for Set Debug Cbv. | 2017-12-14 | ||
| | | | | | | | | * | | | | | | | | | | | | Add doc for Set Info/Debug Auto/Trivial/Eauto. | 2017-12-14 | ||
| | | | | | | | | * | | | | | | | | | | | | Add optindex for Set Bullet Behavior. | 2017-12-14 | ||
| | | | | | | | | * | | | | | | | | | | | | Add doc for Set Congruence Verbose | 2017-12-14 | ||
| | | | | | | | | | | | | | | | | * | | | | Circle CI: separate job to boot opam with all used packages. | 2017-12-14 | ||
| | | | | | | | | | | | | | | | | * | | | | Circle CI: remove warning jobs | 2017-12-14 | ||
| | | | | | | | | | | | | | | | | * | | | | Circle CI: cat failed test suite logs | 2017-12-14 | ||
| | | | | | | | | * | | | | | | | | | | | | Fix typo in doc optindex for Typeclass Resolution ... | 2017-12-14 | ||
| | | | | | | | | | |_|_|/ / / / / / / / | | | | | | | | | |/| | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6395: Revert [ci] Temporal workaround for checker non-backwards com... | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6388: Fix issue #6387 | 2017-12-14 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1108: [stm] Reorganize flags | 2017-12-13 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check. | 2017-12-13 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6251: [proof] Embed evar_map in RefinerError exception. | 2017-12-13 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6175: Restoring filtering of native files passed to `rm` during `ma... | 2017-12-13 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | * | | | | | | | | | | | | | | | [meta] Minor linking fix. | 2017-12-13 | ||
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | | | | [econstr] Small cleanup in `vernac/lemmas` | 2017-12-13 | ||
| | | | | | | | | | | | | | | | | * | | | | | | | | | [econstr] Add a couple of new API functions. | 2017-12-13 | ||
| | | | | | | | | | | | | | | | | * | | | | | | | | | [lib] Auxiliary functions in List + fixes. | 2017-12-13 | ||
| | | | | | | | | | | | | | | | |/ / / / / / / / / | ||||
| | | | | | | | | | | | | | | | | | | | | * | | | | Circle CI: uses dependencies between external developments. | 2017-12-13 |