diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 7 | ||||
| -rw-r--r-- | printing/printer.mli | 1 | ||||
| -rw-r--r-- | printing/printmod.ml | 10 |
3 files changed, 13 insertions, 5 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index d6f0778f75..c27a9b009d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -261,6 +261,13 @@ let pr_universe_ctx sigma c = else mt() +let pr_universe_info_ind sigma uii = + if !Detyping.print_universes && not (Univ.UInfoInd.is_empty uii) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_universe_info_ind (Termops.pr_evd_level sigma) uii)) uii + else + mt() + (**********************************************************************) (* Global references *) diff --git a/printing/printer.mli b/printing/printer.mli index 3fce065613..6531036a1f 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -97,6 +97,7 @@ val pr_sort : evar_map -> sorts -> std_ppcmds val pr_polymorphic : bool -> std_ppcmds val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds +val pr_universe_info_ind : evar_map -> Univ.universe_info_ind -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index c4affd4acd..7dc47a4a4c 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -89,7 +89,7 @@ let build_ind_type env mip = let print_one_inductive env sigma mib ((_,i) as ind) = let u = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in @@ -100,7 +100,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let envpar = push_rel_context params env in let inst = if mib.mind_polymorphic then - Printer.pr_universe_instance sigma mib.mind_universes + Printer.pr_universe_instance sigma (Univ.UInfoInd.univ_context mib.mind_universes) else mt () in hov 0 ( @@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib = def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env sigma mib) inds ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -142,7 +142,7 @@ let get_fields = let print_record env mind mib = let u = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty in let mip = mib.mind_packets.(0) in @@ -175,7 +175,7 @@ let print_record env mind mib = (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then |