When printing the type in About, use the renamed arguments.

2 files changed, 9 insertions, 9 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
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index d84165d032..722a27c432 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -75,12 +75,12 @@ let print_ref reduce ref udecl =
   let inst = Univ.make_abstract_instance univs in
   let bl = Printer.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
-  let typ = EConstr.of_constr typ in
   let typ =
     if reduce then
-      let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
-      in EConstr.it_mkProd_or_LetIn ccl ctx
+      let ctx,ccl = Reductionops.splay_prod_assum env sigma (EConstr.of_constr typ)
+      in EConstr.to_constr sigma (EConstr.it_mkProd_or_LetIn ccl ctx)
     else typ in
+  let typ = Arguments_renaming.rename_type typ ref in
   let impargs = select_stronger_impargs (implicits_of_global ref) in
   let impargs = List.map binding_kind_of_status impargs in
   let variance = let open GlobRef in match ref with
@@ -95,7 +95,7 @@ let print_ref reduce ref udecl =
     else mt ()
   in
   let priv = None in (* We deliberately don't print private univs in About. *)
-  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma ~impargs typ ++
+  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma ~impargs typ ++
          Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv)
 
 (********************************)