diff options
| author | Hugo Herbelin | 2020-08-22 12:50:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 1a91771fdc26bd0260ff26aceb91070217717d3b (patch) | |
| tree | 0aec8f289eb7da44dfb1e38f205282ebbc2804aa /vernac | |
| parent | 699eb941cbdd2b3caf98f18b2d49b249b598ca1b (diff) | |
When printing the type in About, use the renamed arguments.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/prettyp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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) (********************************) |