aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Collapse)Author
2015-10-22Fixing a bug in reporting ill-formed inductive.Hugo Herbelin
Was introduced in b06d3badb (15 Jul 2015).
2015-10-11Fixing test-suiteHugo Herbelin
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables.
2015-10-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo Herbelin
which was broken after it became possible to have binding names themselves bound to ltac variables (2fcc458af16b). Interpretation was corrected, but error message was damaged.
2015-09-15Test for bug #4269.Pierre-Marie Pédrot
2015-09-03Update test-suite after 518049fe7.Maxime Dénès
"Fetching opaque proofs" notices are not printed by default anymore.
2015-07-27Output test for bug #2169.Pierre-Marie Pédrot
2015-06-24Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.Maxime Dénès
2015-03-09Do not display the status of monomorphic constants unless in ↵Guillaume Melquiond
universe-polymorphism mode.
2015-03-05Fix testsuite with respect to the new formatting of Fail messages.Guillaume Melquiond
2015-02-15Undo: back to 8.4 semantics (Close #3514)Enrico Tassi
Only tactics are taken into account.
2015-01-12Fixing name of evars in output test Notation.v.Hugo Herbelin
2014-12-15Adapted test file for About.Pierre Courtieu
2014-12-15About now accepts hypothesis names and goal selector.Pierre Courtieu
2014-12-15Tests for Searchxxx commands added and modified.Pierre Courtieu
2014-11-11Adapting output tests to current naming of evars, even if unclearHugo Herbelin
where it will eventually stabilize.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 14:23:58 +0000