diff options
| author | Hugo Herbelin | 2020-08-27 14:48:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | d07d14dfd82cd08564ef0513c23236d73a67664f (patch) | |
| tree | f0584509b4390135114e417a37b0c60c41a289eb /test-suite/output | |
| parent | 4b9a823c03b61034e0fde76716a8623ff68977b0 (diff) | |
About: Add a mention that arguments have been renamed, if ever it is the case.
See https://github.com/coq/coq/pull/12875#issuecomment-679190489.
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index d56cd4d610..e46774f68a 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -15,19 +15,23 @@ Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x Arguments eq {A}%type_scope _ _ Arguments eq_refl {B}%type_scope {y}, [_] _ + (where some original arguments have been renamed) eq_refl : forall {B : Type} {y : B}, y = y eq_refl is not universe polymorphic Arguments eq_refl {B}%type_scope {y}, [_] _ + (where some original arguments have been renamed) 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 _ + (where some original arguments have been renamed) myrefl : forall {C : Type} (x : A), C -> myEq C x x myrefl is not universe polymorphic Arguments myrefl {C}%type_scope x _ + (where some original arguments have been renamed) Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := @@ -38,10 +42,12 @@ 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 + (where some original arguments have been renamed) myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z}%type_scope !t (!n m)%nat_scope + (where some original arguments have been renamed) The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -53,10 +59,12 @@ Inductive myEq (A B : Type) (x : A) : A -> Prop := Arguments myEq (_ _)%type_scope _ _ Arguments myrefl A%type_scope {C}%type_scope x _ + (where some original arguments have been renamed) 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 _ + (where some original arguments have been renamed) Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x @@ -69,10 +77,12 @@ 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 + (where some original arguments have been renamed) myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z}%type_scope !t (!n m)%nat_scope + (where some original arguments have been renamed) The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent |