aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* test-suite: Local Tactic Notation is now legal since r15731Gravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15757 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more coqtop.opt, produce directly a coqtop binaryGravatar letouzey2012-08-23
| | | | | | | | | | | 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
* Unification in Evar_conv uses an abstract machine stateGravatar pboutill2012-08-09
| | | | | | | | | 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
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #2836 (materialize_evar might refine as a side effect theGravatar herbelin2012-07-29
| | | | | | | | | | | 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
* Fixing bug #2835 (the rationale for printing notations was notGravatar herbelin2012-07-21
| | | | | | standard under lambdas and products). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving management of notations with binders (see #2708 where aGravatar herbelin2012-07-21
| | | | | | | 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
* Restore test file induct.v where the "in |- *" is mandatoryGravatar letouzey2012-07-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15585 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r15459: it helps testing occur-check early in someGravatar herbelin2012-07-06
| | | | | | | | | 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
* Minor fixes in the test-suite after my recent commitsGravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15542 85f007b7-540e-0410-9357-904b9bb8a0f7
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
| | | | | | | | | 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
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
| | | | | | | 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
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | - 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
* Fixing bug #2817 (occur check was not done up to instantiation ofGravatar herbelin2012-06-20
| | | | | | 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
* Fixing bug #2809 (anomaly when printing a module with notations due toGravatar herbelin2012-06-20
| | | | | | | 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
* Proof using: nested sections bugfixGravatar gareuselesinge2012-06-18
| | | | | | | | | | | | | | 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
* Constrextern is allow to use partially applied notationsGravatar pboutill2012-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing test-suite after last storm in Pp.Gravatar pboutill2012-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.Gravatar ppedrot2012-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notations are back in the "in" clause of pattern matching.Gravatar pboutill2012-05-15
| | | | | | Fixes the test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit arguments of Definition are taken from the type when given by the user.Gravatar pboutill2012-04-27
| | | | | | 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
* remove undocumented and scarcely-used tactic auto decompGravatar letouzey2012-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2733 : { } implicits and FixpointsGravatar pboutill2012-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15187 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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
* Repair two testsGravatar letouzey2012-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
| | | | | | | | | | | | | | | | | | | | | | | | - 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
* Relax uniform inheritance conditionGravatar gareuselesinge2012-04-05
| | | | | | | 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
* Unification: Added a heuristic to solve problems of the formGravatar herbelin2012-03-26
| | | | | | | | | | | | | | | | | | ?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
* Fix the test-suite by removing any Reset in the scriptsGravatar letouzey2012-03-23
| | | | | | | | 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
* evarconv: MaybeFlex/MaybeFlex case infers more Canonical StructuresGravatar gareuselesinge2012-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Fixing bug #2724 (using notations with binders in cases patternsGravatar herbelin2012-03-20
| | | | | | 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
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The optimisation done of Namegen.visibly_occur_id did not preserve the previous behavior when pr_constr/constr_extern/detype were called on a term with free rel variables. We backtrack on it to go back to the 8.2 behavior. Seized this opportunity to clarify the meaning of the at_top flag in constrextern.ml and printer.ml and to rename it into goal_concl_style. The badly-named at_top flag was introduced in Coq 6.3 in 1999 to mean that when printing variables bound in the goal, names had to avoid the names of the variables of the goal context, so as to keep naming stable when using "intro"; in r4458, printing improved by not avoiding names that were short names of global definitions, e.g. "S", or "O" (except when the at_top flag was on for compatibility reasons). Other printing strategies could be possible in the non-goal-concl-style mode. For instance, all bound variables could be made distinct in a given expression, even if no clash occur, therefore following so-called Barendregt's convention. This could be done by setting "avoid" to "ids_of_rel_context (rel_context env)" in extern_constr and extern_type (and then, Namegen.visibly_occur_id could be re-simplified again!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized the use of evar candidates in type inference unification:Gravatar herbelin2012-03-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
| | | | | | | | | | | - reinstall (x : T | P) binder syntax extension. - fix a wrong Evd.define in coercion code. - Simplify interface of eterm_obligations to take a single evar_map. - Fix a slightly subtle bug related to resolvability of evars: some were marked unresolvable and never set back to resolvable across calls to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | "f atomic_tac" as a short-hand for "f ltac:(atomic_tac)" for "f" an Ltac function - see Tacinterp.add_primitive_tactic). More precisely, when parsing "f ref" and "ref" is recognized as the name of some TACTIC-EXTEND-defined tactic parsable as an atomic tactic (like "eauto", "firstorder", "discriminate", ...), the code was correct only when a rule of the form `TACTIC EXTEND ... [ "foo" -> ...] END' was given (where "foo" has no arguments in the rule) but not when a rule of the form `TACTIC EXTEND ... [ "foo" tactic_opt(p) -> ...] END' was given (where "foo" had an optional argument in the rule). In particular, "firstorder" was in this case. More generally, if, for an extra argument able to parse the empty string, a rule `TACTIC EXTEND ... [ "foo" my_special_extra_arg(p) -> ...] END' was given, then "foo" was not recognized as parseable as an atomic string (this happened e.g. for "eauto"). This is now also fixed. There was also another bug when the internal name of tactic was not the same as the user-level name of the tactic. This is the reason why "congruence" was not recognized when given as argument of an ltac (its internal name is "cc"). Incidentally removed the redundant last line in the parsing rule for "firstorder". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
| | | | | | | | did not handle let-ins and was wrongly specified). Thanks to Pierre Boutillier and Pierre-Marie Pédrot for pointing out the source of the bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15027 85f007b7-540e-0410-9357-904b9bb8a0f7
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02
| | | | | | | | This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf. An other wrong externalize function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use a heuristic to not simplify equality hypotheses remaining after ↵Gravatar msozeau2012-02-20
| | | | | | | | dependent induction if they don't look really trivial. We still are making a choice though. Fixes bug #2712. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arguments supports extra notation scopesGravatar gareuselesinge2012-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix consequence of pp bugfix in testsuiteGravatar pboutill2012-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14954 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix simplification of ind. hyps., recognized by a [block] in their type (bug ↵Gravatar msozeau2012-01-28
| | | | | | #2674) and properly clear [block] at end of simplification (bug #2691). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notations with binders: Accepting using notations for functional termsGravatar herbelin2012-01-20
| | | | | | | which do not necessarily depend on their parameter (e.g. a notation for "fun x => t" might match also "fun _ => t"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14926 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parameters in pattern first step.Gravatar pboutill2012-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In interp/constrintern.ml, '_' for constructor parameter are required if you use AppExpl ('@Constr') and added in order to be erased at the last time if you do not use '@'. It makes the use of notation in pattern more permissive. For example, -8<------ Inductive I (A: Type) : Type := C : A -> I A. Notation "x <: T" := (C T x) (at level 38). Definition uncast A (x : I A) := match x with | x <: _ => x end. -8<------ was forbidden. Backward compatibility is strictly preserved expect for syntactic definitions: While defining "Notation SOME = @Some", SOME had a special treatment and used to be an alias of Some in pattern. It is now uniformly an alias of @Some ('_' must be provided for parameters). In interp/constrextern.ml, except if all the parameters are implicit and all the arguments explicit (This covers all the cases of the test-suite), pattern are generated with AppExpl (id est '@') (so with '_' for parameters) in order to become compatible in any case with future behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14909 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add distclean back to test-suite/MakefileGravatar glondu2012-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtracking on r14876 (fix for bug #2267): extra scopes might beGravatar herbelin2012-01-05
| | | | | | | useful in the presence of coercions to Funclass. Fixed the bug differently. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Arguments Scope bug when too many scopes are given (bug #2667).Gravatar herbelin2012-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Type inference unification: fixed a 8.4 bug in the presence of unificationGravatar herbelin2012-01-04
| | | | | | with evars under binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arguments: check rename even if no implicit is specifiedGravatar gareuselesinge2011-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14827 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 09:28:38 +0000