aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Collapse)Author
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-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 *)
2014-06-26Fix bug # 3325 using canonical structure declarations where needed.Matthieu Sozeau
2014-06-26Fixed bug with new semantics of change.Matthieu Sozeau
2014-06-26Properly refresh the local hintdb database in case an external tactic changedMatthieu Sozeau
the hypotheses in eauto.
2014-06-26Bug #3329 is closed.Matthieu Sozeau
2014-06-263392 is now closed thanks to E. Tassi.Matthieu Sozeau
2014-06-26Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into ↵Matthieu Sozeau
JasonGross-more-test-suite Conflicts: test-suite/bugs/closed/3300.v test-suite/bugs/closed/3373.v
2014-06-26Fix test-suite files.Matthieu Sozeau
2014-06-26Bug #3301 is closed, the projection cannot be defined anymore.Matthieu Sozeau
2014-06-26Fix test-suite file for bug # 3036, the unification has _never_ succeeded,Matthieu Sozeau
as this would result in an ill-scoped substitution.
2014-06-26Change interface of refresh universes to get a pbty argument instead ofMatthieu Sozeau
the computed direction argument. In case pbty is conv, no refreshing is done as the evar body must be convertible with the given term, however refreshing of template application evar arguments can still happen. (Re)-Closing bug #2966.
2014-06-26Add an Unset Standard...Matthieu Sozeau
2014-06-23Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Enrico Tassi
Every time you use abstract a kitten dies, please stop.
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-04 04:13:11 +0000