diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 23 | ||||
| -rw-r--r-- | printing/printmod.ml | 15 |
2 files changed, 9 insertions, 29 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 605c1ae957..66f748454d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,8 +73,7 @@ let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref udecl = let typ, univs = Global.type_of_global_in_context (Global.env ()) ref in let inst = Univ.make_abstract_instance univs in - let bl = UnivNames.universe_binders_with_opt_names ref - (Array.to_list (Univ.Instance.to_array inst)) udecl in + let bl = UnivNames.universe_binders_with_opt_names ref udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let typ = EConstr.of_constr typ in let typ = @@ -556,33 +555,23 @@ let print_constant with_values sep sp udecl = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in let typ = cb.const_type in - let univs, ulist = + let univs = let open Univ in let otab = Global.opaque_tables () in match cb.const_body with - | Undef _ | Def _ -> - begin - match cb.const_universes with - | Monomorphic_const ctx -> Monomorphic_const ctx, [] - | Polymorphic_const ctx -> - let inst = make_abstract_instance ctx in - Polymorphic_const ctx, - Array.to_list (Instance.to_array inst) - end + | Undef _ | Def _ -> cb.const_universes | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with | Monomorphic_const ctx -> - Monomorphic_const (ContextSet.union body_uctxs ctx), [] + Monomorphic_const (ContextSet.union body_uctxs ctx) | Polymorphic_const ctx -> assert(ContextSet.is_empty body_uctxs); - let inst = make_abstract_instance ctx in - Polymorphic_const ctx, - Array.to_list (Instance.to_array inst) + Polymorphic_const ctx in let ctx = UState.of_binders - (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl) + (UnivNames.universe_binders_with_opt_names (ConstRef sp) udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in diff --git a/printing/printmod.ml b/printing/printmod.ml index f8d88aea07..1fc308ac99 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -119,14 +119,7 @@ let print_mutual_inductive env mind mib udecl = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in - let univs = - let open Univ in - if Declareops.inductive_is_polymorphic mib then - Array.to_list (Instance.to_array - (make_abstract_instance (Declareops.inductive_polymorphic_context mib))) - else [] - in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in + let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative @@ -164,8 +157,7 @@ let print_record env mind mib udecl = let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) - (Array.to_list (Univ.Instance.to_array u)) udecl in + let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = let open Declarations in @@ -304,8 +296,7 @@ let print_body is_impl env mp (l,body) = (match env with | None -> mt () | Some env -> - let univs = Array.to_list (Univ.Instance.to_array (Univ.make_abstract_instance ctx)) in - let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) univs None in + let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) None in let sigma = Evd.from_ctx (UState.of_binders bl) in str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ |