diff options
| -rw-r--r-- | toplevel/coqc.ml | 6 | ||||
| -rw-r--r-- | vernac/declaremods.ml | 6 | ||||
| -rw-r--r-- | vernac/declaremods.mli | 2 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 94 | ||||
| -rw-r--r-- | vernac/prettyp.mli | 62 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 21 |
7 files changed, 89 insertions, 104 deletions
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 642dc94ab2..98206fb341 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -53,11 +53,7 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in - let library_accessor = Library.indirect_accessor in - let mod_ops = { Printmod.import_module = Declaremods.import_module - ; process_module_binding = Declaremods.process_module_binding - } in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~mod_ops ~library_accessor env) sigma) ++ fnl ()) + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; CProfile.print_profile () diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index c7b68d18c2..65cd4cd6a4 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -1068,3 +1068,9 @@ let debug_print_modtab _ = in let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in hov 0 modules + + +let mod_ops = { + Printmod.import_module = import_module; + process_module_binding = process_module_binding; +} diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index ae84704656..23f25bc597 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -126,3 +126,5 @@ val debug_print_modtab : unit -> Pp.t val process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + +val mod_ops : Printmod.mod_ops diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index b03ff7b2ae..5ebc89892c 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -34,20 +34,22 @@ module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> 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; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } -let gallina_print_module = print_module -let gallina_print_modtype = print_modtype +let gallina_print_module = print_module ~mod_ops:Declaremods.mod_ops +let gallina_print_modtype = print_modtype ~mod_ops:Declaremods.mod_ops + + (**************) (** Utilities *) @@ -585,9 +587,9 @@ let print_instance sigma cb = pr_universe_instance sigma inst else mt() -let print_constant indirect_accessor with_values sep sp udecl = +let print_constant with_values sep sp udecl = let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body indirect_accessor cb in + let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in let typ = cb.const_type in let univs = let open Univ in @@ -595,7 +597,7 @@ let print_constant indirect_accessor with_values sep sp udecl = match cb.const_body with | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in + let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in match cb.const_universes with | Monomorphic ctx -> Monomorphic (ContextSet.union body_uctxs ctx) @@ -625,8 +627,8 @@ let print_constant indirect_accessor with_values sep sp udecl = (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_universes sigma univs ?priv) -let gallina_print_constant_with_infos indirect_accessor sp udecl = - print_constant indirect_accessor true " = " sp udecl ++ +let gallina_print_constant_with_infos sp udecl = + print_constant true " = " sp udecl ++ with_line_skip (print_name_infos (GlobRef.ConstRef sp)) let gallina_print_syntactic_def env kn = @@ -642,7 +644,7 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> @@ -653,7 +655,7 @@ let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (( constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> - Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) + Some (print_constant with_values sep (Constant.make1 kn) None) | (_,"INDUCTIVE") -> Some (gallina_print_inductive (MutInd.make1 kn) None) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| @@ -663,17 +665,17 @@ let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (( end | ModuleObject _ -> let (mp,l) = KerName.repr kn in - Some (print_module ~mod_ops with_values (MPdot (mp,l))) + Some (print_module with_values ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) | ModuleTypeObject _ -> let (mp,l) = KerName.repr kn in - Some (print_modtype ~mod_ops (MPdot (mp,l))) + Some (print_modtype ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values ent = +let gallina_print_library_entry env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj) + gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> @@ -681,10 +683,10 @@ let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context ~mod_ops indirect_accessor env sigma with_values = +let gallina_print_context env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with + (match gallina_print_library_entry env sigma with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () @@ -722,8 +724,8 @@ let print_syntactic_def x = !object_pr.print_syntactic_def x let print_module x = !object_pr.print_module x let print_modtype x = !object_pr.print_modtype x let print_named_decl x = !object_pr.print_named_decl x -let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x -let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x +let print_library_entry x = !object_pr.print_library_entry x +let print_context x = !object_pr.print_context x let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x let print_eval x = !object_pr.print_eval x @@ -744,12 +746,12 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) -let print_full_context_typ ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) +let print_full_context env sigma = + print_context env sigma true None (Lib.contents ()) +let print_full_context_typ env sigma = + print_context env sigma false None (Lib.contents ()) -let print_full_pure_context ~mod_ops ~library_accessor env sigma = +let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let pp = match object_tag lobj with @@ -765,7 +767,9 @@ let print_full_pure_context ~mod_ops ~library_accessor env sigma = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) + str "Proof " ++ pr_lconstr_env env sigma + (fst (Opaqueproof.force_proof Library.indirect_accessor + (Global.opaque_tables ()) lc)) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ @@ -784,11 +788,11 @@ let print_full_pure_context ~mod_ops ~library_accessor env sigma = | ((_,kn),Lib.Leaf ModuleObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _::rest -> prec rest | _ -> mt () in prec (Lib.contents ()) @@ -813,11 +817,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) +let print_sec_context env sigma sec = + print_context env sigma true None (read_sec_context sec) -let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) +let print_sec_context_typ env sigma sec = + print_context env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = let open GlobRef in @@ -827,19 +831,19 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name ~mod_ops indirect_accessor env sigma na udecl = +let print_any_name env sigma na udecl = maybe_error_reject_univ_decl na udecl; let open GlobRef in match na with - | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl + | Term (ConstRef sp) -> print_constant_with_infos sp udecl | Term (IndRef (sp,_)) -> print_inductive sp udecl | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp | Syntactic kn -> print_syntactic_def env kn | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> - print_module ~mod_ops (printable_body obj_dir) obj_mp + print_module (printable_body obj_dir) obj_mp | Dir _ -> mt () - | ModuleType mp -> print_modtype ~mod_ops mp + | ModuleType mp -> print_modtype mp | Other (obj, info) -> info.print obj | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) @@ -851,23 +855,23 @@ let print_any_name ~mod_ops indirect_accessor env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name ~mod_ops indirect_accessor env sigma na udecl = +let print_name env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name ~mod_ops indirect_accessor env sigma + print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl | {loc; v=Constrexpr.AN ref} -> - print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl + print_any_name env sigma (locate_any_name ref) udecl -let print_opaque_name indirect_accessor env sigma qid = +let print_opaque_name env sigma qid = let open GlobRef in match Nametab.global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in if Declareops.constant_has_body cb then - print_constant_with_infos indirect_accessor cst None + print_constant_with_infos cst None else user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> @@ -915,8 +919,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect ~mod_ops indirect_accessor env sigma depth = - print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) +let inspect env sigma depth = + print_context env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli index c8b361d95b..dc4280f286 100644 --- a/vernac/prettyp.mli +++ b/vernac/prettyp.mli @@ -19,48 +19,31 @@ val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref val print_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map + : env + -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t val print_library_entry - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map - -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option -val print_full_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t -val print_full_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t - -val print_full_pure_context - : mod_ops:Printmod.mod_ops - -> library_accessor:Opaqueproof.indirect_accessor - -> env + : env -> Evd.evar_map - -> Pp.t + -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option +val print_full_context : env -> Evd.evar_map -> Pp.t +val print_full_context_typ : env -> Evd.evar_map -> Pp.t + +val print_full_pure_context : env -> Evd.evar_map -> Pp.t -val print_sec_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t -val print_sec_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation - -> UnivNames.univ_name_list option -> Pp.t -val print_opaque_name - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_name : env -> Evd.evar_map + -> qualid Constrexpr.or_by_notation + -> UnivNames.univ_name_list option + -> Pp.t +val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t @@ -77,10 +60,7 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> int -> Pp.t +val inspect : env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -113,14 +93,14 @@ val print_located_other : string -> qualid -> Pp.t type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.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; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 7563b4a5d5..5226c2ba65 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -10,7 +10,6 @@ Locality Egramml Vernacextend Ppvernac -Prettyp Proof_using Egramcoq Metasyntax @@ -20,6 +19,7 @@ DeclareObl Canonical RecLemmas Library +Prettyp Lemmas Class Auto_ind_decl diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4c7332f011..edff80af00 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -175,7 +175,7 @@ let print_module qid = let globdir = Nametab.locate_dir qid in match globdir with DirModule Nametab.{ obj_dir; obj_mp; _ } -> - Printmod.print_module (Printmod.printable_body obj_dir) obj_mp + Printmod.print_module ~mod_ops:Declaremods.mod_ops (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) @@ -183,12 +183,12 @@ let print_module qid = let print_modtype qid = try let kn = Nametab.locate_modtype qid in - Printmod.print_modtype kn + Printmod.print_modtype ~mod_ops:Declaremods.mod_ops kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try let mp = Nametab.locate_module qid in - Printmod.print_module false mp + Printmod.print_module ~mod_ops:Declaremods.mod_ops false mp with Not_found -> user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) @@ -1672,29 +1672,26 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~pstate ~atts = - let mod_ops = { Printmod.import_module = Declaremods.import_module - ; process_module_binding = Declaremods.process_module_binding - } in let sigma, env = get_current_or_global_context ~pstate in function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ ~mod_ops Library.indirect_accessor env sigma - | PrintSectionContext qid -> print_sec_context_typ ~mod_ops Library.indirect_accessor env sigma qid - | PrintInspect n -> inspect ~mod_ops Library.indirect_accessor env sigma n + | PrintFullContext-> print_full_context_typ env sigma + | PrintSectionContext qid -> print_sec_context_typ env sigma qid + | PrintInspect n -> inspect env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () - | PrintModule qid -> print_module ~mod_ops qid - | PrintModuleType qid -> print_modtype ~mod_ops qid + | PrintModule qid -> print_module qid + | PrintModuleType qid -> print_modtype qid | PrintNamespace ns -> print_namespace ~pstate ns | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name ~mod_ops Library.indirect_accessor env sigma qid udecl + print_name env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() |