diff options
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 533e64f5b4..a5858fb056 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -15,7 +15,7 @@ Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x Arguments eq {A}%type_scope _ _ Arguments eq_refl {B}%type_scope {y}, [B] _ -eq_refl : forall {A : Type} {x : A}, x = x +eq_refl : forall {B : Type} {y : B}, y = y eq_refl is not universe polymorphic Arguments eq_refl {B}%type_scope {y}, [B] _ @@ -24,7 +24,7 @@ Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x Arguments myEq _%type_scope _ _ Arguments myrefl {C}%type_scope x _ : rename -myrefl : forall {B : Type} (x : A), B -> myEq B x x +myrefl : forall {C : Type} (x : A), C -> myEq C x x myrefl is not universe polymorphic Arguments myrefl {C}%type_scope x _ : rename @@ -38,7 +38,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := : forall T : Type, T -> nat -> nat -> nat Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall {T : Type}, T -> nat -> nat -> nat +myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename @@ -53,7 +53,7 @@ Inductive myEq (A B : Type) (x : A) : A -> Prop := Arguments myEq (_ _)%type_scope _ _ Arguments myrefl A%type_scope {C}%type_scope x _ : rename -myrefl : forall (A : Type) {B : Type} (x : A), B -> myEq A B x x +myrefl : forall (A : Type) {C : Type} (x : A), C -> myEq A C x x myrefl is not universe polymorphic Arguments myrefl A%type_scope {C}%type_scope x _ : rename @@ -69,7 +69,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := : forall T : Type, T -> nat -> nat -> nat Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall {T : Type}, T -> nat -> nat -> nat +myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename |