aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Collapse)Author
2014-11-06Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Hugo Herbelin
2014-10-23Fixing clash in output test-suite Cases.Hugo Herbelin
2014-10-23Taking into account factorization of consecutive names of same typesHugo Herbelin
in goal context. Note: printing of a declaration was previously done in the context made of the preceding segment of hypotheses, while now it is made in the full context of all hyps (those coming before and after the hyp being printed). As a consequence, constants which could be confused with a variable in the context are now always qualified even if the conflicting variable name is coming later. But why not, that looks somehow more uniform like this.
2014-10-22Fixing typo in output test Notations.Hugo Herbelin
2014-10-21Adapting output tests to the removal of the new token warning and toHugo Herbelin
the printing of the context of open evars in Check.
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
but the internal representation dropped let-in. Ideally, the internal representation of the "match" should use contexts for the predicate and the branches. This would however be a rather significant change. In the meantime, just a hack. To do, there is still an extra @ in the constructor name that does not need to be there.
2014-10-03Adapting output/Arguments_renaming continued.Hugo Herbelin
2014-10-02An evar name changed in output test.Hugo Herbelin
2014-10-02Adapting the output test Notations:Hugo Herbelin
- unbound variables in notation are allowed, forcing only parsing mode - plus and mult are now themselves abbreviations - evars are named
2014-10-02Revert "test-suite: New names for vars but the expected invariant is preserved"Hugo Herbelin
This reverts commit cc06ffe3df0ecc023ad046a085b0751ed4161cbf. Going back to the convention of naming bound variables in hypotheses of the goal as in 8.4. My arguments for the revert are: - apply ... with (id:=...) would have to be changed too, then possibly breaking the compatibility - the naming became dependent of the order of variables as in x:nat H:forall x0, x0=0 ===== goal but H:forall x, x=0 x:nat ===== goal Accordingly, this is all a matter of convention, since the meaning of bindings is anyway the same in both cases.
2014-10-02Adapting output/Arguments_renaming.out after fixing printing ofHugo Herbelin
constants which without a @ would have a maximally inserted implicit argument.
2014-09-27Adapting to naming of evars.Hugo Herbelin
2014-09-18Reductionops: (Co)Fixpoints are always refolded during iotaPierre Boutillier
2014-09-15Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Hugo Herbelin
2014-08-25Grammar: "avoiding to" isn't proper, eitherJason Gross
2014-08-12Upgrading output tests.Hugo Herbelin
output/Arguments.v output/ArgumentsScope.v output/Arguments_renaming.v output/Cases.v output/Implicit.v output/PrintInfos.v output/TranspModType.v Main changes: monomorphic -> not universe polymorphic, Peano vs Nat
2014-07-21Fixing output test-suite.Pierre-Marie Pédrot
2014-06-04cbn understand ! Arguments directivePierre Boutillier
Of course, this is an under approximation of the expected behavior : unfolding a constant iff a leaf of its underlying split-tree is reached.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:58:06 +0000