diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-21 18:05:41 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-21 18:05:41 +0000 |
| commit | 5d9d019b1978f1a3ebb8429fcf23d8da9bf52212 (patch) | |
| tree | 036fc4e6de72614a641c38adfa1104fa78dc3c7f /test-suite/output/PrintInfos.out | |
| parent | 440af48253bb8b9870c78e1392f0c7a10c23feee (diff) | |
Some fixes of the test-suite scripts
In particular, the Fail meta-command cannot for the moment catch a Syntax Error,
which is raised by Vernac.parse_sentence, before we even now that the line starts
by a Fail...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13847 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/PrintInfos.out')
| -rw-r--r-- | test-suite/output/PrintInfos.out | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 19d7e7c68..d60c8097c 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -17,17 +17,26 @@ Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted -For eq_refl: Argument A is implicit +For eq_refl, when applied to no arguments: + Arguments A, x are implicit and maximally inserted +For eq_refl, when applied to 1 argument: + Argument A is implicit For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x -Argument A is implicit +When applied to no arguments: + Arguments A, x are implicit and maximally inserted +When applied to 1 argument: + Argument A is implicit Argument scopes are [type_scope _] Expands to: Constructor Coq.Init.Logic.eq_refl eq_refl : forall (A : Type) (x : A), x = x -Argument A is implicit +When applied to no arguments: + Arguments A, x are implicit and maximally inserted +When applied to 1 argument: + Argument A is implicit plus = fix plus (n m : nat) : nat := match n with | 0 => m @@ -43,7 +52,6 @@ plus is transparent Expands to: Constant Coq.Init.Peano.plus plus : nat -> nat -> nat -No implicit arguments plus_n_O : forall n : nat, n = n + 0 Argument scope is [nat_scope] |