diff options
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 10 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 4 |
2 files changed, 13 insertions, 1 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 diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 7ceaa5a1bc..8b00484b4a 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -341,7 +341,9 @@ let print_arguments ref = let open Constrexpr in let open Vernacexpr in [Ppvernac.pr_vernac_expr - (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))] + (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags)) ++ + (if renames = [] then mt () else + fnl () ++ str " (where some original arguments have been renamed)")] let print_name_infos ref = let type_info_for_implicit = |