aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
|\
* | 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
|/
* 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
* | | 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
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
| | | * | | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
| | | * | | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| |_|/ / / |/| | | |
| | * | | More detailed error messages for Canonical Structure, #6398Gravatar Paul Steckler2018-02-06
| |/ / / |/| | |
* | | | Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"Gravatar Maxime Dénès2018-01-31
|\ \ \ \
* \ \ \ \ Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \
| | | * | | Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
| |_|/ / / |/| | | |
* | | | | Add test case for #5286.Gravatar Maxime Dénès2018-01-29
| | | * | Support universe instances on the literal TypeGravatar Tej Chajed2018-01-26
| | * | | Add test case for #5747Gravatar Maxime Dénès2018-01-25
| |/ / / |/| | |
* | | | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...Gravatar Maxime Dénès2018-01-23
|\ \ \ \ | |_|/ / |/| | |
* | | | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\ \ \ \
* \ \ \ \ Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Gravatar Maxime Dénès2018-01-22
|\ \ \ \ \
| | | * | | Adding a test for coqchk bug #6619.Gravatar Pierre-Marie Pédrot2018-01-20
| |_|/ / / |/| | | |
| * | | | Add test-suite file for issue #6617.Gravatar Cyprien Mangin2018-01-19
* | | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \ \ \ \ | |/ / / / |/| | | |
* | | | | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Gravatar Maxime Dénès2018-01-17
|\ \ \ \ \
| | | * | | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionGravatar Jasper Hugunin2018-01-17
| | * | | | Add a test that `prod_applist_assum` reduces the right number of let-insGravatar Jasper Hugunin2018-01-17
| | * | | | Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-01-17
| | |/ / /
* | | | | Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\ \ \ \ \ | |_|/ / / |/| | | |
| * | | | More tests on brackets with goal selectors (including failures).Gravatar Théo Zimmermann2018-01-15
| * | | | Add test-suite file for bracket with goal selector.Gravatar Théo Zimmermann2018-01-15
* | | | | Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGravatar Maxime Dénès2018-01-13
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6483: Strong invariants in polymorphic definitionsGravatar Maxime Dénès2018-01-12
|\ \ \ \ \ \
| | * | | | | Document test-suite PRINT_LOGS.Gravatar Gaëtan Gilbert2018-01-11
| | * | | | | Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGravatar Gaëtan Gilbert2018-01-11
| |/ / / / / |/| | | | |
* | | | | | Merge PR #6557: First stab at documenting the test suite.Gravatar Maxime Dénès2018-01-11
|\ \ \ \ \ \
| | * | | | | Force polymorphic definitions to have no internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
| |/ / / / / |/| | | | |
| * | | | | Lint and remove redundant lineGravatar Jasper Hugunin2018-01-11
| * | | | | Add comments by @psteckler to test-suite/README.mdGravatar Jasper Hugunin2018-01-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 01:19:24 +0000