aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2014-04-10Add a regression test for bug 3001Jason Gross
2014-04-05Test for bug #3142, actually duplicate of #3262.Hugo Herbelin
2014-04-05Fixing bug #3228 (fixing precedence of ltac variables over variables in env).Hugo Herbelin
2014-04-02Add a test case for bug 3251Jason Gross
It was closed in 5b39c3535f7b3383d89d7b844537244a4e7c0eca.
2014-04-01Fixing bug #2900 (evar/evar unif was supposed to be treated inHugo Herbelin
solve_simple_eqn but in case the second evar was hidden behind a local variable, it arrived in evar_define and imitate, wrongly assuming progress).
2014-01-25Adding a test for bug #3023.Pierre-Marie Pédrot
2014-01-10Fix bug#2080: error message on Ltac name clash with primitive tacticsxclerc
2013-12-19Missing Fail in r16792Pierre Boutillier
2013-12-16Added test-suite for bug #2990.Pierre-Marie Pédrot
2013-12-12Better unification for [projT1] and [proj1_sig].Jason Gross
This way, [fun A (P : A -> Prop) (X : sigT P) => proj1_sig X] unifies with [fun A (P : A -> Prop) (X : sigT P) => projT1 X]. This closes Bug 3043.
2013-12-06Fix the refine related test-suite files to account for the new refine.Arnaud Spiwack
2013-12-02Test case for bug#2848.xclerc
2013-11-29Testsuite: flatten the 'bugs/opened' directory.xclerc
2013-09-20Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Get rid of "shouldfail" subdirectory by moving tests to parent directory.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16796 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Wrong bug identifier.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16795 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Update test for bug 2846 in order to use "Fail".xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16793 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Use "Fail" rather than rely on exit code.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Added test for bug #2846.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16663 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Added a test for bug #3062.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16661 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Added a test for bug #3088.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16650 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-29Tentative fix for #3054: we refresh universes in a term generatedppedrot
by congruence, as it seems to be done methodically on the remaining of this plugin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16642 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-25Fixing bug #3093 by adding the asked test case.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16634 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-27Bugfix: Fixing #3050ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16608 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Protection against "Bad recursive type" in w_unify0 (bug #3036).herbelin
Morally, unification wants to unify "fun x:Meta => Meta" with "fun x:nat => match x with ... end". Retyping is asked to type "match x with ... end" in the context "x:Meta" where the type of x has de facto been lost. Retyping fails. I don't see an easy remedy since w_unify0 builds the unifier lazily, and I'm not sure it is worth to propagate the unifier to retyping so that it knows it. After all, the call to retyping in w_unify0 is not so critical. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16489 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-27Added a unit test for bug #2230.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16460 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18Finer fix for bug 3017, mark unresolvability only of goals that aremsozeau
instances of metas in clenvtac. Makes Math-Classes compile again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16429 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Like in r16346, do not filter local definitions (here in theherbelin
type-based second-order unification algorithm). In type-based second-order unification algorithm, protect local definitions in instances of evars to wrongly be considered as potentially flexible. Altogether, this fixes the anomaly in #3003 (even if some additional work has to be done to improve the resulting error message, see next commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16414 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-16Added regression test for bug #3023 which was solved by Matthieu'sherbelin
commit r16134 (eta was missing in Flexible/Rigid and SemiFlexible/Rigid conversion problems). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16409 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-10Equality: avoid some unprotected List.nth (fix #2837)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16392 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-08Enrich test-suite with a test for #3022.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16390 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Enrich test-suite with a test for #2928letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16367 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Enrich test-suite with a test for #2734letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16365 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Add the test-case of bug 2750 in the test-suiteletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16362 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
Since the nametab isn't aware of everything needed to print mismatched types (cf the bug test-cases), we create a robust term printer that known how to print a fully-qualified name when [shortest_qualid_of_global] has failed. These Printer.safe_pr_constr and alii are meant to never fail (at worse they display "??", for instance when the env isn't rich enough). Moreover, the environnement may have changed between the raise of NotConvertibleTypeField and its display, so we store the original env in the exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16342 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Firstorder: record with defined field aren't conjonctions (fix #2629)letouzey
The let-in in the type of constructor was perturbating the Hipattern.dependent check, leading firstorder to consider too much inductives as dependent-free conjonctions, ending with lift errors (UNBOUND_REL_-2, ouch). This patch is probably overly cautious : if the variable of the let-in is used, we consider the constructor to be dependent. If someday somebody feels it necessary, he/she could try to reduce the let-in's instead... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16339 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16328 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-20Check a list length before doing a List.chop (fix #3000)letouzey
I'm not completely sure that raising Not_found is the right thing to do here, but it seems reasonable... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16326 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-18Fix for bug #3004 (thanks Hugo!)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16317 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-21A slightly more efficient test of well-typedness of restriction ofherbelin
evars (though this might be slighty more costly). This incidentally solves Appel's part of bug #2830 even though a conceptual problem around the interaction of unification with the proof engine has to be solved. Indeed, what to do when unification, called as part of a tactic, solves or refines the current goal by side effect. Somehow, unifyTerms or tclEVARS should take this possibility into consideration, either by forbidding the refinement of the current goal by side effect, or by acknowledging this refinement by producing new subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16232 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-05Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenherbelin
variable names). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16185 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-29Added a file for testing regression of bug #2955 (anomaly in simpl inherbelin
the presence of aliased modules). Bug was actually fixed in trunk (thanks to PMP's monomorphization (and change of semantics) of equality over evaluable references. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16180 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-29Fixing bug #2969 (admit failing after Grab Existential Variables dueherbelin
to inconsistency in using evar_hyps which is unfiltered and evar_env which is filtered). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16175 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Fixed bug #2966 (de Bruijn error in computation of heads for coercions).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16168 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Fixing one part of #2830 (anomaly "defined twice" due to nested calls toherbelin
the function solve_candidates introduced in 8.4). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16163 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18Unset Asymmetric Patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25Fixed bug #2930: folded let-in's were hiding a violation to the occurherbelin
check condition in pattern-unification, resulting in the instantiation of evars by terms depending on themselves, henceforth leading eventually to a stack overflow. Occur-check in the arguments of evars was also missing. [Also fixed what looked like a typo in the env passed to project_evar_on_evar on line 1611.] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15996 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-29Fixing #2836 (materialize_evar might refine as a side effect theherbelin
current evar to project; this may happen if this evar is dependent and is involved in evar-evar conversion problem eventually solved by instantiating the current evar; could maybe be optimized when the evar to materialize has invertible instance in which case define_evar_from_virtual_equation applied on the current evar could be shortcut, avoiding to create an evar). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15657 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Continuing r15459: it helps testing occur-check early in someherbelin
situations (see rewrite MonoidMonadTrans.bind_toLower' in Misc/QuicksortComplexity/monoid_expec.v). Also fixing badly designed test 2817.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15543 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
- For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-06 15:46:38 +0000