aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Collapse)Author
2014-05-08Fixing output test-suite: since universe polymorphism, the Print commandPierre-Marie Pédrot
shows the polymorphism status of the term.
2014-04-28Fixing #3293 (eta-expansion at "match" printing time was failingHugo Herbelin
because of let-in's interpreted as being part of the expansion).
2014-03-01Never suppress the typing constraint of bound variables whose name wasPierre-Marie Pédrot
reserved with Implicit Type.
2014-02-28test-suite: opaque term -> opaque proofPierre Boutillier
2014-02-28test-suite: New names for vars but the expected invariant is preservedPierre Boutillier
2014-02-28Fix output test-suite 'simpl tactic' -> 'reduction tactics'Pierre Boutillier
2013-12-19test-suite/output/Notations : evar number changePierre Boutillier
2013-12-02Test suite: update output reference.xclerc
2013-12-02Print logical name rather than path (thus allowing reproducible tests).xclerc
2013-11-03test-suite fixuppboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17046 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-08Fixing 2 output test-suites.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16863 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-03Fixing some tests from the test-suite.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16760 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Fix testsuite so that it works with STMgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16676 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-29better error message for unexpected renaming (closes #2987)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16641 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Updating some output tests in test-suite:herbelin
InitSyntax, PrintInfos: consequence of r16467 which improved printing of sigT Notations2: consequence of r16470 on using notations while asked to print the body of an abbreviation Notations: fix from r16417 was incomplete (and by the way associated to a wrong commit message) names: related to commit r16205 which aligned "In environment" with the variables of the environment (maybe should it be better to still have "In environment" printed after "Error: " but I don't know how to do it with a forced newline). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16503 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Using Parameter instead of Variable in test-suite/outputherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16417 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-30Continuation of r16346 on filtering local definitions. Refinedherbelin
the "choose less dependent" constraint-solving heuristic so that it is not disturbed by local definitions. This is a quick fix. A deeper analysis of the structure of constraints of the form ?x[args] = y, determining if variable y can itself be a local def or not, and whether args can be let-ins aliasing other variables, would allow to know if the fix needs to be refined further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16376 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-25Evarconv: When doing a iota of a fixpoint, use constant name instead of ↵pboutill
fixpoint definition + Help the use of #trace on evar_conv_appr_x git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16244 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
interleaving of ltac and ml code is not visible (this particularly applies to ltac notation ring, which calls ml-level ring_lookup and Ring again at the ltac level, resulting in non-localisation of "ring" errors). Added also missing LtacLocated checks in Class_instance and Proofview. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16204 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-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-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-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-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-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-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-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-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
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
2012-03-02Noise for nothingpboutill
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
2012-02-14Arguments supports extra notation scopesgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14977 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-31Fix consequence of pp bugfix in testsuitepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14954 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Notations with binders: Accepting using notations for functional termsherbelin
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
2012-01-16Parameters in pattern first step.pboutill
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
2011-12-19Arguments: check rename even if no implicit is specifiedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14827 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Command Arguments: standardizing format of error messages and American spelling.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Bypassing the use of (currently unimplemented) "Show Script" in testsherbelin
that used it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14802 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-07Adapting test Existentials to new numbering strategy of evars (r14764).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14777 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Minor fixes to Argumentsgareuselesinge
- Implicit arguments can be mentioned anonymously: Arguments map {_ _} f l. - To rename implicit arguments, the ": rename" flag must be used: Arguments map {T1 T2} f l : rename. Without the ": rename" flag arguments can be used to assert that a function has indeed the expected number of arguments and that the arguments are named as expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-04A small test for type inference (used to be a regression at some time).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14759 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-04Fixing superflous newline in output of About when no parameter is renamed.herbelin
Fixing output tests after having added flushing of warning in revisions 14747 and 14750. Moving Implicit output test to new command Arguments. Adding test of new Arguments syntax in PrintInfos.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14758 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Renamig support added to "Arguments"gareuselesinge
Example: Arguments eq_refl {B y}, [B] y. Check (eq_refl (B := nat)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14719 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21New Arguments vernaculargareuselesinge
The new vernacular "Arguments" attaches to constants the extra-logical piece of information regarding implicit arguments, notation scopes and the behaviour of the simpl tactic. The About vernacular is extended to print the new extra logical data for simpl. Examples: Arguments foo {A B}%type f [T] x. (* declares A B and T as implicit arguments, A B maximally inserted. declares type_scope on A and B *) Arguments foo {A%type b%nat} p%myscope q. (* declares A and b as maximally inserted implicit arguments. declares type_scope on A, nat_scope on b and the scope delimited by myscope on p *) Arguments foo (A B)%type c d. (* declares A and b in type_scope, but not as implicit arguments. *) Arguments foo A B c. (* leaves implicit arguments and scopes declared for foo untouched *) Arguments foo A B c : clear implicits (* equivalente too Implicit Arguments foo [] *) Arguments foo A B c : clear scopes (* equivalente too Arguments Scope foo [_ _ _] *) Arguments foo A B c : clear scopes, clear implicits Arguments foo A B c : clear implicits, clear scopes Arguments foo A B c : clear scopes and implicits Arguments foo A B c : clear implicits and scopes (* equivalente too Arguments Scope foo [_ _ _]. Implcit Arguments foo [] *) Arguments foo A B c : default implicits. (* equivalent to Implicit Arguments foo. *) Arguments foo {A B} x , A [B] x. (* equivalent to Implicit Arguments foo [[A] [B]] [B]. *) Arguments foo a !b c !d. (* foo is unfolded by simpl if b and d evaluate to a constructor *) Arguments foo a b c / d. (* foo is unfolded by simpl if applied to 3 arguments *) Arguments foo a !b c / d. (* foo is unfolded by simpl if applied to 3 arguments and if b evaluates to a constructor *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14717 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ↵letouzey
#2168) We replace Global.lookup_constant by our own code that looks for a module and enters its implementation. This is still preliminary work, I would prefer to understand more completely the part about module substitutions when entering an applied functor. But this code already appears to work quite well. Anyway, since we only search for constants, we don't need to reconstitute a 100% accurate environment, as long as the same objects are in it. Note: - Digging inside module structures is slower than just using Global.lookup_constant. Hence we try to avoid it as long as we could. Only in front of axioms (or in front of constant unknown to Global) do we check whether we have an inner-module implementation for this constant. There is some memoization of the search for internal structure_body out of a module_path. - In case of inner-module axioms, we might not be able to print its type, but only its long name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-22test-suite : an additional message displayed by Notation2.vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14485 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-22Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.letouzey
Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14484 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 10:59:17 +0000