aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2015-02-15Test for bug #3916.Pierre-Marie Pédrot
2015-02-15Fixing test-suite.Pierre-Marie Pédrot
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
Of course such proofs cannot be processed asynchronously
2015-02-14Test for bug #4016.Pierre-Marie Pédrot
2015-02-14Univs: fix bug #3755. We were missing refreshements of universes inMatthieu Sozeau
unifications ?X ~= ?Y foo not catched by solve_evar_evar.
2015-02-14Univs: When computing the level of an inductive including indices, letsMatthieu Sozeau
do not contribute. Fixes bug #3808.
2015-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-13Fix test-suite file to finishMatthieu Sozeau
2015-02-12Fixed test-suite file, that should always work.Matthieu Sozeau
2015-02-12Add test-suite files for closed bugs.Matthieu Sozeau
2015-02-12COMPATIBILITY: add note about the change of behavior of Instance foo :=Matthieu Sozeau
{| |}. Add test-suite files for closed bugs.
2015-02-12Univs: fix bug #4031: wrong folding of sigma in change.Matthieu Sozeau
2015-02-11Adding test for bug #3786.Pierre-Marie Pédrot
2015-02-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-11Adding a test-suite for tactic notation naming.Pierre-Marie Pédrot
2015-02-11Adding test for bug #3900.Pierre-Marie Pédrot
2015-02-10Fixing #4001 (missing type constraints when building return clause of match).Hugo Herbelin
2015-02-10Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ↵Hugo Herbelin
declarations).
2015-02-10Fixing #4018 (uncaught exception on non-equality in intros [=]).Hugo Herbelin
2015-02-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-10Test for bug #4012.Pierre-Marie Pédrot
2015-01-28Several reproduction cases for the test suite.Xavier Clerc
2015-01-28Several reproduction cases for the test suite.Xavier Clerc
2015-01-27Adding a test for bug #3957.Pierre-Marie Pédrot
2015-01-25Merge branch 'v8.5' into trunk.Pierre-Marie Pédrot
2015-01-25Test for bug #3798.Pierre-Marie Pédrot
2015-01-19Making unification of LetIn's expressions more consistent (see #3920).Hugo Herbelin
Unifying two let-in's expresions syntactically is a heuristic (compared to performing the zeta-reduction). This heuristic was requiring unification of types which is too strong for the heuristic to work uniformly since the types might only be related modulo subtyping. The patch is to remove the unification of types, which allows then to have the heuristic work uniformly on the bodies. On the other side, I hope it does not loose (still heuristical) unifications compared to before (presumably, since instantiating the evars in the body will induce constraints for solving potential evars in the types of the let-in bodies, but this would need a proof). Anyway, it is not about correction, it is about a heuristic, which maybe done too early actually.
2015-01-18Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
printing functions touched in the kernel).
2015-01-18Revert "Adapting two files from test-suite to now forbidden Require's in ↵Maxime Dénès
modules." This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e.
2015-01-18Revert "Update test for #3363 now that Require is forbidden inside modules."Maxime Dénès
This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d.
2015-01-18Revert "Fix files in test-suite having to do with Require inside modules."Maxime Dénès
This reverts commit a7ed77403cd15ba1cc2c05f2b6193b46f0028eda.
2015-01-18Univs: Fix alias computation for VMs, computation of normal form ofMatthieu Sozeau
match predicates for vm_compute and compile polymorphic definitions to constant code. Add univscompute test-suite file testing VM computations in presence of polymorphic universes.
2015-01-18Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Matthieu Sozeau
Not supposed to be part of 8.5beta. This reverts commit 74682bb27da074fedc115238f3085baaccf12d73.
2015-01-18There was one more universe needed due to the use of now ↵Matthieu Sozeau
non-universe-polymorphic ID, fixing the script results in 3 universes for the stdlib again.
2015-01-17Back to 4 expected universes.Matthieu Sozeau
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
printing functions touched in the kernel).
2015-01-17Revert "Adapting two files from test-suite to now forbidden Require's in ↵Maxime Dénès
modules." This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e.
2015-01-17Revert "Update test for #3363 now that Require is forbidden inside modules."Maxime Dénès
This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d.
2015-01-17Revert "Fix files in test-suite having to do with Require inside modules."Maxime Dénès
This reverts commit a7ed77403cd15ba1cc2c05f2b6193b46f0028eda.
2015-01-17Univs: Fix alias computation for VMs, computation of normal form ofMatthieu Sozeau
match predicates for vm_compute and compile polymorphic definitions to constant code. Add univscompute test-suite file testing VM computations in presence of polymorphic universes.
2015-01-16Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Matthieu Sozeau
Not supposed to be part of 8.5beta. This reverts commit 74682bb27da074fedc115238f3085baaccf12d73.
2015-01-13TCs: Properly handle Hint Extern with conclusions of the form _ -> _Matthieu Sozeau
in typeclasses eauto, remaining compatible with eauto and still producing eta-reduced applications for Hint Resolves. Fixes bug #3794.
2015-01-13Fix test-suite file, we were testing that no anomaly was raisedMatthieu Sozeau
and this is the case now.
2015-01-12Fix files in test-suite having to do with Require inside modules.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-12Update test for #3363 now that Require is forbidden inside modules.Maxime Dénès
2015-01-12Fixing name of evars in output test Notation.v.Hugo Herbelin
2015-01-11Extraction: discard code unnecessary to fulfill a module signaturePierre Letouzey
2015-01-09STM: fix handling of side effects in vio2voEnrico Tassi
2015-01-06rename: vi -> vioEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-11 17:15:31 +0000