[declaremods] Remove abstraction of imperative module operations

Now that `Printmods` is above `Declaremods`, we don't need to pass the
extra `mod_ops` argument.

7 files changed, 47 insertions, 64 deletions

diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 50fa6052f6..d2eeebc246 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -1103,9 +1103,3 @@ 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 Unfiltered;
-  process_module_binding = process_module_binding;
-}
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli
index 5e45957e83..9ca2ca5593 100644
--- a/vernac/declaremods.mli
+++ b/vernac/declaremods.mli
@@ -126,5 +126,3 @@ 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 80e0b9987f..176ddd6c5b 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -46,10 +46,8 @@ type object_pr = {
   print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
 }
 
-let gallina_print_module  = print_module ~mod_ops:Declaremods.mod_ops
-let gallina_print_modtype = print_modtype ~mod_ops:Declaremods.mod_ops
-
-
+let gallina_print_module  = print_module
+let gallina_print_modtype = print_modtype
 
 (**************)
 (** Utilities *)
@@ -701,10 +699,10 @@ let gallina_print_leaf_entry env sigma with_values ((sp, kn),lobj) =
     handle handler o
   | ModuleObject _ ->
     let (mp,l) = KerName.repr kn in
-    Some (print_module with_values ~mod_ops:Declaremods.mod_ops (MPdot (mp,l)))
+    Some (print_module with_values (MPdot (mp,l)))
   | ModuleTypeObject _ ->
     let (mp,l) = KerName.repr kn in
-          Some (print_modtype ~mod_ops:Declaremods.mod_ops (MPdot (mp,l)))
+          Some (print_modtype (MPdot (mp,l)))
   | _ -> None
 
 let gallina_print_library_entry env sigma with_values ent =
diff --git a/vernac/printmod.ml b/vernac/printmod.ml
index 9beac17546..219e445c56 100644
--- a/vernac/printmod.ml
+++ b/vernac/printmod.ml
@@ -239,14 +239,12 @@ let nametab_register_body mp dir (l,body) =
             mip.mind_consnames)
         mib.mind_packets
 
-type mod_ops =
-  { import_module : export:bool -> ModPath.t -> unit
-  ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit
-  }
+let import_module = Declaremods.import_module Libobject.Unfiltered
+let process_module_binding = Declaremods.process_module_binding
 
-let nametab_register_module_body ~mod_ops mp struc =
+let nametab_register_module_body mp struc =
   (* If [mp] is a globally visible module, we simply import it *)
-  try mod_ops.import_module ~export:false mp
+  try import_module ~export:false mp
   with Not_found ->
     (* Otherwise we try to emulate an import by playing with nametab *)
     nametab_register_dir mp;
@@ -256,7 +254,7 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with
   | Some (NoFunctor me) -> me
   | _ -> raise Not_found
 
-let nametab_register_modparam ~mod_ops mbid mtb =
+let nametab_register_modparam mbid mtb =
   let id = MBId.to_id mbid in
   match mtb.mod_type with
   | MoreFunctor _ -> id (* functorial param : nothing to register *)
@@ -264,7 +262,7 @@ let nametab_register_modparam ~mod_ops 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 () = mod_ops.process_module_binding mbid (get_typ_expr_alg mtb) in
+      let () = 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 *)
@@ -318,9 +316,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 ~mod_ops is_type extent env mp locals struc =
+let print_structure 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 ~mod_ops mp struc;
+  nametab_register_module_body 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")
@@ -366,31 +364,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 ~mod_ops fty fatom is_type extent env mp locals = function
-  | NoFunctor me -> fatom ~mod_ops is_type extent env mp locals me
+let rec print_functor fty fatom is_type extent env mp locals = function
+  | NoFunctor me -> fatom is_type extent env mp locals me
   | MoreFunctor (mbid,mtb1,me2) ->
-      let id = nametab_register_modparam ~mod_ops mbid mtb1 in
+      let id = nametab_register_modparam mbid mtb1 in
       let mp1 = MPbound mbid in
-      let pr_mtb1 = fty ~mod_ops extent env mp1 locals mtb1 in
+      let pr_mtb1 = fty 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 ~mod_ops fty fatom is_type extent env' mp locals' me2)
+         spc() ++ print_functor fty fatom is_type extent env' mp locals' me2)
 
-let rec print_expression ~mod_ops x =
-  print_functor ~mod_ops
+let rec print_expression x =
+  print_functor
     print_modtype
-    (fun ~mod_ops -> function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x
+    (function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x
 
-and print_signature ~mod_ops x =
-  print_functor ~mod_ops print_modtype print_structure x
+and print_signature x =
+  print_functor print_modtype print_structure x
 
-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
+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
 
 let rec printable_body dir =
   let dir = pop_dirpath dir in
@@ -407,52 +405,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' ~mod_ops is_type extent env mp me =
+let print_expression' is_type extent env mp me =
   States.with_state_protection
-    (fun e -> print_expression ~mod_ops is_type extent env mp [] e) me
+    (fun e -> print_expression is_type extent env mp [] e) me
 
-let print_signature' ~mod_ops is_type extent env mp me =
+let print_signature' is_type extent env mp me =
   States.with_state_protection
-    (fun e -> print_signature ~mod_ops is_type extent env mp [] e) me
+    (fun e -> print_signature is_type extent env mp [] e) me
 
-let unsafe_print_module ~mod_ops extent env mp with_body mb =
+let unsafe_print_module 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' ~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
+    | _, 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
   in
   let modtype = match mb.mod_expr, mb.mod_type_alg with
     | FullStruct, _ -> mt ()
-    | _, 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
+    | _, 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
   in
   hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body)
 
 exception ShortPrinting
 
-let print_module ~mod_ops with_body mp =
+let print_module with_body mp =
   let me = Global.lookup_module mp in
   try
     if !short then raise ShortPrinting;
-    unsafe_print_module ~mod_ops WithContents
+    unsafe_print_module WithContents
       (Global.env ()) mp with_body me ++ fnl ()
   with e when CErrors.noncritical e ->
-    unsafe_print_module ~mod_ops OnlyNames
+    unsafe_print_module OnlyNames
       (Global.env ()) mp with_body me ++ fnl ()
 
-let print_modtype ~mod_ops kn =
+let print_modtype 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' ~mod_ops true WithContents
+      print_signature' true WithContents
         (Global.env ()) kn mtb.mod_type
      with e when CErrors.noncritical e ->
-      print_signature' ~mod_ops true OnlyNames
+      print_signature' true OnlyNames
         (Global.env ()) kn mtb.mod_type)
diff --git a/vernac/printmod.mli b/vernac/printmod.mli
index c7f056063b..694821a2d6 100644
--- a/vernac/printmod.mli
+++ b/vernac/printmod.mli
@@ -17,10 +17,5 @@ val pr_mutual_inductive_body : Environ.env ->
   MutInd.t -> Declarations.mutual_inductive_body ->
   UnivNames.univ_name_list option -> 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
+val print_module : bool -> ModPath.t -> Pp.t
+val print_modtype : ModPath.t -> Pp.t
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 085e2e35bc..f357a04668 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -2,8 +2,8 @@ Vernacexpr
 Attributes
 Pvernac
 States
-Printmod
 Declaremods
+Printmod
 G_vernac
 G_proofs
 Vernacprop
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d44e4babf4..f5ef5ee86f 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 ~mod_ops:Declaremods.mod_ops (Printmod.printable_body obj_dir) obj_mp
+          Printmod.print_module (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 ~mod_ops:Declaremods.mod_ops kn
+    Printmod.print_modtype 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 ~mod_ops:Declaremods.mod_ops false mp
+      Printmod.print_module false mp
     with Not_found ->
       user_err (str"Unknown Module Type or Module " ++ pr_qualid qid)