| Commit message (Expand) | Author | Age |
* | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc. | Hugo Herbelin | 2018-02-20 |
* | Change default for notations with variables bound to both terms and binders. | Hugo Herbelin | 2018-02-20 |
* | Notations: Adding modifiers to tell which kind of binder a constr can parse. | Hugo Herbelin | 2018-02-20 |
* | When printing a notation with "match", more flexibility in matching equations. | Hugo Herbelin | 2018-02-20 |
* | Adding general support for irrefutable disjunctive patterns. | Hugo Herbelin | 2018-02-20 |
* | Using an "as" clause when needed for printing irrefutable patterns. | Hugo Herbelin | 2018-02-20 |
* | Refining the strategy for glueing let-ins to a sequence of binders. | Hugo Herbelin | 2018-02-20 |
* | A (significant) simplification in printing notations with recursive binders. | Hugo Herbelin | 2018-02-20 |
* | Respecting the ident/pattern distinction in notation modifiers. | Hugo Herbelin | 2018-02-20 |
* | Adding support for parsing subterms of a notation as "pattern". | Hugo Herbelin | 2018-02-20 |
* | Adding patterns in the category of binders for notations. | Hugo Herbelin | 2018-02-20 |
* | In printing notations with "match", reasoning up to the order of clauses. | Hugo Herbelin | 2018-02-20 |
* | Supporting recursive notations reversing the left-to-right order. | Hugo Herbelin | 2018-02-20 |
* | Allowing variables used in recursive notation to occur several times in pattern. | Hugo Herbelin | 2018-02-20 |
* | Allows recursive patterns for binders to be associative on the left. | Hugo Herbelin | 2018-02-20 |
* | Fixing/improving notations with recursive patterns. | Hugo Herbelin | 2018-02-20 |
* | Using name given by user to name a 'pat, if any. | Hugo Herbelin | 2018-02-20 |
* | Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr. | Hugo Herbelin | 2018-02-20 |
* | Notations: Do not consider a non-occurring variable as a binder-only variable. | Hugo Herbelin | 2018-02-20 |
* | Adding support for re-folding notation referring to isolated "forall '(x,y), t". | Hugo Herbelin | 2018-02-20 |
* | Merge PR #6728: Extrude monomorphic universe contexts from with Definition co... | Maxime Dénès | 2018-02-19 |
|\ |
|
* | | Cleaner treatment of parameters in inferCumulativity | Gaëtan Gilbert | 2018-02-16 |
| * | Adding a test for the construction that was broken in Coccinelle. | Pierre-Marie Pédrot | 2018-02-16 |
|/ |
|
* | Merge PR #1073: new quick2vo target: like vio2vo, but smarter | Maxime Dénès | 2018-02-15 |
|\ |
|
| * | disable tests: vio2vo is broken in Windows | Ralf Jung | 2018-02-15 |
| * | also test vio2vo | Ralf Jung | 2018-02-15 |
| * | test "make quick2vo" | Ralf Jung | 2018-02-15 |
* | | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProject | Maxime Dénès | 2018-02-15 |
|\ \ |
|
| * | | coq_makefile: Support "" as the prefix in _CoqProject | Joachim Breitner | 2018-02-15 |
* | | | Merge PR #6713: Fix #6677: Critical bug with VM and universes | Maxime Dénès | 2018-02-14 |
|\ \ \ |
|
* \ \ \ | Merge PR #1082: Fixing Print for inductive types with let-in in parameters | Maxime Dénès | 2018-02-12 |
|\ \ \ \
| |_|/ /
|/| | | |
|
| | * | | Add test case for #6677. | Maxime Dénès | 2018-02-12 |
| | |/ |
|
* | | | Merge PR #1047: Support universe instances on the literal Type | Maxime Dénès | 2018-02-12 |
|\ \ \ |
|
* \ \ \ | Merge PR #6128: Simplification: cumulativity information is variance informa... | Maxime Dénès | 2018-02-12 |
|\ \ \ \ |
|
* \ \ \ \ | Merge PR #6418: More detailed error messages for Canonical Structure, #6398 | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ |
|
* \ \ \ \ \ | Merge PR #6651: Use r.(p) syntax to print primitive projections. | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \
| |_|_|_|_|/
|/| | | | | |
|
| | | * | | | Use specialized function for inductive subtyping inference. | Gaëtan Gilbert | 2018-02-11 |
| | | * | | | Simplification: cumulativity information is variance information. | Gaëtan Gilbert | 2018-02-10 |
| |_|/ / /
|/| | | | |
|
| | * | | | More detailed error messages for Canonical Structure, #6398 | Paul Steckler | 2018-02-06 |
| |/ / /
|/| | | |
|
* | | | | Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees" | Maxime Dénès | 2018-01-31 |
|\ \ \ \ |
|
* \ \ \ \ | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | Maxime Dénès | 2018-01-31 |
|\ \ \ \ \ |
|
| | | * | | | Use r.(p) syntax to print primitive projections. | Maxime Dénès | 2018-01-30 |
| |_|/ / /
|/| | | | |
|
* | | | | | Add test case for #5286. | Maxime Dénès | 2018-01-29 |
| | | * | | Support universe instances on the literal Type | Tej Chajed | 2018-01-26 |
| | * | | | Add test case for #5747 | Maxime Dénès | 2018-01-25 |
| |/ / /
|/| | | |
|
* | | | | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for... | Maxime Dénès | 2018-01-23 |
|\ \ \ \
| |_|/ /
|/| | | |
|
* | | | | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction. | Maxime Dénès | 2018-01-22 |
|\ \ \ \ |
|
* \ \ \ \ | Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints. | Maxime Dénès | 2018-01-22 |
|\ \ \ \ \ |
|
| | | * | | | Adding a test for coqchk bug #6619. | Pierre-Marie Pédrot | 2018-01-20 |
| |_|/ / /
|/| | | | |
|
| * | | | | Add test-suite file for issue #6617. | Cyprien Mangin | 2018-01-19 |