aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2013-01-21Fix bug 2958: Inductive deep in in clause are impossiblepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16133 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-21Last test-suite not in Symmetric Patterns syntaxpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16132 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-12-18Fixing parsing of specific primitive tokens used as notations for patternsherbelin
(e.g. 1 for eq_refl). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16094 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Taking into account the possibility of having a type of type which isherbelin
an evar in typing.ml. Thanks to HoTT people for noticing the problem. Fixed behavior of e_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16092 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
different instances of a meta are checked against full conversion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16086 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Backtrack on activating scopes with type casts (was r15978).herbelin
IT happens that there are some other uses of casts, e.g. in nat_int de MathClasses which uses a notation 0 for some class constructor zero, and a cast (0:nat) to force this notation 0 to represent the instance O in nat of the class of types having a zero (eventually, 0, i.e. "zero nat O" and "O" are convertible but the information of being a class instance is lost). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16024 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Revised the strategy for automatic insertion of spaces when printingherbelin
notations: - hopefully never 2 spaces when the user did not ask for - more systematic default insertion of spaces around symbols - e.g. have space before "[" if after a non-terminal - have spaces between consecutive terminals git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16019 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-28Evarconv: Fix #2936 + commentspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16011 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-11-21Fixing test-suite: Scope.vppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15990 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-18Hurkens' paradox on Type (r15973 and r15977) needs two (non-Set)herbelin
universes. As it uses eq_rect on Type(2), the arguments of eq_rect has to be in Type(3) and compiling the standard library now needs one more universe! If needed, we could avoid this by inlining the definition of (eq_rect Type2) in Hurkens.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15981 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-17Update output/Search.out after hint-related extra defs in Peanoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15980 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
type in "cast" to activate the temporary interpretation scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Fix test-suite output/* in benchpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15906 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-04test-suite: fix grep rule for output testspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15770 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-04test-suite uses coqtop instead of coqtop.bytepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15769 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24In the output tests, ignore dynlink messagesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15767 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23test-suite: Local Tactic Notation is now legal since r15731letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15757 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more coqtop.opt, produce directly a coqtop binaryletouzey
We now always produce two binaries, coqtop and coqtop.byte : - If ocamlopt is available, coqtop is directly what used to be coqtop.opt, no more symlinks needed. - Otherwise, coqtop is a copy of coqtop.byte. The same for coqchk and coqide... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15752 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
It uses a term in front of a stack instead of a term in front of a list of applied terms. From outside of eq_appr_x nothing should have changed. Nasty evar instantiation bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15719 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 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-21Fixing bug #2835 (the rationale for printing notations was notherbelin
standard under lambdas and products). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15644 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-21Improving management of notations with binders (see #2708 where aherbelin
variable is used both as term and as binder, resulting in ununderstandable error message about scopes). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15642 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Restore test file induct.v where the "in |- *" is mandatoryletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15585 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-06Minor fixes in the test-suite after my recent commitsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15542 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 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-06-20Fixing bug #2809 (anomaly when printing a module with notations due toherbelin
bad interaction between lazy evaluation of pp streams and temporary effectful extension of global environment). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15457 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-18Proof using: nested sections bugfixgareuselesinge
It used to be the case that the list of declared section variables for a constant was taken into account only when discharging the first enclosing sections, but not any outer section. Example of the bug: Section A. Variable x : bool. Section B. Variable y : nat. Lemma foo : True. Proof using x y. Admitted. End B. End A. Check foo. (* nat -> True instead of bool -> nat -> True *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15445 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-14Constrextern is allow to use partially applied notationspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15440 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-12Fixing test-suite after last storm in Pp.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15433 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
Fixes the test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 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-23remove undocumented and scarcely-used tactic auto decompletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 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-04-06Fixing a few bugs (see #2571) related to interpretation of multiple bindersherbelin
- fixing missing spaces in the format of the exists' notations (Logic.v); - fixing wrong variable name in check_is_hole error message (topconstr.ml); - interpret expressions with open binders such as "forall x y, t" as "forall (x:_) (y:_),t" instead of "forall (x y:_),t" to avoid the "implicit type" of a variable being propagated to the type of another variable of different base name. An open question remains: when writing explicitly "forall (x y:_),t", should the types of x and y be the same or not. To avoid the "bug" that x and y have implicit types but the one of x takes precedences, I enforced the interpretation (in constrintern, not in parsing) that "forall (x y:_),t" means the same as "forall (x:_) (y:_),t". However, another choice could have been made. Then one would have to check that if x and y have implicit types, they are the same; also, glob_constr should ideally be changed to support a GProd and GLam with multiple names in the same type, especially if this type is an evar. On the contrary, one might also want e.g. "forall x y : list _, t" to mean "forall (x:list _) (y:list _), t" with distinct instanciations of "_" ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15121 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-05Relax uniform inheritance conditiongareuselesinge
Uniform inheritance is not always needed for the coercion mechanism to work. We turn it into a warning. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15117 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-26Unification: Added a heuristic to solve problems of the formherbelin
?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to know if it occurs in rigid position or not. Such equations typically come from matching problems such as "match a return ?T[a] with pair a1 a2 => a1 end" where, a is in type "?A * ?B", and, in the branch, the return clause, of the form "?T[pair ?A ?B a1 a2]", has to be unified with ?A. This possible dependency is kept since commits r15060-15062. The heuristic is to restrict ?T so that the dependency is removed, leading to a behavior similar to the one existing before these commits. This allows BGsection15.v, from contrib Ssreflect, to compile as it did before these commits. Also, removed one function exported without true need in r15061. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15092 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-23Fix the test-suite by removing any Reset in the scriptsletouzey
Reset and the other backtracking commands (Back, BackTo, Backtrack) are now allowed only during interactive session, not in compiled or loaded scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15087 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-22evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structuresgareuselesinge
Canonical Structure inference works on named terms only: i.e. the projection and the value must be named (with few exceptions). The set of named (head) terms is: (Var _|Construct _|Ind _|Const _|Prod _|Sort _) The set of unnamed is thus: (Case _|Fix _|CoFix _|Evar _|Meta _|Rel _) The MaybeFlex/MaybeFlex case, when no CS inference takes place, unfolds the rhs only if it exposes a named term. If it exposes an unnamed term, it tries to unfold on the lhs first. Note that unnamed terms are whd normal terms, since iota and zeta are performed by evar_apprec. So the algorithm behaves as before, but stops unfolding the rhs 1 delta step before it exposes an unnamed term. Then it starts unfolding the lhs. If the lhs exposes a rigid term the rhs is naturally unfolded, going back to same situation in which the algorithm was ending before. But while it unfolds on the left, the rhs is still named, and canonical structure inference can succeed. Ex failing before, the "canon_" prefix marks projections/values declared as canonical. Record test := K { canon_proj : nat } (* canon_proj x := math x with K y => y end *) canon_val x := match x with 0 => 0 | S m => m end Canonical Structure canon_struct x := K (canon_val x) (* aliases *) proj := canon_proj val := canon_val Old alg: proj ? ===?=== val x proj ? ===?=== canon_val x proj ? ===?=== match x with ... end canon_proj ? ===?=== match x with ... end (* no inference *) match ? with K x...end ===?=== match x with 0 ...end (* FAIL *) New alg: proj ? ===?=== val x proj ? ===?=== canon_val x canon_proj ? ===?=== canon_val x (* inference works: ? := canon_struct *) In case canon_struct is not declared for canon_proj and canon_val it continues like that: canon_proj ? ===?=== canon_val x match ? with K x...end ===?=== canon_val x match ? with K x...end ===?=== match x with 0 ...end (* FAIL *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15077 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-20Fixing bug #2724 (using notations with binders in cases patternsherbelin
was provoking an anomaly instead of a regular error). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15070 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 12:02:40 +0000