| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | [make] More build fixes for static plugins and ocamlfind. |  Emilio Jesus Gallego Arias | 2017-12-16 |
| * | 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 | 2017-12-15 |
| | |_|/ / |/| | | | |||
| | | * | | 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 | 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 sa... | Maxime Dénès | 2017-12-14 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume... | Maxime Dénès | 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 com... | Maxime Dénès | 2017-12-14 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6388: Fix issue #6387 | Maxime Dénès | 2017-12-14 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | 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 `ma... | Maxime Dénès | 2017-12-13 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | * | | | | | | [meta] Minor linking fix. | Emilio Jesus Gallego Arias | 2017-12-13 |
| | |_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | * | [econstr] Cleanup in `vernac/classes.ml`. | Emilio Jesus Gallego Arias | 2017-12-13 |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | | | | Documenting the new options for printing "match". |  Hugo Herbelin | 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 | 2017-12-12 |
| | | | | | | | | | | * | | | | | | Removing cumbersome location in multiple patterns. | Hugo Herbelin | 2017-12-12 |
| | | | | | | | | | | * | | | | | | Improving spacing in printing disjunctive patterns. | Hugo Herbelin | 2017-12-12 |
| | | | | | | * | | | | | | | | | | Revert "[ci] Temporal workaround for checker non-backwards compatible change." | Théo Zimmermann | 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 | 2017-12-12 |
| | |_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | | | Merge PR #6359: Remove most uses of function extensionality in Program.Combin... | Maxime Dénès | 2017-12-12 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6275: [summary] Allow typed projections from global state. | Maxime Dénès | 2017-12-12 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | * | | | | Use msg_info for LtacProf |  Jason Gross | 2017-12-11 |
| | | | | | | | | | | | | | * | | | | Allow LtacProf tactics to be called | Jason Gross | 2017-12-11 |
| * | | | | | | | | | | | | | | | | | Merge PR #6312: [configure] fix detection of `md5sum` | Maxime Dénès | 2017-12-11 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |