aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Collapse)Author
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
2014-10-15Fix test-suite files which failed due to usage of $(admit)$ whichMatthieu Sozeau
now fails with Error: Already an existential evar of name Main
2014-10-15Fix bug 3637.Matthieu Sozeau
2014-10-15Reenable FO unification of primitive projections and their eta-expandedMatthieu Sozeau
forms in evarconv and unification, as well as fallback to first-order unification when eta for constructors fail. Update test-suite file 3484 to test for the FO case in evarconv as well.
2014-10-15Fix test-suite file after moving back to using C as the nameMatthieu Sozeau
of the record binder for Class C's projections.
2014-10-15Implement a different strategy to expand primitive projections only whenMatthieu Sozeau
required, i.e. in first-order unification cases where the head of the other side is a hole or the eta-expanded constant.
2014-10-14Fix bug #3698: stack overflow due to eta+canonical structures inMatthieu Sozeau
unification.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 04:40:55 +0000