Merge PR #16213: Cleanup open modules in library/

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

library/coqlib.ml

@@ -8,11 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
 open Util
-open Pp
 open Names
-open Libnames
 
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
@@ -52,7 +49,7 @@ let check_ind_ref s ind =
 let lib_ref s =
   try CString.Map.find s !table
   with Not_found ->
-    user_err Pp.(str "not found in table: " ++ str s)
+    CErrors.user_err Pp.(str "not found in table: " ++ str s)
 
 let add_ref s c =
   table := CString.Map.add s c !table
@@ -77,28 +74,28 @@ let register_ref s c =
 (* Generic functions to find Coq objects *)
 
 let has_suffix_in_dirs dirs ref =
-  let dir = dirpath (Nametab.path_of_global ref) in
-  List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
+  let dir = Libnames.dirpath (Nametab.path_of_global ref) in
+  List.exists (fun d -> Libnames.is_dirpath_prefix_of d dir) dirs
 
 let gen_reference_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
-  let qualid = qualid_of_string s in
+  let qualid = Libnames.qualid_of_string s in
   let all = Nametab.locate_all qualid in
   let all = List.sort_uniquize GlobRef.UserOrd.compare all in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
     | [x] -> x
     | [] ->
-        anomaly ~label:locstr (str "cannot find " ++ str s ++
-        str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
-        prlist_with_sep pr_comma DirPath.print dirs ++ str ".")
+      CErrors.anomaly ~label:locstr Pp.(str "cannot find " ++ str s
+        ++ str " in module" ++ str (if List.length dirs > 1 then "s " else " ")
+        ++ prlist_with_sep pr_comma DirPath.print dirs ++ str ".")
     | l ->
-      anomaly ~label:locstr
-        (str "ambiguous name " ++ str s ++ str " can represent " ++
-           prlist_with_sep pr_comma
-           (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
-           str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
-           prlist_with_sep pr_comma DirPath.print dirs ++ str ".")
+      CErrors.anomaly ~label:locstr
+        Pp.(str "ambiguous name " ++ str s ++ str " can represent "
+          ++ prlist_with_sep pr_comma (fun x ->
+            Libnames.pr_path (Nametab.path_of_global x)) l ++ str " in module"
+          ++ str (if List.length dirs > 1 then "s " else " ")
+          ++ prlist_with_sep pr_comma DirPath.print dirs ++ str ".")
 
 (* For tactics/commands requiring vernacular libraries *)
 
@@ -113,8 +110,8 @@ let check_required_library d =
       | _ -> false
     in
     if not in_current_dir then
-      user_err
-        (str "Library " ++ DirPath.print dir ++ str " has to be required first.")
+      CErrors.user_err Pp.(str "Library " ++ DirPath.print dir
+        ++ str " has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects                                                 *)
@@ -321,4 +318,4 @@ let coq_or_ref     = Lazy.from_fun build_coq_or
 let coq_iff_ref    = Lazy.from_fun build_coq_iff
 
 (** Deprecated functions that search by library name. *)
-let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type.")
+let build_sigma_set () = CErrors.anomaly (Pp.str "Use build_sigma_type.")

library/global.ml

@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Environ
 
 (** We introduce here the global environment of the system,
     and we declare it as a synchronized table. *)
@@ -118,19 +117,19 @@ let add_module_parameter mbid mte inl =
 
 (** Queries on the global environment *)
 
-let universes () = universes (env())
-let universes_lbound () = universes_lbound (env())
-let named_context () = named_context (env())
-let named_context_val () = named_context_val (env())
+let universes () = Environ.universes (env())
+let universes_lbound () = Environ.universes_lbound (env())
+let named_context () = Environ.named_context (env())
+let named_context_val () = Environ.named_context_val (env())
 
-let lookup_named id = lookup_named id (env())
-let lookup_constant kn = lookup_constant kn (env())
+let lookup_named id = Environ.lookup_named id (env())
+let lookup_constant kn = Environ.lookup_constant kn (env())
 let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind
 let lookup_pinductive (ind,_) = Inductive.lookup_mind_specif (env()) ind
-let lookup_mind kn = lookup_mind kn (env())
+let lookup_mind kn = Environ.lookup_mind kn (env())
 
-let lookup_module mp = lookup_module mp (env())
-let lookup_modtype kn = lookup_modtype kn (env())
+let lookup_module mp = Environ.lookup_module mp (env())
+let lookup_modtype kn = Environ.lookup_modtype kn (env())
 
 let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 
@@ -181,15 +180,19 @@ let import c u d = globalize (Safe_typing.import c u d)
     environment and a given context. *)
 
 let env_of_context hyps =
-  reset_with_named_context hyps (env())
+  Environ.reset_with_named_context hyps (env())
 
-let is_polymorphic r = Environ.is_polymorphic (env()) r
+let is_polymorphic r =
+  Environ.is_polymorphic (env()) r
 
-let is_template_polymorphic r = is_template_polymorphic (env ()) r
+let is_template_polymorphic r =
+  Environ.is_template_polymorphic (env ()) r
 
-let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r
+let get_template_polymorphic_variables r =
+  Environ.get_template_polymorphic_variables (env ()) r
 
-let is_type_in_type r = is_type_in_type (env ()) r
+let is_type_in_type r =
+  Environ.is_type_in_type (env ()) r
 
 let current_modpath () =
   Safe_typing.current_modpath (safe_env ())

library/globnames.ml

@@ -10,7 +10,6 @@
 
 open Names
 open Constr
-open Mod_subst
 
 type global_reference = GlobRef.t =
   | VarRef of variable     [@ocaml.deprecated "Use Names.GlobRef.VarRef"]
@@ -35,25 +34,25 @@ let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destCon
 let subst_global_reference subst ref = match ref with
   | VarRef var -> ref
   | ConstRef kn ->
-    let kn' = subst_constant subst kn in
+    let kn' = Mod_subst.subst_constant subst kn in
       if kn==kn' then ref else ConstRef kn'
   | IndRef ind ->
-    let ind' = subst_ind subst ind in
+    let ind' = Mod_subst.subst_ind subst ind in
       if ind==ind' then ref else IndRef ind'
   | ConstructRef ((kn,i),j as c) ->
-    let c' = subst_constructor subst c in
+    let c' = Mod_subst.subst_constructor subst c in
     if c'==c then ref else ConstructRef c'
 
 let subst_global subst ref = match ref with
   | VarRef var -> ref, None
   | ConstRef kn ->
-     let kn',t = subst_con subst kn in
+     let kn',t = Mod_subst.subst_con subst kn in
       if kn==kn' then ref, None else ConstRef kn', t
   | IndRef ind ->
-      let ind' = subst_ind subst ind in
+      let ind' = Mod_subst.subst_ind subst ind in
       if ind==ind' then ref, None else IndRef ind', None
   | ConstructRef ((kn,i),j as c) ->
-      let c' = subst_constructor subst c in
+      let c' = Mod_subst.subst_constructor subst c in
       if c'==c then ref,None else ConstructRef c', None
 
 let canonical_gr = function
@@ -118,5 +117,5 @@ module ExtRefMap = HMap.Make(ExtRefOrdered)
 module ExtRefSet = ExtRefMap.Set
 
 let subst_extended_reference sub = function
-  | Abbrev kn -> Abbrev (subst_kn sub kn)
+  | Abbrev kn -> Abbrev (Mod_subst.subst_kn sub kn)
   | TrueGlobal gr -> TrueGlobal (subst_global_reference sub gr)