aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2016-09-15Continuing fix to #5078, taking also into account intropatterns.Hugo Herbelin
Getting closer from before when the bug was introduced + test.
2016-09-14Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-12Merge remote-tracking branch 'github-coq/pr/249' into v8.6Matthieu Sozeau
2016-09-11Add a test for 4836Jason Gross
This required improving the machinery of the test-suite Makefile to support -compile.
2016-09-10Test for #5077.Hugo Herbelin
2016-09-09no-refold patchPaul Steckler
Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
2016-09-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-05Test file for #5065 - Anomaly: Not a proof by inductionMaxime Dénès
2016-09-02Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-31Fix bug #5043: [Admitted] lemmas pick up section variables.Pierre-Marie Pédrot
We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables.
2016-08-30Fix bug #4893: not_evar: unexpected failure in 8.5pl1.Pierre-Marie Pédrot
2016-08-30Fix bug #3920: eapply masks an hypothesis name.Pierre-Marie Pédrot
The problem came from the fact that the legacy beta-reduction occurring after a rewrite was wrongly applied to the side-conditions of the rewriting step. We restrict it to the correct goal in this patch.
2016-08-28Fix bug #4764: Syntactic notation externalization breaks.Pierre-Marie Pédrot
2016-08-23Fix bug #4904: [Import] does not load intermediately unqualified names of ↵Pierre-Marie Pédrot
aliases.
2016-08-19Test file for bug #4187.Pierre-Marie Pédrot
2016-08-18Adding a test for bug #4653.Pierre-Marie Pédrot
2016-08-17Fixing #3070 ("subst" taking properly into account chains of dependencies).Hugo Herbelin
2016-08-16Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-29Fix bug #4673: regression in setoid_rewrite.Matthieu Sozeau
Modulo delta for types should be fully transparent.
2016-07-29Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-29Fix bug #3886, generation of obligations of fixesMatthieu Sozeau
This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
2016-07-29Fix #4769, univ poly and elim schemes in sectionsMatthieu Sozeau
2016-07-26Fix bug #4754, allow conversion problems to remainMatthieu Sozeau
when checking that the rewrite relation is homogeneous in setoid_rewrite.
2016-07-21Fix bug #4679, weakened setoid_rewrite unificationMatthieu Sozeau
It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4.
2016-07-20Fix bug #4780: universe leak in letin_tacMatthieu Sozeau
2016-07-20Fix bug #4780: universe leak in letin_tacMatthieu Sozeau
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns).
2016-07-18Marking bug #3383 as solved.Pierre-Marie Pédrot
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.Pierre-Marie Pédrot
2016-07-17Fixing #4932 (anomaly when using binders as terms in recursive notations).Hugo Herbelin
This application was actually not anticipated. It is nice and was not too difficult to support. Design for pattern binders maybe to clarify. When seing pat(x1,..,xn) as a term, I just reused pat(x1,..,xn), but maybe it is worth using the variable aliasing the pattern, for more a concise notation. But at the same time, this means exposing the internal name of the alias which is not so elegant.
2016-07-13Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-08Fix test file for #4858.Maxime Dénès
2016-07-08Test file for #4858.Maxime Dénès
2016-07-08Add test file for #4880.Maxime Dénès
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-07Merge remote-tracking branch 'github/bug4653' into v8.6Matthieu Sozeau
2016-07-07Program: fix #4873: transparency option not usedMatthieu Sozeau
2016-07-06Fixed bug #4622.Matthieu Sozeau
2016-07-06Merge remote-tracking branch 'github/pr/199' into v8.5Maxime Dénès
Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
2016-07-06Fix test-suite file 3690Matthieu Sozeau
2016-07-05congruence fix: test-suite code and update CHANGESMatthieu Sozeau
This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-04congruence/univs: properly refresh (fix #4609)Matthieu Sozeau
In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609.
2016-07-02Adding test for #4811.Hugo Herbelin
2016-07-01Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).Hugo Herbelin
But there are still bugs with Declare Implicit Tactic, which should probably rather be reimplemented with ltac:(tac). Indeed, it does support evars in the type of the term, and solve_by_implicit_tactic should transfer universe constraints to the main goal. E.g., the following still fails, at Qed time. Definition Foo {T}{a : T} : T := a. Declare Implicit Tactic eassumption. Goal forall A (x : A), A. intros. apply Foo. Qed.
2016-06-30Goal selectors now use the keyword [only].Cyprien Mangin
This fixes some parsing problems when doing things like [let n := 2 in idtac n]. See bug #4877.
2016-06-29Fixing #4865 (deciding on which arguments to recompute scopes was not robust).Hugo Herbelin
See 4865.v for details.
2016-06-29Univs: Fix bug #4726Matthieu Sozeau
When using Record and an explicit sort constraint, the universe was wrongly made flexible and minimized.
2016-06-29Fix issues in test-suite revealed by warnings.Maxime Dénès
2016-06-27Univs: allowing notations to take univ instancesMatthieu Sozeau
They can apply to the head reference under a notation.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 09:48:22 +0000