aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2016-09-26Unbreak Ltac [ | .. | ] notation in -compat 8.5Jason Gross
Importing VectorNotations breaks `; []`. So we make sure it's not imported by defualt. Some files might be required to `Import VectorDef.VectorNotations` rather than just `Import VectorNotations`.
2016-09-26Fix bug #4785 (use [ ] for vector nil)Jason Gross
Also delimit vector_scope with vector, so that people can write %vector without having to delimit it themselves.
2016-09-26Fix bug #5093: typeclasses eauto depth arg does not accept a var.Pierre-Marie Pédrot
2016-09-24Adding a test for bug #5096.Pierre-Marie Pédrot
2016-09-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-22Fixing #5095 (non relevant too strict test in let-in abstraction).Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:53:24 +0000