[prettyp] remove `mod_ops` and `indirect_accessor` parameters

`Prettyp` is now late enough in linking to refer to them.

1 files changed, 21 insertions, 41 deletions

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;
 }