| Age | Commit message (Expand) | Author |
|---|
| 2018-02-28 | Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit... | Maxime Dénès |
| 2018-02-24 | Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism). | Maxime Dénès |
| 2018-02-24 | Merge PR #6599: Decimals in prelude | Maxime Dénès |
| 2018-02-23 | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion). | Hugo Herbelin |
| 2018-02-21 | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred` | Maxime Dénès |
| 2018-02-21 | Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585) | Maxime Dénès |
| 2018-02-21 | Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the... | Maxime Dénès |
| 2018-02-21 | Merge PR #6740: Adding a sanity check on inductive variance subtyping. | Maxime Dénès |
| 2018-02-20 | Update SearchPattern.out for numeral notations | Jason Gross |
| 2018-02-20 | Fixes bug #6774 (anomaly with ill-typed template polymorphism). | Hugo Herbelin |
| 2018-02-20 | Adding a test for wish #5532. | Hugo Herbelin |
| 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-19 | Fix #6529: nf_evar_info and check the env evars' not just the concl | Matthieu Sozeau |
| 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 | Adding a test for variance subtyping in the module system. | 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 | Extend `zify_N` with knowledge about `N.pred` | 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 |
