aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
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
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
known instances in unification.ml). This refines the fix to bug #1918. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15459 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Implicit arguments of Definition are taken from the type when given by the user.pboutill
There is a warning if the term is more precise. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15252 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-17Bug 2733 : { } implicits and Fixpointspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15187 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
- tauto/intuition now works uniformly on and, prod, or, sum, False, Empty_set, unit, True (and isomorphic copies of them), iff, ->, and on all inhabited singleton types with a no-arguments constructor such as "eq t t" (even though the last case goes out of propositional logic: this features is so often used that it is difficult to come back on it). - New dtauto and dintuition works on all inductive types with one constructors and no real arguments (for instance, they work on records such as "Equivalence"), in addition to -> and eq-like types. - Moreover, both of them no longer unfold inner negations (this is a souce of incompatibility for intuition and evaluation of the level of incompatibility on contribs still needs to be done). Incidentally, and amazingly, fixing bug #2680 made that constants InfA_compat and InfA_eqA in SetoidList.v lost one argument: old tauto had indeed destructed a section hypothesis "@StrictOrder A ltA@ thinking it was a conjunction, making this section hypothesis artificially necessary while it was not. Renouncing to the unfolding of inner negations made auto/eauto sometimes succeeding more, sometimes succeeding less. There is by the way a (standard) problem with not in auto/eauto: even when given as an "unfold hint", it works only in goals, not in hypotheses, so that auto is not able to solve something like "forall P, (forall x, ~ P x) -> P 0 -> False". Should we automatically add a lemma of type "HYPS -> A -> False" in the hint database everytime a lemma ""HYPS -> ~A" is declared (and "unfold not" is a hint), and similarly for all unfold hints? At this occasion, also re-did some proofs of Znumtheory. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15180 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-12Repair two testsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15131 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-20Generalized the use of evar candidates in type inference unification:herbelin
- use evar candidates instead of postponed conversion problems when it is known (according to the projection heuristic used) that an evar has only a fixed number of possible instances (as e.g. in equation ?n[x,x] = x, with x a variable); - this allows to be more robust in solving remaining problems: if several instanciations exist, and one is not compatible with a previous instantiation made among several choices for another evar, backtracking is now possible; - this allows in particular to fix regression #2670 (two postponed conversion problems solved in an inconsistent way); - but this requires more code. At the same time, a refactoring of the code has been made so as to hopefully clarify the elementary pieces of the algorithm. For instance, there are now generic functions for both applying a filter and giving candidates. The filter is systematically generalized so as to have the ccl of the evar well-typed even in situations where we could try on the contrary to restrict the evars occurring in the ccl. Anyway, when the representation of instances will be optimized using identity substitutions, it will no longer be useful to use the filter to shorten the size of the instances. Then, the filters will have, like candidates, the only role of restricting the search space for potential solutions to the unification problems. Also, solve_refl can now be used to restrict equations ?x[t1..tn]=?x[u1..un] up to conversion instead of up to unification. This (potententially) looses constraints but this avoids looping at the time of considering remaining problems and applying heuristics to them. Also added printing of evar candidates in debugging evar printers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15061 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 13:50:25 +0000