aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Collapse)Author
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 "Fix files in test-suite having to do with Require inside modules."Maxime Dénès
This reverts commit a7ed77403cd15ba1cc2c05f2b6193b46f0028eda.
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-06Fixing test for bug #2830.Pierre-Marie Pédrot
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
Removing unused argument and fixing bug #3899, now warning when a record cannot be made primitive in Set Primitive Projections mode because it has no projection or at least one undefinable projection.
2015-01-04Adapting two files from test-suite to now forbidden Require's in modules.Hugo Herbelin
Status of 335 and 3363 which are explicitly testing Require in modules still to be addressed (to remove from test suite?).
2015-01-03Fixing #3896 (incorrect sigma given to printer).Hugo Herbelin
2015-01-03Fixing #3895 (thanks to PMP for diagnosis).Hugo Herbelin
2014-12-30Fixing #3892: Ensure that notation variables do not capture namesHugo Herbelin
hidden behind another notation.
2014-12-16#3828 is solved.Hugo Herbelin
2014-12-16Moving #2447 (congruence) to fixed.Hugo Herbelin
2014-12-16Test for #3654.Hugo Herbelin
2014-12-15Tests for #3848 and #3854.Hugo Herbelin
2014-12-12Two fixes in unification (bugs #3782 and #3709)Matthieu Sozeau
- In evarconv, check_conv_record properly computes the parameters of primitive record projections for later unification, adding env and sigma as arguments. - In unification, backtrack on pattern-unification and not only application unification if eta for a record failed.
2014-12-03Updading test-suite.Hugo Herbelin
2014-12-02When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifHugo Herbelin
possible, which is the "natural" way to orient an equation. At least it matters for matching subterms against patterns, so that it is the pattern variables which are substituted if ever the subterm has itself existential variables, as in: Goal exists x, S x = x. eexists. destruct (S _).
2014-12-01Fixing test-suite.Pierre-Marie Pédrot
2014-11-30Adding test for bug #3417.Pierre-Marie Pédrot
2014-11-30Test for bug #3485.Pierre-Marie Pédrot
2014-11-30Test for bug #3487.Pierre-Marie Pédrot
2014-11-30Test of bug #3682.Pierre-Marie Pédrot
2014-11-25Bug #3804 is actually closed (thanks to Jason Gross for the notification).Xavier Clerc
2014-11-23Pass around information on the use of template polymorphism forMatthieu Sozeau
inductive types (i.e., ones declared with an explicit anonymous Type at the conclusion of their arity). With this change one can force inductives to live in higher universes even in the non-fully universe polymorphic case (e.g. bug #3821).
2014-11-22Test for closed #2713 and #2876.Hugo Herbelin
2014-11-21Adding test for bug #3326.Pierre-Marie Pédrot
2014-11-21Adding test for bug #3424.Pierre-Marie Pédrot
2014-11-21Cleaning up closed bugs in test-suite.Pierre-Marie Pédrot
2014-11-21Test for bug #3788.Pierre-Marie Pédrot
2014-11-21Add test-suite file for bug #3804.Matthieu Sozeau
2014-11-20Adding test for bug #3684.Pierre-Marie Pédrot
2014-11-09Adding test for bug 3792.Pierre-Marie Pédrot
2014-11-08Test fixed by PMP's commits from Oct 21.Hugo Herbelin
2014-11-07Test for #3675 on primitive projections.Hugo Herbelin
2014-11-07Fixing #3562 ("as" in "destruct" expects either a disjunctiveHugo Herbelin
intropattern or a bound ltac variable).
2014-11-07Test for #3542 fixed some time ago.Hugo Herbelin
2014-11-06Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels.Hugo Herbelin
2014-11-04Test for bug #2149.Pierre-Marie Pédrot
2014-11-03New bugs revealed fixed: #3408 by (probably) Maxime's commitsHugo Herbelin
on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459.
2014-10-22Fix test-suite for #2729.Maxime Dénès
Was always failing due to an incorrect use of Ltac's or.
2014-10-20Fixing a (new) part of bug #2729.Hugo Herbelin
By moving convert_concl to new proof engine, re-typecheckeing was incidentally introduced. Re-typechecking revealed that vm bug #2729 was still open. Indeed, the vm was still producing an ill-typed term. This commit fixes ill-typedness of the vm in #2729 when reconstructing a "match" in an inductive type whose constructors have let-ins. Another part is still open (see test-suite).
2014-10-16Fix test-suite scripts.Matthieu Sozeau
2014-10-16Bug fixed by Hugo.Matthieu Sozeau
2014-10-15To stay closer to non-primitive projections, only unfold primitiveMatthieu Sozeau
projections in cbv when delta _and_ beta flags are set. Add test-suite file for bug 3700 too.
2014-10-15Fix for bug #3618.Matthieu Sozeau
Fix typeclass resolution which was considering as subgoals of a tactic application unrelated pre-existing undefined evars.
2014-10-15Closed bug 3710.Matthieu Sozeau
2014-10-15Bug 3692 is fixed.Matthieu Sozeau
2014-10-15Bug 3628 is fixed.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-03 15:34:15 +0000