[library] Move `Declaremods` to `vernac/`

We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.

This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.

The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.

This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.

12 files changed, 144 insertions, 114 deletions

diff --git a/interp/modintern.ml b/interp/modintern.ml
index 955288244e..ddf5b2d7b1 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -12,7 +12,6 @@ open Declarations
 open Libnames
 open Constrexpr
 open Constrintern
-open Declaremods
 
 type module_internalization_error =
   | NotAModuleNorModtype of string
@@ -21,9 +20,11 @@ type module_internalization_error =
 
 exception ModuleInternalizationError of module_internalization_error
 
+type module_kind = Module | ModType | ModAny
+
 let error_not_a_module_loc kind loc qid =
   let s = string_of_qualid qid in
-  let e = let open Declaremods in match kind with
+  let e = match kind with
     | Module -> Modops.ModuleTypingError (Modops.NotAModule s)
     | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
     | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
@@ -46,7 +47,6 @@ let error_application_to_module_type loc =
     it is equal to the input kind when this one isn't ModAny. *)
 
 let lookup_module_or_modtype kind qid =
-  let open Declaremods in
   let loc = qid.CAst.loc in
   try
     if kind == ModType then raise Not_found;
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 75ab38c64a..72695a680e 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -28,5 +28,7 @@ exception ModuleInternalizationError of module_internalization_error
    kind is never ModAny, and it is equal to the input kind when this one
    isn't ModAny. *)
 
+type module_kind = Module | ModType | ModAny
+
 val interp_module_ast :
-  env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t
+  env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t
diff --git a/library/library.mllib b/library/library.mllib
index c34d8911e8..a6188f7661 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -5,7 +5,6 @@ Summary
 Nametab
 Global
 Lib
-Declaremods
 States
 Kindops
 Goptions
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
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 7658ad68a5..642dc94ab2 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -54,7 +54,10 @@ 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
-    Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~library_accessor env) sigma) ++ fnl ())
+    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 ())
   end;
   CProfile.print_profile ()
 
diff --git a/library/declaremods.ml b/vernac/declaremods.ml
index b4dc42bdfe..9f2e30b7a6 100644
--- a/library/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -17,6 +17,7 @@ open Entries
 open Libnames
 open Libobject
 open Mod_subst
+open Modintern
 
 (** {6 Inlining levels} *)
 
@@ -35,8 +36,6 @@ type inline =
   | DefaultInline
   | InlineAt of int
 
-type module_kind = Module | ModType | ModAny
-
 let default_inline () = Some (Flags.get_inline_level ())
 
 let inl2intopt = function
@@ -457,15 +456,15 @@ let rec compute_subst env mbids sign mp_l inl =
     | _,[] -> mbids,empty_subst
     | [],r -> user_err Pp.(str "Application of a functor with too few arguments.")
     | mbid::mbids,mp::mp_l ->
-	let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
-	let mb = Environ.lookup_module mp env in
-	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in
-	let resolver =
+        let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
+        let mb = Environ.lookup_module mp env in
+        let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in
+        let resolver =
           if Modops.is_functor mb.mod_type then empty_delta_resolver
           else
             Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta
-	in
-	mbid_left,join (map_mbid mbid mp resolver) subst
+        in
+        mbid_left,join (map_mbid mbid mp resolver) subst
 
 (** Create the objects of a "with Module" structure. *)
 
@@ -588,10 +587,10 @@ let intern_args interp_modast params =
 let check_sub mtb sub_mtb_l =
   (* The constraints are checked and forgot immediately : *)
   ignore (List.fold_right
-	    (fun sub_mtb env ->
-	       Environ.add_constraints
-		 (Subtyping.check_subtypes env mtb sub_mtb) env)
-	    sub_mtb_l (Global.env()))
+            (fun sub_mtb env ->
+               Environ.add_constraints
+                 (Subtyping.check_subtypes env mtb sub_mtb) env)
+            sub_mtb_l (Global.env()))
 
 (** This function checks if the type calculated for the module [mp] is
     a subtype of all signatures in [sub_mtb_l]. Uses only the global
@@ -952,9 +951,9 @@ let declare_module interp id args mtys me_l =
     | [] -> RawModOps.declare_module interp id args mtys None fs
     | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs
     | me_l ->
-	ignore (RawModOps.start_module interp None id args mtys fs);
-	RawIncludeOps.declare_include interp me_l;
-	RawModOps.end_module ()
+        ignore (RawModOps.start_module interp None id args mtys fs);
+        RawIncludeOps.declare_include interp me_l;
+        RawModOps.end_module ()
   in
   protect_summaries declare_me
 
@@ -968,9 +967,9 @@ let declare_modtype interp id args mtys mty_l =
     | [] -> assert false
     | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs
     | mty_l ->
-	ignore (RawModTypeOps.start_modtype interp id args mtys fs);
-	RawIncludeOps.declare_include interp mty_l;
-	RawModTypeOps.end_modtype ()
+        ignore (RawModTypeOps.start_modtype interp id args mtys fs);
+        RawIncludeOps.declare_include interp mty_l;
+        RawModTypeOps.end_modtype ()
   in
   protect_summaries declare_mt
 
diff --git a/library/declaremods.mli b/vernac/declaremods.mli
index b7c7cd1dba..5c2c992825 100644
--- a/library/declaremods.mli
+++ b/vernac/declaremods.mli
@@ -29,11 +29,9 @@ type inline =
 
 (** Kinds of modules *)
 
-type module_kind = Module | ModType | ModAny
-
 type 'modast module_interpretor =
-  Environ.env -> module_kind -> 'modast ->
-    Entries.module_struct_entry * module_kind * Univ.ContextSet.t
+  Environ.env -> Modintern.module_kind -> 'modast ->
+    Entries.module_struct_entry * Modintern.module_kind * Univ.ContextSet.t
 
 type 'modast module_params =
   (lident list * ('modast * inline)) list
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index cd13f83e96..4868182bb3 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,6 +1,7 @@
 Vernacexpr
 Attributes
 Pvernac
+Declaremods
 G_vernac
 G_proofs
 Vernacprop
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 43b58d6d4b..85ba464a2d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1966,26 +1966,29 @@ 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 Library.indirect_accessor env sigma
-  | PrintSectionContext qid -> print_sec_context_typ Library.indirect_accessor env sigma qid
-  | PrintInspect n -> inspect Library.indirect_accessor env sigma n
+  | 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
   | 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 qid
-  | PrintModuleType qid -> print_modtype qid
+  | PrintModule qid -> print_module ~mod_ops qid
+  | PrintModuleType qid -> print_modtype ~mod_ops 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 Library.indirect_accessor env sigma qid udecl
+    print_name ~mod_ops Library.indirect_accessor env sigma qid udecl
   | PrintGraph -> Prettyp.print_graph ()
   | PrintClasses -> Prettyp.print_classes()
   | PrintTypeClasses -> Prettyp.print_typeclasses()