diff options
Diffstat (limited to 'test-suite/output')
| -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 |