aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Collapse)Author
2016-10-11Fix test-suite file 5123 to fail in case of regressionMatthieu Sozeau
2016-10-11Fix bug #5123: mark all shelved evars unresolvableMatthieu Sozeau
Previously, some splipped through and were caught by unrelated calls to typeclass resolution.
2016-10-11Fix for bug #4863, update the Proofview's env withMatthieu Sozeau
side_effects. Partial solution to the handling of side effects in proofview.
2016-10-10Add test file for #4416.Maxime Dénès
2016-10-08Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-08Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.Pierre-Marie Pédrot
2016-10-07Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Pierre-Marie Pédrot
We simply catch the RetypeError raised by the retyping function and translate it into a user error, so that it is captured by the tactic monad instead of reaching toplevel.
2016-10-06evarconv.ml: Fix bug #4529, primproj unfoldingMatthieu Sozeau
Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that.
2016-10-06unification.ml: fix for bug #4763, unif regressionMatthieu Sozeau
Do not force all remaining conversions problems to be solved after the _first_ solution of an evar, but only at the end of assignment of terms to evars in w_merge. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too.
2016-10-05Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-03Fixing #4970 (confusion between special "{" and non special "{{" in notations).Hugo Herbelin
2016-10-01Fix bug #4661: Cannot mask the absolute name.Pierre-Marie Pédrot
The patch is quite dumb: it essentially consists in alpha-renaming bound module names when printing a functor, by checking that the name was not already present, and generating a fresh one otherwise.
2016-09-30Fix bug #5045: [generalize] creates ill-typed terms in 8.6.Pierre-Marie Pédrot
2016-09-30Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk.Pierre-Marie Pédrot
This bug was introduced by 37ab45726, because the new apply_type function was not checking that the new goal was indeed well-typed. We add this check locally in the generalize dependent tactic.
2016-09-30Merge remote-tracking branch 'github/pr/299' into v8.6Maxime Dénès
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in constraints.
2016-09-30Merge branch 'v8.5' into v8.6Maxime Dénès
2016-09-30Fix #4762.Cyprien Mangin
2016-09-29Move vector/list compat notations to their relevant filesJason Gross
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files.
2016-09-29Fix bug #4798: compat notations should not modify the parser.Pierre-Marie Pédrot
This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data.
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
It seems warnings are not taken into account in output/ tests.
2016-09-29Merge branch 'bug5036' into v8.6Matthieu Sozeau
2016-09-29Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
2016-09-29Merge branch 'bug4723' into v8.6Matthieu Sozeau
2016-09-29Fix bug 4969, autoapply was not tagging shelved subgoals correctly as ↵Matthieu Sozeau
unresolvable
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-09-29Fix bug #5011: Anomaly on [Existing Class].Pierre-Marie Pédrot
2016-09-28Fix bug #4723 and FIXME in API for solve_by_tacMatthieu Sozeau
This avoids leakage of universes. Also makes Program Lemma/Fact work again, it tries to solve the remaining evars using the obligation tactic.
2016-09-28Merge remote-tracking branch 'github/pr/232' into v8.6Maxime Dénès
Was PR#232: Fix the parsing of goal selectors.
2016-09-27Add fixed test-suite file for bug #4527Matthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 05:31:15 +0000