aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-02-20Fixing/improving notations with recursive patterns.Hugo Herbelin
2018-02-20Using name given by user to name a 'pat, if any.Hugo Herbelin
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
2018-02-20Notations: Do not consider a non-occurring variable as a binder-only variable.Hugo Herbelin
2018-02-20Adding support for re-folding notation referring to isolated "forall '(x,y), t".Hugo Herbelin
2018-02-19Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...Maxime Dénès
2018-02-19Fix #6529: nf_evar_info and check the env evars' not just the conclMatthieu Sozeau
2018-02-17Implement name mangling optionJasper Hugunin
2018-02-16Cleaner treatment of parameters in inferCumulativityGaëtan Gilbert
2018-02-16Adding a test for the construction that was broken in Coccinelle.Pierre-Marie Pédrot
2018-02-15Adding a test for variance subtyping in the module system.Pierre-Marie Pédrot
2018-02-15Merge PR #1073: new quick2vo target: like vio2vo, but smarterMaxime Dénès
2018-02-15disable tests: vio2vo is broken in WindowsRalf Jung
2018-02-15also test vio2voRalf Jung
2018-02-15test "make quick2vo"Ralf Jung
2018-02-15Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectMaxime Dénès
2018-02-15coq_makefile: Support "" as the prefix in _CoqProjectJoachim Breitner
2018-02-14Extend `zify_N` with knowledge about `N.pred`Joachim Breitner
2018-02-14Merge PR #6713: Fix #6677: Critical bug with VM and universesMaxime Dénès
2018-02-13Fix issue with spurious timing test failuresJason Gross
2018-02-13Fixing an anomaly in the presence of "let-in" in the type of a record.Hugo Herbelin
2018-02-12Merge PR #1082: Fixing Print for inductive types with let-in in parametersMaxime Dénès
2018-02-12Add test case for #6677.Maxime Dénès
2018-02-12Merge PR #1047: Support universe instances on the literal TypeMaxime Dénès
2018-02-12Merge PR #6128: Simplification: cumulativity information is variance informa...Maxime Dénès
2018-02-12Merge PR #6418: More detailed error messages for Canonical Structure, #6398Maxime Dénès
2018-02-12Merge PR #6651: Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2018-02-06More detailed error messages for Canonical Structure, #6398Paul Steckler
2018-01-31Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"Maxime Dénès
2018-01-31Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Maxime Dénès
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-01-29Add test case for #5286.Maxime Dénès
2018-01-26Support universe instances on the literal TypeTej Chajed
2018-01-25Add test case for #5747Maxime Dénès
2018-01-23Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...Maxime Dénès
2018-01-22Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Maxime Dénès
2018-01-22Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Maxime Dénès
2018-01-20Adding a test for coqchk bug #6619.Pierre-Marie Pédrot
2018-01-19Add test-suite file for issue #6617.Cyprien Mangin
2018-01-18Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Maxime Dénès
2018-01-17Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Maxime Dénès
2018-01-17Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionJasper Hugunin
2018-01-17Add a test that `prod_applist_assum` reduces the right number of let-insJasper Hugunin
2018-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
2018-01-16Merge PR #6551: Bracket with goal selectorMaxime Dénès
2018-01-15More tests on brackets with goal selectors (including failures).Théo Zimmermann
2018-01-15Add test-suite file for bracket with goal selector.Théo Zimmermann
2018-01-13Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGSMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 13:19:53 +0000