aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Collapse)AuthorAge
* Adapted test file for About.Gravatar Pierre Courtieu2014-12-15
|
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
|
* Tests for Searchxxx commands added and modified.Gravatar Pierre Courtieu2014-12-15
|
* Adapting output tests to current naming of evars, even if unclearGravatar Hugo Herbelin2014-11-11
| | | | where it will eventually stabilize.
* Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Gravatar Hugo Herbelin2014-11-06
|
* Fixing clash in output test-suite Cases.Gravatar Hugo Herbelin2014-10-23
|
* Taking into account factorization of consecutive names of same typesGravatar Hugo Herbelin2014-10-23
| | | | | | | | | | | | 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.
* Fixing typo in output test Notations.Gravatar Hugo Herbelin2014-10-22
|
* Adapting output tests to the removal of the new token warning and toGravatar Hugo Herbelin2014-10-21
| | | | the printing of the context of open evars in Check.
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
| | | | | | | | | | | 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.
* Adapting output/Arguments_renaming continued.Gravatar Hugo Herbelin2014-10-03
|
* An evar name changed in output test.Gravatar Hugo Herbelin2014-10-02
|
* Adapting the output test Notations:Gravatar Hugo Herbelin2014-10-02
| | | | | | - unbound variables in notation are allowed, forcing only parsing mode - plus and mult are now themselves abbreviations - evars are named
* Revert "test-suite: New names for vars but the expected invariant is preserved"Gravatar Hugo Herbelin2014-10-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Adapting output/Arguments_renaming.out after fixing printing ofGravatar Hugo Herbelin2014-10-02
| | | | | constants which without a @ would have a maximally inserted implicit argument.
* Adapting to naming of evars.Gravatar Hugo Herbelin2014-09-27
|
* Reductionops: (Co)Fixpoints are always refolded during iotaGravatar Pierre Boutillier2014-09-18
|
* Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.Gravatar Hugo Herbelin2014-09-15
|
* Grammar: "avoiding to" isn't proper, eitherGravatar Jason Gross2014-08-25
|
* Upgrading output tests.Gravatar Hugo Herbelin2014-08-12
| | | | | | | | | | | | 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
* Fixing output test-suite.Gravatar Pierre-Marie Pédrot2014-07-21
|
* cbn understand ! Arguments directiveGravatar Pierre Boutillier2014-06-04
| | | | | Of course, this is an under approximation of the expected behavior : unfolding a constant iff a leaf of its underlying split-tree is reached.
* Fixing output test-suite: since universe polymorphism, the Print commandGravatar Pierre-Marie Pédrot2014-05-08
| | | | shows the polymorphism status of the term.
* Fixing #3293 (eta-expansion at "match" printing time was failingGravatar Hugo Herbelin2014-04-28
| | | | because of let-in's interpreted as being part of the expansion).
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
| | | | reserved with Implicit Type.
* test-suite: opaque term -> opaque proofGravatar Pierre Boutillier2014-02-28
|
* test-suite: New names for vars but the expected invariant is preservedGravatar Pierre Boutillier2014-02-28
|
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
|
* test-suite/output/Notations : evar number changeGravatar Pierre Boutillier2013-12-19
|
* Test suite: update output reference.Gravatar xclerc2013-12-02
|
* Print logical name rather than path (thus allowing reproducible tests).Gravatar xclerc2013-12-02
|
* test-suite fixupGravatar pboutill2013-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing 2 output test-suites.Gravatar ppedrot2013-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing some tests from the test-suite.Gravatar ppedrot2013-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16760 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix testsuite so that it works with STMGravatar gareuselesinge2013-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16676 85f007b7-540e-0410-9357-904b9bb8a0f7
* better error message for unexpected renaming (closes #2987)Gravatar gareuselesinge2013-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16641 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating some output tests in test-suite:Gravatar herbelin2013-05-09
| | | | | | | | | | | | | | 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
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
| | | | | | 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
* Using Parameter instead of Variable in test-suite/outputGravatar herbelin2013-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuation of r16346 on filtering local definitions. RefinedGravatar herbelin2013-03-30
| | | | | | | | | | | | 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
* Evarconv: When doing a iota of a fixpoint, use constant name instead of ↵Gravatar pboutill2013-02-25
| | | | | | | | 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
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
| | | | | | | | 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
* Revised the Ltac trace mechanism so that trace breaking due toGravatar herbelin2013-02-17
| | | | | | | | | | | 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
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing parsing of specific primitive tokens used as notations for patternsGravatar herbelin2012-12-18
| | | | | | (e.g. 1 for eq_refl). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16094 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revised the strategy for automatic insertion of spaces when printingGravatar herbelin2012-12-04
| | | | | | | | | 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
* Update output/Search.out after hint-related extra defs in PeanoGravatar letouzey2012-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15980 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
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 04:03:02 +0000