diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 1e3cc37df4..3488cb3056 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -6,8 +6,10 @@ Error: To rename arguments the "rename" flag must be specified. Argument A renamed to T. @eq_refl : forall (B : Type) (y : B), y = y -@eq_refl nat - : forall x : nat, x = x +eq_refl + : ?y = ?y +where +?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq_refl: Arguments are renamed to B, y |