diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 17 |
1 files changed, 5 insertions, 12 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f926e82751..1810cc6588 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -40,7 +40,7 @@ type object_pr = { print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; @@ -98,7 +98,8 @@ let print_ref reduce ref udecl = (Array.to_list (Univ.Instance.to_array inst)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = - if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs + if Global.is_polymorphic ref + then Printer.pr_universe_instance sigma (Univ.UContext.instance univs) else mt () in hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ @@ -552,8 +553,7 @@ let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then let univs = Declareops.constant_polymorphic_context cb in let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in - pr_universe_instance sigma univs + pr_universe_instance sigma inst else mt() let print_constant with_values sep sp udecl = @@ -657,14 +657,10 @@ let gallina_print_library_entry env sigma with_values ent = gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection _) -> - Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { obj_dir; _ }) -> Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) - | (oname,Lib.ClosedModule _) -> - Some (str " >>>>>>> Closed Module " ++ pr_name oname) let gallina_print_context env sigma with_values = let rec prec n = function @@ -793,9 +789,6 @@ let read_sec_context qid = let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest -> if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | (_,Lib.ClosedSection _)::rest -> - user_err Pp.(str "Cannot print the contents of a closed section.") - (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest in @@ -909,7 +902,7 @@ let inspect env sigma depth = open Classops -let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v) +let print_coercion_value env sigma v = Printer.pr_global v.coe_value let print_class i = let cl,_ = class_info_from_index i in |