aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2014-09-17Revert "While resolving typeclass evars in clenv, touch only the ones that ↵Matthieu Sozeau
appear in the" This reverts commit 9de1edd730eeb3cada742a27a36bc70178eda6d8. Not the right way to do it. The evd shouldn't contain unrelated evars in the first place.
2014-09-17While resolving typeclass evars in clenv, touch only the ones that appear in theMatthieu Sozeau
clenv's value and type, ensuring we don't try to solve unrelated goals (fixes bug#3633).
2014-09-17Update test-suite files after last commit. Add a file for rewrite_stratMatthieu Sozeau
examples.
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
2014-09-15Fixing line break in test for #3559.Hugo Herbelin
2014-09-13Fixing injection bug #3616 on sigma-types.Hugo Herbelin
2014-09-12An old typo which was preventing example #3537 to work the same as itHugo Herbelin
was working in 8.4.
2014-09-11Fix test-suite files, and move some opened to closed.Matthieu Sozeau
2014-09-11Fix bug #3594: eta for constructors and functions at the same time whichMatthieu Sozeau
was failing in this case due to the wrong postponment of an unsolvable ?X = RigidContext[?X] problem.
2014-09-11Fix bug #3596, wrong treatment of projections in compute_constelim_direct.Matthieu Sozeau
2014-09-11Fix bug #3505.Matthieu Sozeau
When w_unifying primitive projection applications, force the unification of types of the projected records to recover instances for the parameters (evarconv does this automatically by unifying evar instances with their expected type).
2014-09-07Test for "inversion as" naming bug.Hugo Herbelin
2014-09-07Regression test #3557Hugo Herbelin
2014-09-07Regression test for bug #2883.Hugo Herbelin
2014-09-06Fix bug #3584, elaborating pattern-matching on primitive records to theMatthieu Sozeau
use of projections.
2014-09-04Status error for bug #3459.Pierre-Marie Pédrot
2014-09-04Test for bug #3459.Pierre-Marie Pédrot
2014-09-04Fix bug #3561, correct folding of env in context[] matching.Matthieu Sozeau
2014-09-04Fix bug #3559, ensuring a canonical order of universe level quantifications whenMatthieu Sozeau
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one used before introduction of hMaps in LMap/LSet.
2014-09-04Add test suite files for closed bugs.Matthieu Sozeau
2014-09-04Fix bug #3563, making syntactic matching of primitive projectionsMatthieu Sozeau
and their eta-expanded forms succeed, potentially filling parameter metavariables from the type information of the projected object.
2014-09-03Test-suite for bug #2818.Pierre-Marie Pédrot
2014-08-29Add test-suite file. Compute the name for the record binder in theMatthieu Sozeau
eta-expanded version of a projection as before.
2014-08-28Fix bugs #3484 and #3546.Matthieu Sozeau
The unification oracle now prefers unfolding the eta-expanded form of a projection over the primitive projection, and allows first-order unification on applications of constructors of primitive records, in case eta-conversion fails (disabled by previous patch on eta).
2014-08-28There are some occurs-check cases that can be handled by imitation (using ↵Matthieu Sozeau
pruning), hence do not entirely prevent solve_simple_eqn in case of apparent occurs-check but backtrack to eqappr on OccurCheck failures (problem found in Ssreflect).
2014-08-28Adding test-suite for bug #3212.Pierre-Marie Pédrot
2014-08-26Add a regression test for 3427Jason Gross
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing.
2014-08-25Fix computation of dangling constraints at the end of a proof (bug #3531).Matthieu Sozeau
2014-08-23Fix test-suite file.Matthieu Sozeau
2014-08-18Fix test-suite files.Matthieu Sozeau
2014-08-18Fix test-suite file.Matthieu Sozeau
2014-08-14Restrict eta-conversion to inductive records, fixing bug #3310.Matthieu Sozeau
2014-08-13Fix test-suite files according to new parsing rule for application of primitiveMatthieu Sozeau
projections.
2014-08-12Bug #3469: fixing unterminated comment.Hugo Herbelin
2014-08-12In bug #2406, renouncing to test failure of parsing error.Hugo Herbelin
(AFAIU, it is the table of supported unicode characters which has to be upgraded anyway.)
2014-08-09Fix unification which was failing when unifying a primitive projection againstMatthieu Sozeau
its expansion if it could reduce (fixes bug #3480).
2014-08-08Fix evarconv not applying eta when it used to. Fixes bug#3319.Matthieu Sozeau
2014-08-03Fixing #3483 (graceful failing with notations to non-constructors in "match").Hugo Herbelin
2014-07-31Finish fixes on notations and primitive projections, add test-suite files ↵Matthieu Sozeau
for closed bugs
2014-07-30Add test-suite file for bug #3439.Matthieu Sozeau
2014-07-29Add test-suite file for bug 3454.Matthieu Sozeau
2014-07-29Add test-suite file for bug #3453Matthieu Sozeau
2014-07-21Adding a test-suite for bug #3422.Pierre-Marie Pédrot
2014-07-16Adding a test-suite for bug #3416.Pierre-Marie Pédrot
2014-07-03Fix eta expansion of primitive records (HoTT bug #78), which now fails ↵Matthieu Sozeau
cleanly when called on partially applied constructors. Also protect evar_conv from that case.
2014-07-02Indeed simpl never is really honored now.Matthieu Sozeau
2014-06-30Tests for bugs #2834 and #2994.Hugo Herbelin
2014-06-30Completing test for bug report #2830Hugo Herbelin
2014-06-28Quickly fixing bug #2996: typing functions now check when referring toHugo Herbelin
a global reference that the current (goal) env contains all the section variables that the global reference expects to be present. Note that the test for inclusion might be costly: everytime a conversion happens in a section variable copied in a goal, this conversion has to be redone when referring to a constant dependent on this section variable. It is unclear to me whether we should not instead give global names to section variables so that they exist even if they are not listed in the context of the current goal. Here are two examples which are still problematic: Section A. Let B := True : Type. Definition C := eq_refl : B = True. Theorem D : Type. clearbody B. set (x := C). unfold C in x. (* inconsistent context *) or Section A. Let B : Type. exact True. Qed. Definition C := eq_refl : B = True. (* Note that this violated the Qed. *) Theorem D : Type. set (x := C). unfold C in x. (* inconsistent context *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-19 07:13:03 +0000