Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Archive the `gallina` tool | 2018-06-25 | |
* | Merge PR #7559: Existing Class noop when already a class + warning. | 2018-06-25 | |
|\ | |||
* \ | Merge PR #7620: [ssr] rewrite: turn anomaly into regular error | 2018-06-25 | |
|\ \ | |||
* \ \ | Merge PR #7895: Revert "Add a note about [ci skip] in CI README." | 2018-06-24 | |
|\ \ \ | |||
* \ \ \ | Merge PR #7805: Towards listing the critical bugs of the history of Coq. | 2018-06-24 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7772: [native_compute] Delay computations with toplevel match | 2018-06-24 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #7784: Remove Tutorials from a few other places following #7466. | 2018-06-24 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #7614: Simplify the code that handles trust of side-effects in kerne... | 2018-06-23 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #7236: [ssr] simpler semantics for delayed clears | 2018-06-23 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #7827: [engine] safe [add_unification_pb] interface | 2018-06-23 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #7750: Handle mutual records in the kernel | 2018-06-23 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | Adapt the kernel to generate proper data for mutual records. | 2018-06-23 | |
| * | | | | | | | | | | Using more general information for primitive records. | 2018-06-23 | |
| * | | | | | | | | | | Change the proj_ind field from MutInd.t to inductive. | 2018-06-23 | |
|/ / / / / / / / / / | |||
* | | | | | | | | | | Merge PR #7715: Simplify the cooking of primitive projections. | 2018-06-23 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function. | 2018-06-22 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7893: Update dpdgraph branch name | 2018-06-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7776: [ssr] Fix rewrite with universes | 2018-06-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | * | | | | | | | | [ssr] document {}/view | 2018-06-22 | |
| | | | | | * | | | | | | | | [ssr] document rewrite {}foo | 2018-06-22 | |
| | | | | | * | | | | | | | | [ssr] implement {}/v as a short hand for {v}/v when v is an id | 2018-06-22 | |
| | | | | | * | | | | | | | | [ssr] simplify delayed clears | 2018-06-22 | |
| |_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | |||
| * | | | | | | | | | | | | [ssr] test case for rewrite and set on univ poly keys | 2018-06-22 | |
| * | | | | | | | | | | | | [ssr] matching: use eq_constr_nounivs in approximated matching | 2018-06-22 | |
| * | | | | | | | | | | | | [ssr] set: merge universe constraints before type checking the term | 2018-06-22 | |
|/ / / / / / / / / / / / | |||
| | | | | | | | | * / / | Revert "Add a note about [ci skip] in CI README." | 2018-06-22 | |
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | |||
* | | | | | | | | | | | Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3 | 2018-06-21 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7873: Make Clément the secondary codeowner of doc/tools/coqrst. | 2018-06-21 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | | | Update dpdgraph branch name | 2018-06-21 | |
* | | | | | | | | | | | | | Merge PR #7770: Move indices on top on the TOC. Closes #7764. | 2018-06-21 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | |||
* | | | | | | | | | | | | | Merge PR #7815: On cygwin, pass the filename in a format that coqdoc understa... | 2018-06-21 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter. | 2018-06-21 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7842: Fix #7836: tools/inferior-coq.el uses next-line instead of fo... | 2018-06-21 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7880: Clean up Dyn | 2018-06-21 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | | | | | | | Add documentation for Dyn. | 2018-06-21 | |
| * | | | | | | | | | | | | | | | | Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose. | 2018-06-21 | |
| * | | | | | | | | | | | | | | | | Reformat Dyn.{ml,mli}. | 2018-06-21 | |
|/ / / / / / / / / / / / / / / / | |||
| | | * | | | | | | | | | | | | | On cygwin, pass the filename in a format that coqdoc understands. | 2018-06-20 | |
* | | | | | | | | | | | | | | | | Merge PR #7868: [coqtop] Give priority to stdlib load path over current direc... | 2018-06-20 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | | * | | [ssr] test case for rewrite (setoid) making the goal illtyped | 2018-06-20 | |
| | | | | | | | | | | | | | | * | | [ssr] rewrite: turn anomaly into regular error | 2018-06-20 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | |||
| | | | | | * | | | | | | | | | | Make Clément the secondary codeowner of doc/tools/coqrst. | 2018-06-20 | |
| |_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | | [coqtop] Give priority to stdlib load path over current directory | 2018-06-19 | |
* | | | | | | | | | | | | | | | Merge PR #7797: Remove reference name type. | 2018-06-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6754: Better elaboration of pattern-matchings on primitive projections | 2018-06-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7491: Fix #7421: constr_eq ignores universe constraints. | 2018-06-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7801: [vernac] Add option to force building really mutual induction... | 2018-06-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7841: Remove Canary | 2018-06-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | |||
| | | | | | | * | | | | | | | | | | | | [doc] Rewrite and document the prodn directive | 2018-06-19 | |
| | | | | | | * | | | | | | | | | | | | [doc] Fix a typo in the ssreflect chapter | 2018-06-19 |