Merge PR #8758: [api] Qualify access to `Nametab`

5 files changed, 7 insertions, 12 deletions

diff --git a/vernac/class.ml b/vernac/class.ml
index 614b2181d9..526acd40b5 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -21,7 +21,6 @@ open Environ
 open Classops
 open Declare
 open Globnames
-open Nametab
 open Decl_kinds
 
 let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL
@@ -310,7 +309,7 @@ let add_coercion_hook poly local ref =
   | Global -> false
   in
   let () = try_add_new_coercion ref ~local poly in
-  let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
+  let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
 let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3cf5e9bfdf..52c1e1cf98 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -12,7 +12,6 @@
 module CVars = Vars
 open Names
 open EConstr
-open Nametab
 open CErrors
 open Util
 open Typeclasses_errors
@@ -67,7 +66,7 @@ let intern_info {hint_priority;hint_pattern} =
 
 (** TODO: add subinstances *)
 let existing_instance glob g info =
-  let c = global g in
+  let c = Nametab.global g in
   let info = Option.default Hints.empty_hint_info info in
   let info = intern_info info in
   let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 7b28895814..885a22b209 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -22,7 +22,6 @@ open Nameops
 open Constrexpr
 open Constrexpr_ops
 open Constrintern
-open Nametab
 open Impargs
 open Reductionops
 open Indtypes
@@ -575,6 +574,6 @@ let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite =
   (* Declare the possible notations of inductive types *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes;
+  List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes;
   (* If positivity is assumed declares itself as unsafe. *)
   if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 5f2818c12b..4efbb968fb 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -33,7 +33,6 @@ open Globnames
 open Goptions
 open Nameops
 open Termops
-open Nametab
 open Smartlocate
 open Vernacexpr
 open Ind_tables
@@ -369,7 +368,7 @@ requested
               | InSet -> recs ^ "_nodep"
               | InType -> recs ^ "t_nodep")
         ) in
-        let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
+        let newid = add_suffix (Nametab.basename_of_global (IndRef ind)) suffix in
         let newref = CAst.make newid in
           ((newref,isdep,ind,z)::l1),l2
       in
diff --git a/vernac/search.ml b/vernac/search.ml
index 04dcb7d565..2273130668 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -18,7 +18,6 @@ open Environ
 open Pattern
 open Libnames
 open Globnames
-open Nametab
 
 module NamedDecl = Context.Named.Declaration
 
@@ -192,7 +191,7 @@ let rec head_filter pat ref env sigma typ =
   | _ -> false
 
 let full_name_of_reference ref =
-  let (dir,id) = repr_path (path_of_global ref) in
+  let (dir,id) = repr_path (Nametab.path_of_global ref) in
   DirPath.to_string dir ^ "." ^ Id.to_string id
 
 (** Whether a reference is blacklisted *)
@@ -204,14 +203,14 @@ let blacklist_filter_aux () =
   List.for_all is_not_bl l
 
 let module_filter (mods, outside) ref env typ =
-  let sp = path_of_global ref in
+  let sp = Nametab.path_of_global ref in
   let sl = dirpath sp in
   let is_outside md = not (is_dirpath_prefix_of md sl) in
   let is_inside md = is_dirpath_prefix_of md sl in
   if outside then List.for_all is_outside mods
   else List.is_empty mods || List.exists is_inside mods
 
-let name_of_reference ref = Id.to_string (basename_of_global ref)
+let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref)
 
 let search_about_filter query gr env typ = match query with
 | GlobSearchSubPattern pat ->