Merge PR #10727: [library] Move `Declaremods` to `vernac/`

Ack-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: ppedrot

4 files changed, 105 insertions, 80 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fb0b1eca8d..c995887f31 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -38,11 +38,11 @@ type object_pr = {
   print_constant_with_infos : Opaqueproof.indirect_accessor -> 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              : bool -> ModPath.t -> Pp.t;
-  print_modtype             : ModPath.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_named_decl          : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
-  print_library_entry       : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
-  print_context             : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> 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_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;
 }
@@ -618,7 +618,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 indirect_accessor env sigma with_values ((sp,kn as oname),lobj) =
+let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : " in
   match lobj with
   | AtomicObject o ->
@@ -639,17 +639,17 @@ let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as
     end
   | ModuleObject _ ->
     let (mp,l) = KerName.repr kn in
-    Some (print_module with_values (MPdot (mp,l)))
+    Some (print_module ~mod_ops with_values (MPdot (mp,l)))
   | ModuleTypeObject _ ->
     let (mp,l) = KerName.repr kn in
-          Some (print_modtype (MPdot (mp,l)))
+          Some (print_modtype ~mod_ops (MPdot (mp,l)))
   | _ -> None
 
-let gallina_print_library_entry indirect_accessor env sigma with_values ent =
+let gallina_print_library_entry ~mod_ops indirect_accessor 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 indirect_accessor env sigma with_values (oname,lobj)
+      gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj)
     | (oname,Lib.OpenedSection (dir,_)) ->
       Some (str " >>>>>>> Section " ++ pr_name oname)
     | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) ->
@@ -657,10 +657,10 @@ let gallina_print_library_entry indirect_accessor env sigma with_values ent =
     | (oname,Lib.OpenedModule _) ->
       Some (str " >>>>>>> Module " ++ pr_name oname)
 
-let gallina_print_context indirect_accessor env sigma with_values =
+let gallina_print_context ~mod_ops indirect_accessor 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 indirect_accessor env sigma with_values h with
+      (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with
        | None -> prec n rest
        | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ())
     | _ -> mt ()
@@ -698,8 +698,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 x = !object_pr.print_library_entry x
-let print_context x = !object_pr.print_context 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_typed_value_in_env x = !object_pr.print_typed_value_in_env x
 let print_eval x = !object_pr.print_eval x
 
@@ -720,10 +720,12 @@ let print_safe_judgment env sigma j =
 (*********************)
 (* *)
 
-let print_full_context indirect_accessor env sigma = print_context indirect_accessor env sigma true None (Lib.contents ())
-let print_full_context_typ indirect_accessor env sigma = print_context indirect_accessor env sigma false None (Lib.contents ())
+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_pure_context ~library_accessor env sigma =
+let print_full_pure_context ~mod_ops ~library_accessor env sigma =
   let rec prec = function
   | ((_,kn),Lib.Leaf AtomicObject lobj)::rest ->
       let pp = match object_tag lobj with
@@ -758,11 +760,11 @@ let print_full_pure_context ~library_accessor env sigma =
   | ((_,kn),Lib.Leaf ModuleObject _)::rest ->
           (* TODO: make it reparsable *)
     let (mp,l) = KerName.repr kn in
-          prec rest ++ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
+          prec rest ++ print_module ~mod_ops 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 (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
+          prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
   | _::rest -> prec rest
   | _ -> mt () in
   prec (Lib.contents ())
@@ -787,11 +789,11 @@ let read_sec_context qid =
   let cxt = Lib.contents () in
   List.rev (get_cxt [] cxt)
 
-let print_sec_context indirect_accessor env sigma sec =
-  print_context indirect_accessor env sigma true None (read_sec_context sec)
+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_typ indirect_accessor env sigma sec =
-  print_context indirect_accessor env sigma false 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 maybe_error_reject_univ_decl na udecl =
   let open GlobRef in
@@ -801,7 +803,7 @@ 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 indirect_accessor env sigma na udecl =
+let print_any_name ~mod_ops indirect_accessor env sigma na udecl =
   maybe_error_reject_univ_decl na udecl;
   let open GlobRef in
   match na with
@@ -810,9 +812,10 @@ let print_any_name indirect_accessor env sigma na 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 (printable_body obj_dir) obj_mp
+  | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) ->
+    print_module ~mod_ops (printable_body obj_dir) obj_mp
   | Dir _ -> mt ()
-  | ModuleType mp -> print_modtype mp
+  | ModuleType mp -> print_modtype ~mod_ops mp
   | Other (obj, info) -> info.print obj
   | Undefined qid ->
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
@@ -824,15 +827,15 @@ let print_any_name indirect_accessor env sigma na udecl =
     user_err
       ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
-let print_name indirect_accessor env sigma na udecl =
+let print_name ~mod_ops indirect_accessor env sigma na udecl =
   match na with
   | {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
-    print_any_name indirect_accessor env sigma
+    print_any_name ~mod_ops indirect_accessor env sigma
       (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
       udecl
   | {loc; v=Constrexpr.AN ref} ->
-    print_any_name indirect_accessor env sigma (locate_any_name ref) udecl
+    print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl
 
 let print_opaque_name indirect_accessor env sigma qid =
   let open GlobRef in
@@ -888,8 +891,8 @@ let print_about env sigma na udecl =
       print_about_any ?loc env sigma (locate_any_name ref) udecl
 
 (* for debug *)
-let inspect indirect_accessor env sigma depth =
-  print_context indirect_accessor env sigma false (Some depth) (Lib.contents ())
+let inspect ~mod_ops indirect_accessor env sigma depth =
+  print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ())
 
 (*************************************************************************)
 (* Pretty-printing functions coming from classops.ml                     *)
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 4299bcc880..c8b361d95b 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -19,28 +19,35 @@ val assumptions_for_print : Name.t list -> Termops.names_context
 
 val print_closed_sections : bool ref
 val print_context
-  : Opaqueproof.indirect_accessor
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor
   -> env -> Evd.evar_map
   -> bool -> int option -> Lib.library_segment -> Pp.t
 val print_library_entry
-  : Opaqueproof.indirect_accessor
+  : 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
- : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t
 val print_full_context_typ
-  : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t
 
 val print_full_pure_context
-  : library_accessor:Opaqueproof.indirect_accessor
+  : mod_ops:Printmod.mod_ops
+  -> library_accessor:Opaqueproof.indirect_accessor
   -> env
   -> Evd.evar_map
   -> Pp.t
 
 val print_sec_context
-  : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t
 val print_sec_context_typ
-  : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor -> 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 :
@@ -48,7 +55,8 @@ val print_eval :
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
 val print_name
-  : Opaqueproof.indirect_accessor
+  : 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
@@ -69,7 +77,10 @@ val print_typeclasses : unit -> Pp.t
 val print_instances : GlobRef.t -> Pp.t
 val print_all_instances : unit -> Pp.t
 
-val inspect : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> int -> Pp.t
+val inspect
+  : mod_ops:Printmod.mod_ops
+  -> Opaqueproof.indirect_accessor
+  -> env -> Evd.evar_map -> int -> Pp.t
 
 (** {5 Locate} *)
 
@@ -105,11 +116,11 @@ type object_pr = {
   print_constant_with_infos : Opaqueproof.indirect_accessor -> 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              : bool -> ModPath.t -> Pp.t;
-  print_modtype             : ModPath.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_named_decl          : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
-  print_library_entry       : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option;
-  print_context             : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> 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_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/printing/printmod.ml b/printing/printmod.ml
index 141469ff9c..03921bca30 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -240,9 +240,14 @@ let nametab_register_body mp dir (l,body) =
 	    mip.mind_consnames)
 	mib.mind_packets
 
-let nametab_register_module_body mp struc =
+type mod_ops =
+  { import_module : export:bool -> ModPath.t -> unit
+  ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit
+  }
+
+let nametab_register_module_body ~mod_ops mp struc =
   (* If [mp] is a globally visible module, we simply import it *)
-  try Declaremods.import_module ~export:false mp
+  try mod_ops.import_module ~export:false mp
   with Not_found ->
     (* Otherwise we try to emulate an import by playing with nametab *)
     nametab_register_dir mp;
@@ -252,7 +257,7 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with
   | Some (NoFunctor me) -> me
   | _ -> raise Not_found
 
-let nametab_register_modparam mbid mtb =
+let nametab_register_modparam ~mod_ops mbid mtb =
   let id = MBId.to_id mbid in
   match mtb.mod_type with
   | MoreFunctor _ -> id (* functorial param : nothing to register *)
@@ -260,7 +265,7 @@ let nametab_register_modparam mbid mtb =
     (* We first try to use the algebraic type expression if any,
        via a Declaremods function that converts back to module entries *)
     try
-      let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in
+      let () = mod_ops.process_module_binding mbid (get_typ_expr_alg mtb) in
       id
     with e when CErrors.noncritical e ->
       (* Otherwise, we try to play with the nametab ourselves *)
@@ -314,9 +319,9 @@ let print_body is_impl extent env mp (l,body) =
 let print_struct is_impl extent env mp struc =
   prlist_with_sep spc (print_body is_impl extent env mp) struc
 
-let print_structure is_type extent env mp locals struc =
+let print_structure ~mod_ops is_type extent env mp locals struc =
   let env' = Modops.add_structure mp struc Mod_subst.empty_delta_resolver env in
-  nametab_register_module_body mp struc;
+  nametab_register_module_body ~mod_ops mp struc;
   let kwd = if is_type then "Sig" else "Struct" in
   hv 2 (keyword kwd ++ spc () ++ print_struct false extent env' mp struc ++
 	brk (1,-2) ++ keyword "End")
@@ -362,31 +367,31 @@ let print_mod_expr env mp locals = function
         (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
   | MEwith _ -> assert false (* No 'with' syntax for modules *)
 
-let rec print_functor fty fatom is_type extent env mp locals = function
-  | NoFunctor me -> fatom is_type extent env mp locals me
+let rec print_functor ~mod_ops fty fatom is_type extent env mp locals = function
+  | NoFunctor me -> fatom ~mod_ops is_type extent env mp locals me
   | MoreFunctor (mbid,mtb1,me2) ->
-      let id = nametab_register_modparam mbid mtb1 in
+      let id = nametab_register_modparam ~mod_ops mbid mtb1 in
       let mp1 = MPbound mbid in
-      let pr_mtb1 = fty extent env mp1 locals mtb1 in
+      let pr_mtb1 = fty ~mod_ops extent env mp1 locals mtb1 in
       let env' = Modops.add_module_type mp1 mtb1 env in
       let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in
       let kwd = if is_type then "Funsig" else "Functor" in
       hov 2
         (keyword kwd ++ spc () ++
 	 str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++
-         spc() ++ print_functor fty fatom is_type extent env' mp locals' me2)
+         spc() ++ print_functor ~mod_ops fty fatom is_type extent env' mp locals' me2)
 
-let rec print_expression x =
-  print_functor
+let rec print_expression ~mod_ops x =
+  print_functor ~mod_ops
     print_modtype
-    (function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x
+    (fun ~mod_ops -> function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x
 
-and print_signature x =
-  print_functor print_modtype print_structure x
+and print_signature ~mod_ops x =
+  print_functor ~mod_ops print_modtype print_structure x
 
-and print_modtype extent env mp locals mtb = match mtb.mod_type_alg with
-  | Some me -> print_expression true extent env mp locals me
-  | None -> print_signature true extent env mp locals mtb.mod_type
+and print_modtype ~mod_ops extent env mp locals mtb = match mtb.mod_type_alg with
+  | Some me -> print_expression ~mod_ops true extent env mp locals me
+  | None -> print_signature ~mod_ops true extent env mp locals mtb.mod_type
 
 let rec printable_body dir =
   let dir = pop_dirpath dir in
@@ -403,52 +408,52 @@ let rec printable_body dir =
 (** Since we might play with nametab above, we should reset to prior
     state after the printing *)
 
-let print_expression' is_type extent env mp me =
+let print_expression' ~mod_ops is_type extent env mp me =
   States.with_state_protection
-    (fun e -> print_expression is_type extent env mp [] e) me
+    (fun e -> print_expression ~mod_ops is_type extent env mp [] e) me
 
-let print_signature' is_type extent env mp me =
+let print_signature' ~mod_ops is_type extent env mp me =
   States.with_state_protection
-    (fun e -> print_signature is_type extent env mp [] e) me
+    (fun e -> print_signature ~mod_ops is_type extent env mp [] e) me
 
-let unsafe_print_module extent env mp with_body mb =
+let unsafe_print_module ~mod_ops extent env mp with_body mb =
   let name = print_modpath [] mp in
   let pr_equals = spc () ++ str ":= " in
   let body = match with_body, mb.mod_expr with
     | false, _
     | true, Abstract -> mt()
-    | _, Algebraic me -> pr_equals ++ print_expression' false extent env mp me
-    | _, Struct sign -> pr_equals ++ print_signature' false extent env mp sign
-    | _, FullStruct -> pr_equals ++ print_signature' false extent env mp mb.mod_type
+    | _, Algebraic me -> pr_equals ++ print_expression' ~mod_ops false extent env mp me
+    | _, Struct sign -> pr_equals ++ print_signature' ~mod_ops false extent env mp sign
+    | _, FullStruct -> pr_equals ++ print_signature' ~mod_ops false extent env mp mb.mod_type
   in
   let modtype = match mb.mod_expr, mb.mod_type_alg with
     | FullStruct, _ -> mt ()
-    | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' true extent env mp ty
-    | _, _ -> brk (1,1) ++ str": " ++ print_signature' true extent env mp mb.mod_type
+    | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' ~mod_ops true extent env mp ty
+    | _, _ -> brk (1,1) ++ str": " ++ print_signature' ~mod_ops true extent env mp mb.mod_type
   in
   hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body)
 
 exception ShortPrinting
 
-let print_module with_body mp =
+let print_module ~mod_ops with_body mp =
   let me = Global.lookup_module mp in
   try
     if !short then raise ShortPrinting;
-    unsafe_print_module WithContents
+    unsafe_print_module ~mod_ops WithContents
       (Global.env ()) mp with_body me ++ fnl ()
   with e when CErrors.noncritical e ->
-    unsafe_print_module OnlyNames
+    unsafe_print_module ~mod_ops OnlyNames
       (Global.env ()) mp with_body me ++ fnl ()
 
-let print_modtype kn =
+let print_modtype ~mod_ops kn =
   let mtb = Global.lookup_modtype kn in
   let name = print_kn [] kn in
   hv 1
     (keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++
      try
       if !short then raise ShortPrinting;
-      print_signature' true WithContents
+      print_signature' ~mod_ops true WithContents
         (Global.env ()) kn mtb.mod_type
      with e when CErrors.noncritical e ->
-      print_signature' true OnlyNames
+      print_signature' ~mod_ops true OnlyNames
         (Global.env ()) kn mtb.mod_type)
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 8fd1cb4183..4c9245ee27 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -16,5 +16,11 @@ val printable_body : DirPath.t -> bool
 val pr_mutual_inductive_body : Environ.env ->
   MutInd.t -> Declarations.mutual_inductive_body ->
   UnivNames.univ_name_list option -> Pp.t
-val print_module : bool -> ModPath.t -> Pp.t
-val print_modtype : ModPath.t -> Pp.t
+
+type mod_ops =
+  { import_module : export:bool -> ModPath.t -> unit
+  ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit
+  }
+
+val print_module : mod_ops:mod_ops -> bool -> ModPath.t -> Pp.t
+val print_modtype : mod_ops:mod_ops -> ModPath.t -> Pp.t