diff options
| author | Hugo Herbelin | 2020-08-22 12:51:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 9cb28c30955db553f5e2b7abe7633dec97fa9dae (patch) | |
| tree | 49aea4f8b9d10405a2b76e6ccfdab7049cae7e74 /test-suite | |
| parent | 1a91771fdc26bd0260ff26aceb91070217717d3b (diff) | |
Do not write "rename" for arguments in About, since these arguments are validated.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index a5858fb056..8cc4383f49 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -23,11 +23,11 @@ Expands to: Constructor Coq.Init.Logic.eq_refl 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 +Arguments myrefl {C}%type_scope x _ myrefl : forall {C : Type} (x : A), C -> myEq C x x myrefl is not universe polymorphic -Arguments myrefl {C}%type_scope x _ : rename +Arguments myrefl {C}%type_scope x _ Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := @@ -37,11 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -52,11 +52,11 @@ Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x Arguments myEq (_ _)%type_scope _ _ -Arguments myrefl A%type_scope {C}%type_scope x _ : rename +Arguments myrefl A%type_scope {C}%type_scope 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 +Arguments myrefl A%type_scope {C}%type_scope x _ Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x @@ -68,11 +68,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent |