| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-22 | Add printers to dev/db | Gaëtan Gilbert | |
| 2017-12-22 | Reorder dev/db | Gaëtan Gilbert | |
| 2017-12-22 | Cleanup top_printers.mli | Gaëtan Gilbert | |
| 2017-12-22 | Cleanup debug printers a bit, add generated mli. | Gaëtan Gilbert | |
| 2017-12-15 | Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml` | Maxime Dénès | |
| 2017-12-15 | Merge PR #6431: Compatibility of the Coq macOS package with OS X 10.11. | Maxime Dénès | |
| 2017-12-15 | Merge PR #6219: Document undocumented options | Maxime Dénès | |
| 2017-12-15 | Merge PR #6429: 8.7.1 CHANGES. | Maxime Dénès | |
| 2017-12-15 | Compatibility of the Coq macOS package with OS X 10.11. | Théo Zimmermann | |
| Travis has moved on to macOS 10.12 but this makes the package incompatible with earlier versions. This fix should restore the compatibility with OS X 10.11. | |||
| 2017-12-14 | Deprecate dead option Match Strict (ssr). | Gaëtan Gilbert | |
| 2017-12-14 | Deprecate dead code option Congruence Depth. | Gaëtan Gilbert | |
| 2017-12-14 | Merge PR #6386: Catch errors while coercing 'and' intro patterns | Maxime Dénès | |
| 2017-12-14 | Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match ↵ | Maxime Dénès | |
| (fix #6106) | |||
| 2017-12-14 | Merge PR #6379: Fix profiling plugin | Maxime Dénès | |
| 2017-12-14 | Merge PR #6422: [meta] Minor linking fix. | Maxime Dénès | |
| 2017-12-14 | Merge PR #6264: [kernel] Patch allowing to disable VM reduction. | Maxime Dénès | |
| 2017-12-14 | Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵ | Maxime Dénès | |
| same right-hand side. | |||
| 2017-12-14 | Merge PR #6373: Further clean-up in Reductionops, removing unused lift ↵ | Maxime Dénès | |
| arguments. | |||
| 2017-12-14 | Merge PR #6169: Clean up/deprecated options | Maxime Dénès | |
| 2017-12-14 | 8.7.1 CHANGES. | Théo Zimmermann | |
| 2017-12-14 | Document Short Module Printing. | Gaëtan Gilbert | |
| 2017-12-14 | Document Rewriting Schemes (quickly). | Gaëtan Gilbert | |
| 2017-12-14 | Document Record Elimination Schemes. | Gaëtan Gilbert | |
| 2017-12-14 | Document Asymmetric Patterns. | Gaëtan Gilbert | |
| 2017-12-14 | Document some omega options (missing Omega Oldstyle). | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Debug RAKAM. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Debug Cbv. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Info/Debug Auto/Trivial/Eauto. | Gaëtan Gilbert | |
| 2017-12-14 | Add optindex for Set Bullet Behavior. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Congruence Verbose | Gaëtan Gilbert | |
| 2017-12-14 | Fix typo in doc optindex for Typeclass Resolution ... | Gaëtan Gilbert | |
| 2017-12-14 | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | Maxime Dénès | |
| 2017-12-14 | Merge PR #6395: Revert [ci] Temporal workaround for checker non-backwards ↵ | Maxime Dénès | |
| compatible change. | |||
| 2017-12-14 | Merge PR #6388: Fix issue #6387 | Maxime Dénès | |
| 2017-12-13 | Merge PR #1108: [stm] Reorganize flags | Maxime Dénès | |
| 2017-12-13 | Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check. | Maxime Dénès | |
| 2017-12-13 | Merge PR #6251: [proof] Embed evar_map in RefinerError exception. | Maxime Dénès | |
| 2017-12-13 | Merge PR #6175: Restoring filtering of native files passed to `rm` during ↵ | Maxime Dénès | |
| `make clean`. | |||
| 2017-12-13 | [meta] Minor linking fix. | Emilio Jesus Gallego Arias | |
| 2017-12-13 | [econstr] Cleanup in `vernac/classes.ml`. | Emilio Jesus Gallego Arias | |
| We fix quite a few types, and perform some cleanup wrt to the evar_map, in particular we prefer to thread it now as otherwise it may become trickier to check when we are using the correct one. Thanks to @SkySkimmer for lots of comments and bug-finding. | |||
| 2017-12-12 | Documenting the new options for printing "match". | Hugo Herbelin | |
| Namely: - Set Printing Factorizable Match Patterns. = Set Printing Allow Default Clause. | |||
| 2017-12-12 | Decompiling pattern-matching: mini-removal dead code. | Hugo Herbelin | |
| 2017-12-12 | In printing, factorizing "match" clauses with same right-hand side. | Hugo Herbelin | |
| Moreover, when there are at least two clauses and the last most factorizable one is a disjunction with no variables, turn it into a catch-all clause. Adding options Unset Printing Allow Default Clause. to deactivate the second behavior, and Unset Printing Factorizable Match Patterns. to deactivate the first behavior (deactivating the first one deactivates also the second one). E.g. printing match x with Eq => 1 | _ => 0 end gives match x with | Eq => 1 | _ => 0 end or (with default clause deactivates): match x with | Eq => 1 | Lt | Gt => 0 end More to be done, e.g. reconstructing multiple patterns in Nat.eqb... | |||
| 2017-12-12 | Removing cumbersome location in multiple patterns. | Hugo Herbelin | |
| This is to have a better symmetry between CCases and GCases. | |||
| 2017-12-12 | Improving spacing in printing disjunctive patterns. | Hugo Herbelin | |
| Adding a space before the bar separating disjunctive patterns. Removing an extra space after the bar for inner disjunctive patterns. | |||
| 2017-12-12 | Revert "[ci] Temporal workaround for checker non-backwards compatible change." | Théo Zimmermann | |
| This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f. | |||
| 2017-12-12 | Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_facts | Maxime Dénès | |
| 2017-12-12 | Further clean-up in Reductionops, removing unused lift arguments. | Maxime Dénès | |
| This is a follow-up on 866b449c497933a3ab1185c194d8d33a86c432f2. | |||
| 2017-12-12 | Merge PR #6359: Remove most uses of function extensionality in ↵ | Maxime Dénès | |
| Program.Combinators | |||
| 2017-12-12 | Merge PR #6275: [summary] Allow typed projections from global state. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |