diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-02 11:31:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-02 16:17:20 +0200 |
| commit | 8a382c1906728f89b13d20f541137a670d2c3c75 (patch) | |
| tree | f4a59ff8aa4762c3c67ba6360909e2a191eff385 /test-suite/output/Arguments_renaming.out | |
| parent | 0e5c76991d9159bc182baf65d7d44f135c8dfeea (diff) | |
Adapting output/Arguments_renaming.out after fixing printing of
constants which without a @ would have a maximally inserted implicit
argument.
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index c99dfc018..dbc1b4a21 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -6,7 +6,7 @@ The command has indeed failed with message: Argument A renamed to T. @eq_refl : forall (B : Type) (y : B), y = y -eq_refl +@eq_refl nat : forall x : nat, x = x Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x @@ -63,7 +63,7 @@ The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.Test1.myplus -myplus +@myplus : forall Z : Type, Z -> nat -> nat -> nat Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x |