diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 89808ef4d..e885f5978 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -66,7 +66,7 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref = - let typ = Global.type_of_global ref in + let typ = Global.type_of_global_unsafe ref in let typ = if reduce then let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ @@ -122,7 +122,7 @@ let print_renames_list prefix l = hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))] let need_expansion impl ref = - let typ = Global.type_of_global ref in + let typ = Global.type_of_global_unsafe ref in let ctx = prod_assum typ in let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in not (List.is_empty impl) && List.length impl >= nprods && @@ -371,25 +371,23 @@ let print_body = function let print_typed_body (val_0,typ) = (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ) -let ungeneralized_type_of_constant_type = function - | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level) - | NonPolymorphicType t -> t +let ungeneralized_type_of_constant_type t = t let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Declareops.body_of_constant cb in let typ = ungeneralized_type_of_constant_type cb.const_type in - hov 0 ( + hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> str"*** [ " ++ print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_univ_cstr (Declareops.constraints_of_constant cb) + Printer.pr_universe_ctx (Future.force cb.const_universes) | _ -> print_basename sp ++ str sep ++ cut () ++ (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ - Printer.pr_univ_cstr (Declareops.constraints_of_constant cb)) + Printer.pr_universe_ctx (Future.force cb.const_universes)) let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ @@ -626,7 +624,7 @@ let print_opaque_name qid = | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr -> - let ty = Inductiveops.type_of_constructor env cstr in + let ty = Inductiveops.type_of_constructor env (cstr,Univ.Instance.empty) in print_typed_value (mkConstruct cstr, ty) | VarRef id -> let (_,c,ty) = lookup_named id env in |