aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Maxime Dénès2018-02-24
|\
* \ Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \
* \ \ Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \ \
* \ \ \ Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Gravatar Maxime Dénès2018-02-21
|\ \ \ \
* \ \ \ \ Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6740: Adding a sanity check on inductive variance subtyping.Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \
| | | | | * | Update SearchPattern.out for numeral notationsGravatar Jason Gross2018-02-20
| |_|_|_|/ / |/| | | | |
| | | | | * Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Hugo Herbelin2018-02-20
| |_|_|_|/ |/| | | |
| | | * | Adding a test for wish #5532.Gravatar Hugo Herbelin2018-02-20
| | | * | Trying a hack to support {'pat|P} without breaking compatibility.Gravatar Hugo Herbelin2018-02-20
| | | * | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Gravatar Hugo Herbelin2018-02-20
| | | * | Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
| | | * | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
| | | * | When printing a notation with "match", more flexibility in matching equations.Gravatar Hugo Herbelin2018-02-20
| | | * | Adding general support for irrefutable disjunctive patterns.Gravatar Hugo Herbelin2018-02-20
| | | * | Using an "as" clause when needed for printing irrefutable patterns.Gravatar Hugo Herbelin2018-02-20
| | | * | Refining the strategy for glueing let-ins to a sequence of binders.Gravatar Hugo Herbelin2018-02-20
| | | * | A (significant) simplification in printing notations with recursive binders.Gravatar Hugo Herbelin2018-02-20
| | | * | Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
| | | * | Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
| | | * | Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
| | | * | In printing notations with "match", reasoning up to the order of clauses.Gravatar Hugo Herbelin2018-02-20
| | | * | Supporting recursive notations reversing the left-to-right order.Gravatar Hugo Herbelin2018-02-20
| | | * | Allowing variables used in recursive notation to occur several times in pattern.Gravatar Hugo Herbelin2018-02-20
| | | * | Allows recursive patterns for binders to be associative on the left.Gravatar Hugo Herbelin2018-02-20
| | | * | Fixing/improving notations with recursive patterns.Gravatar Hugo Herbelin2018-02-20
| | | * | Using name given by user to name a 'pat, if any.Gravatar Hugo Herbelin2018-02-20
| | | * | Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
| | | * | Notations: Do not consider a non-occurring variable as a binder-only variable.Gravatar Hugo Herbelin2018-02-20
| | | * | Adding support for re-folding notation referring to isolated "forall '(x,y), t".Gravatar Hugo Herbelin2018-02-20
| |_|/ / |/| | |
* | | | Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...Gravatar Maxime Dénès2018-02-19
|\ \ \ \
| | | * | Fix #6529: nf_evar_info and check the env evars' not just the conclGravatar Matthieu Sozeau2018-02-19
* | | | | Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| * | | | Adding a test for the construction that was broken in Coccinelle.Gravatar Pierre-Marie Pédrot2018-02-16
|/ / / /
| * / / Adding a test for variance subtyping in the module system.Gravatar Pierre-Marie Pédrot2018-02-15
|/ / /
* | | Merge PR #1073: new quick2vo target: like vio2vo, but smarterGravatar Maxime Dénès2018-02-15
|\ \ \
| * | | disable tests: vio2vo is broken in WindowsGravatar Ralf Jung2018-02-15
| * | | also test vio2voGravatar Ralf Jung2018-02-15
| * | | test "make quick2vo"Gravatar Ralf Jung2018-02-15
* | | | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectGravatar Maxime Dénès2018-02-15
|\ \ \ \
| * | | | coq_makefile: Support "" as the prefix in _CoqProjectGravatar Joachim Breitner2018-02-15
| | | | * Extend `zify_N` with knowledge about `N.pred`Gravatar Joachim Breitner2018-02-14
| |_|_|/ |/| | |
* | | | Merge PR #6713: Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-14
|\ \ \ \ | |_|_|/ |/| | |
* | | | Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\ \ \ \ | |_|/ / |/| | |
| | * | Add test case for #6677.Gravatar Maxime Dénès2018-02-12
| | |/
* | | Merge PR #1047: Support universe instances on the literal TypeGravatar Maxime Dénès2018-02-12
|\ \ \
* \ \ \ Merge PR #6128: Simplification: cumulativity information is variance informa...Gravatar Maxime Dénès2018-02-12
|\ \ \ \
* \ \ \ \ Merge PR #6418: More detailed error messages for Canonical Structure, #6398Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 05:42:01 +0000