| Age | Commit message (Expand) | Author |
|---|
| 2018-02-20 | Trying a hack to support {'pat|P} without breaking compatibility. | Hugo Herbelin |
| 2018-02-20 | 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-19 | Merge PR #6728: Extrude monomorphic universe contexts from with Definition co... | Maxime Dénès |
| 2018-02-16 | 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-15 | 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-14 | Merge PR #6713: Fix #6677: Critical bug with VM and universes | Maxime Dénès |
| 2018-02-12 | 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-11 | Use specialized function for inductive subtyping inference. | Gaëtan Gilbert |
| 2018-02-10 | Simplification: cumulativity information is variance information. | Gaëtan Gilbert |
| 2018-02-06 | More detailed error messages for Canonical Structure, #6398 | Paul Steckler |
| 2018-01-31 | 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-30 | Use r.(p) syntax to print primitive projections. | Maxime Dénès |
| 2018-01-29 | Add test case for #5286. | Maxime Dénès |
| 2018-01-26 | Support universe instances on the literal Type | Tej Chajed |
| 2018-01-25 | Add test case for #5747 | Maxime Dénès |
| 2018-01-23 | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for... | Maxime Dénès |
| 2018-01-22 | 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-20 | Adding a test for coqchk bug #6619. | Pierre-Marie Pédrot |
