| Commit message (Expand) | Author | Age |
* | 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-24 |
|\ \ |
|
* \ \ | 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-21 |
|\ \ \ \ \ \ |
|
| | | | | * | | 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-20 |
| |_|/ /
|/| | | |
|
* | | | | 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-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 |
|/ / / / |
|
| * / / | 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-15 |
| | | | * | 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-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 |