diff options
| -rw-r--r-- | printing/prettyp.ml | 14 | ||||
| -rw-r--r-- | printing/printer.ml | 4 | ||||
| -rw-r--r-- | printing/printer.mli | 1 | ||||
| -rw-r--r-- | printing/printmod.ml | 6 |
4 files changed, 21 insertions, 4 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b8c5fd4cf..7e625af0d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,7 +73,11 @@ let print_ref reduce ref = in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in - hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++ + let inst = + if Global.is_polymorphic ref then Printer.pr_universe_instance univs + else mt () + in + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype typ ++ Printer.pr_universe_ctx univs) (********************************) @@ -473,6 +477,10 @@ let print_typed_body (val_0,typ) = let ungeneralized_type_of_constant_type t = Typeops.type_of_constant_type (Global.env ()) t +let print_instance cb = + if cb.const_polymorphic then pr_universe_instance cb.const_universes + else mt() + let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in @@ -485,11 +493,11 @@ let print_constant with_values sep sp = match val_0 with | None -> str"*** [ " ++ - print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ + print_basename sp ++ print_instance cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ Printer.pr_universe_ctx univs | _ -> - print_basename sp ++ str sep ++ cut () ++ + print_basename sp ++ print_instance cb ++ str sep ++ cut () ++ (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ Printer.pr_universe_ctx univs) diff --git a/printing/printer.ml b/printing/printer.ml index 18e490225..f4852b108 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -825,3 +825,7 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () +let pr_universe_instance ctx = + let inst = Univ.UContext.instance ctx in + str"@{" ++ Univ.Instance.pr Univ.Level.pr inst ++ str"}" + diff --git a/printing/printer.mli b/printing/printer.mli index 5f56adbe6..25a4aa166 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -84,6 +84,7 @@ val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds +val pr_universe_instance : Univ.universe_context -> std_ppcmds val pr_universe_ctx : Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 53d0508c7..8031de27d 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -94,8 +94,12 @@ let print_one_inductive env mib ((_,i) as ind) = let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in + let inst = + if mib.mind_polymorphic then Printer.pr_universe_instance mib.mind_universes + else mt () + in hov 0 ( - pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++ + pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env Evd.empty params ++ str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes |