aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
how the names of an ltac expression are globalized - allowing the expression to be a constr and in some initial context - and when and how this ltac expression is interpreted - now expecting a pure tactic in a different context). This incidentally found a Ltac bug in Ncring_polynom! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-16Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).herbelin
(technically, since the signature "tomatch" of terms to match and of terms to generalize is typed in a context that does not consider terms to match as binders while the return predicate do consider them as binders, the adjusment of the context of the "tomatch" to the context of the predicate needs lifting in each missing part of the "tomatch" context, what was not done) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14664 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Regression tests for bugs #2613 and #2616.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14604 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25New strategy to infer return predicate of match construct whenherbelin
external type has evars. We now create a new ad hoc evar instead of having evars as arguments of evars and use filters to resolved them as was done since about r10124. In particular, this completes the resolution of bug 2615. Evar filters for occurrences might be obsolete as a consequence of this commit. Also, abstract_tycon, evar_define, second_order_matching which all implement some form of second_order_matching should eventually be merged (abstract_tycon looks for subterms up to delta while second_order_matching currently looks for syntactic equal subterms, evar_define doesn't consider the possible dependencies in non-variables-nor-constructors subterms but has a better handling of aliases, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14592 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-24Mod_subst: Attempt to fix #2608letouzey
In presence of inlining, it seems that no alias is propagated on the canonical kernel_name. We modify [subst_con0] to enforce this semantics. It seems to work well, but my understanding of this code is still limited... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14587 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix bug #2473 due to wrong folding of the evar environmentmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14573 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix inductive coercion code in Program (bug #2378)msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14571 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix bug #2586 and enhance clsubst* as well as a side effectmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14570 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-17Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing ↵msozeau
zeta reductions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14564 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-12test-suite: non-regression test for bug #2603letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14556 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Added test for bug #2615herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14555 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
Btw, we also get rid of equalities on something else than elements or sets git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14525 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
- We now handle things like (H : E.eq x x -> ...) by rewriting E.eq x x into True. - There was also a confusion between E.t and its various equivalent (but syntactically different) forms. This should be solved by preventing inlining during an inner functor application. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14520 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-15Omega aware of Z.pred (fix #1912)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14472 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-15Re-allowing assumptions during proofs seems safe now (fix #2411)letouzey
This restriction was introduce to solve #808, whose underlying issue (causing a anomaly) doesn't seem active anymore. Semantic: - Axiom in the middle of a proof : immediatly usable (just as a Definition) - Hypothesis or Variable : not visible in current proof, only usable in the next ones. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14470 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
evars when rewriting. Use it for autorewrite and subst. Accept evars instantiation in multi_rewrite so that rewrite alone remains compatible (it is used in contribs, e.g. Godel, in places where it does not seem absurd to allow it), but there are no good reason for it. Comments welcome. + addition of some tests for rewriting (one being related to commit 14217) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14222 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18r14204 and 14218 continued: completely removing test for bug #2490,herbelin
leaving the decision of what to do with it to Matthieu; sorry for the confusion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14219 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Partial backtrack on wrong r14204: bug #2490 still open.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14218 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-14Regression files for bugs #2304 and #2490.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14204 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-14Fixing bug #2181 (Class mechanism can create dependencies over unnamedherbelin
fields of records). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14201 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-15Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14124 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
Stop using hnf_constr in unify_type, which might unfold constants that are marked opaque for unification. Conflicts: pretyping/unification.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14092 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-21Some fixes of the test-suite scriptsletouzey
In particular, the Fail meta-command cannot for the moment catch a Syntax Error, which is raised by Vernac.parse_sentence, before we even now that the line starts by a Fail... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13847 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-08Correct handling of existential variables when multiple differentmsozeau
instances of the lemma are rewritten at once. Cleanup dead code and put the problematic cases in the test-suite. Also fix some test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13813 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-12Adding test-case for bug #2362, which uses HO unification duringmsozeau
typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13533 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-12Fix bug #2393: allow let-ins inside telescopes (only fails when there'smsozeau
no undefined variables in the context now). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13532 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-11Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingherbelin
on unsupported unicode character) + forbidding unsupported unicode in Notation declarations too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13526 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-20Fixed test of bug #2360 (use of Fail to check a regular error insteadherbelin
of an anomaly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13442 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-19Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weherbelin
revert the catch of anomalies in reductionops.ml now (commit 13353)? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13439 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
too late, in a global environment which was no longer the correct one, leading to the failure of error printing (hence an anomaly) in case the command modified the state in several steps. Now, errors raised by vernac commands are processed in the same (intermediate) state they were raised from, just before rolling back to the original state. that modify the state in several Now, errors raised by vernac commands that modify the state in several steps (say S1, S2, ..., Sn) are processed in the state they were produced in (S1, S2, ... Sn-1), git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-02fixed bug #2375 (congruence)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13399 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30Updated test on Nsatz after Loïc moved NsatzR to Nsatz.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13361 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-29test-case for bug #2105barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13352 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13337 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-21Backporting fix to bug #2353 (fixpoint with recursively non-uniformherbelin
parameters) to branch 8.2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13302 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-21Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13301 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13225 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-26Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.herbelin
Fixing tests 2145.v about Nsatz. Adding nsatz target in Makefile. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13203 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-20Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13172 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18add in test-suite the scripts about fsetdec bugsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13165 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-16test for bug #2141 (include + extraction)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13160 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Fixing bug 2295 (omission of option "as" in return clause of "match" was notherbelin
working with section/goal variables). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13131 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).herbelin
By the way, there is an open problem of which conversion to use (conv, evarconv, with or w/o universes levels) when trying to unify multiple instances of the same variable in ltac pattern-matching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13130 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withherbelin
metas in return predicate of "match"); propagated protection for #2310 ("refine" problem with dependent metas of higher-order type) in v8.3 to v8.2. Everything goes well in trunk thanks for the new proof engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13129 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"herbelin
by a regular error in v8.3. Example behaves better in trunk thanks to new proof engine. In fact, there are two distinct solutions to a unification problem: should "refine" commit to one of them or leave the problem open? For trunk, improved the unification error message by enforcing nf_evar (but at some time, nf_evar in error messages should move to himsg because it is costly when errors are used for backtracking). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13127 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
- made the example work (a call to whd_meta was missing) - replaced the internal error messages of w_unify_to_subterm_list into user-understandable messages - incidentally fixed the meaning of whd_meta (which now takes an evd) and meta_name (which now does what it means and do not treat differently the instantiated metas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13122 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Added regression tests for bugs + miscellaneous improvementsherbelin
- #2095 (not fixed in v8.2 but fixed in v8.3 and trunk) - #2108 (fixed in v8.2, v8.3, trunk) - #2102 (moved warning to msg_warning to ensure flushing, but still open enhancement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13121 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Fixed bug # 2303 in r 13087.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13104 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
products as implicit if they're part of a term and not a type (issue a warning instead). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13101 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Automatic introduction of names given before ":" in Lemma's andherbelin
Definition's is not so painless. It seems to however generally provide "nicer" scripts so let us keep it and update the contribs and test-suite accordingly. Also enforced that the actual introduced names to be exactly as given in the statements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13097 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-15 00:01:59 +0000