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

18 files changed, 52 insertions, 70 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 7ce759a3fb..db72dc8ec3 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -21,7 +21,6 @@ open Constr
 open Environ
 open EConstr
 open Vars
-open Nametab
 open Nameops
 open Libnames
 open Globnames
@@ -82,14 +81,14 @@ let is_imported_ref = function
 
 let is_global id =
   try
-    let ref = locate (qualid_of_ident id) in
+    let ref = Nametab.locate (qualid_of_ident id) in
     not (is_imported_ref ref)
   with Not_found ->
     false
 
 let is_constructor id =
   try
-    match locate (qualid_of_ident id) with
+    match Nametab.locate (qualid_of_ident id) with
       | ConstructRef _ -> true
       | _ -> false
   with Not_found ->
@@ -116,7 +115,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
     | Cast (c,_,_) | App (c,_) -> hdrec c
     | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn)))
     | Const _ | Ind _ | Construct _ | Var _ as c ->
-	Some (basename_of_global (global_of_constr c))
+        Some (Nametab.basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
 	Some (match lna.(i) with Name id -> id | _ -> assert false)
     | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None
@@ -148,8 +147,8 @@ let hdchar env sigma c =
     | Cast (c,_,_) | App (c,_) -> hdrec k c
     | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn)))
     | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn))
-    | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
-    | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
+    | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
+    | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
     | Var id  -> lowercase_first_char id
     | Sort s -> sort_hdchar (ESorts.kind sigma s)
     | Rel n ->
@@ -267,7 +266,7 @@ let visible_ids sigma (nenv, c) =
       begin
       try
       let gseen = GlobRef.Set_env.add g gseen in
-      let short = shortest_qualid_of_global Id.Set.empty g in
+      let short = Nametab.shortest_qualid_of_global Id.Set.empty g in
       let dir, id = repr_qualid short in
       let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
       accu := (gseen, vseen, ids)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 98e1f6dd36..601099c6ff 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -26,7 +26,6 @@ open Notation_ops
 open Glob_term
 open Glob_ops
 open Pattern
-open Nametab
 open Notation
 open Detyping
 open Decl_kinds
@@ -213,7 +212,7 @@ let is_record indsp =
   with Not_found -> false
 
 let encode_record r =
-  let indsp = global_inductive r in
+  let indsp = Nametab.global_inductive r in
   if not (is_record indsp) then
     user_err ?loc:r.CAst.loc ~hdr:"encode_record"
       (str "This type is not a structure type.");
@@ -279,7 +278,7 @@ let extern_evar n l = CEvar (n,l)
     may be inaccurate *)
 
 let default_extern_reference ?loc vars r =
-  shortest_qualid_of_global ?loc vars r
+  Nametab.shortest_qualid_of_global ?loc vars r
 
 let my_extern_reference = ref default_extern_reference
 
@@ -481,7 +480,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
                  (make_pat_notation ?loc ntn (l,ll) l2') key)
       end
     | SynDefRule kn ->
-      let qid = shortest_qualid_of_syndef ?loc vars kn in
+      let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in
       let l1 =
         List.rev_map (fun (c,(subentry,(scopt,scl))) ->
           extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
@@ -1136,7 +1135,7 @@ and extern_notation (custom,scopes as allscopes) vars t = function
                 List.map (fun (c,(subentry,(scopt,scl))) ->
                   extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
 		  terms in
-              let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in
+              let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in
 	      CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in
  	if List.is_empty args then e
 	else
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d7497d4e8e..6b22261a15 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -28,7 +28,6 @@ open Constrexpr
 open Constrexpr_ops
 open Notation_term
 open Notation_ops
-open Nametab
 open Notation
 open Inductiveops
 open Decl_kinds
@@ -633,7 +632,7 @@ let terms_of_binders bl =
     | PatVar (Name id)   -> CRef (qualid_of_ident id, None)
     | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
     | PatCstr (c,l,_) ->
-       let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in
+       let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in
        let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
        CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
@@ -721,7 +720,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
           try
             let gc = intern nenv c in
             Id.Map.add id (gc, Some c) map
-          with GlobalizationError _ -> map
+          with Nametab.GlobalizationError _ -> map
         in
         let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
           let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
@@ -986,7 +985,7 @@ let intern_extended_global_of_qualid qid =
 let intern_reference qid =
   let r =
     try intern_extended_global_of_qualid qid
-    with Not_found -> error_global_not_found qid
+    with Not_found -> Nametab.error_global_not_found qid
   in
   Smartlocate.global_of_extended_global r
 
@@ -1058,11 +1057,11 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qi
         (* Extra allowance for non globalizing functions *)
         if !interning_grammar || env.unb then
           (gvar (loc,qualid_basename qid) us, [], [], []), args
-        else error_global_not_found qid
+        else Nametab.error_global_not_found qid
   else
     let r,projapp,args2 =
       try intern_qualid qid intern env ntnvars us args
-      with Not_found -> error_global_not_found qid
+      with Not_found -> Nametab.error_global_not_found qid
     in
     let x, imp, scopes, l = find_appl_head_data r in
     (x,imp,scopes,l), args2
@@ -1312,7 +1311,7 @@ let sort_fields ~complete loc fields completer =
         (* the reference constructor of the record *)
         let base_constructor =
           let global_record_id = ConstructRef record.Recordops.s_CONST in
-          try shortest_qualid_of_global ?loc Id.Set.empty global_record_id
+          try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id
           with Not_found ->
             anomaly (str "Environment corruption for records.") in
         let () = check_duplicate loc fields in
@@ -1493,7 +1492,7 @@ let drop_notations_pattern looked_for genv =
   in
   let rec drop_syndef top scopes qid pats =
     try
-      match locate_extended qid with
+      match Nametab.locate_extended qid with
       | SynDef sp ->
 	let (vars,a) = Syntax_def.search_syntactic_definition sp in
 	(match a with
@@ -1550,7 +1549,7 @@ let drop_notations_pattern looked_for genv =
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
      | CPatCstr (qid, Some expl_pl, pl) ->
-      let g = try locate qid
+      let g = try Nametab.locate qid
 	      with Not_found ->
               raise (InternalizationError (loc,NotAConstructor qid)) in
       if expl_pl == [] then
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index e3d490a1ad..b73d238c22 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -15,7 +15,6 @@ open Names
 open Libnames
 open Libobject
 open Lib
-open Nametab
 open Notation_term
 
 (* Syntactic definitions. *)
@@ -38,7 +37,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
 
 let is_alias_of_already_visible_name sp = function
   | _,NRef ref ->
-      let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in
+      let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in
       DirPath.is_empty dir && Id.equal id (basename sp)
   | _ ->
       false
@@ -83,11 +82,11 @@ let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
 let declare_syntactic_definition local id onlyparse pat =
   let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
 
-let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
+let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)
 
 let pr_compat_warning (kn, def, v) =
   let pp_def = match def with
-    | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r
+    | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r
     | _ -> strbrk " is a compatibility notation"
   in
   pr_syndef kn ++ pp_def
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 677515981a..a044a9a395 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -14,7 +14,6 @@ open Pp
 open Names
 open Libnames
 open Globnames
-open Nametab
 
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
@@ -79,7 +78,7 @@ let register_ref s c =
 (* Generic functions to find Coq objects *)
 
 let has_suffix_in_dirs dirs ref =
-  let dir = dirpath (path_of_global ref) in
+  let dir = dirpath (Nametab.path_of_global ref) in
   List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
 
 let gen_reference_in_modules locstr dirs s =
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 1f2c722b34..a88285c9ee 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -115,7 +115,6 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
 
 (* Summary and Object declaration *)
 
-open Nametab
 open Libobject
 
 type ltac_entry = {
@@ -153,19 +152,19 @@ let tac_deprecation kn =
 
 let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
 | None ->
-  let () = if not local then push_tactic (Until i) sp kn in
+  let () = if not local then push_tactic (Nametab.Until i) sp kn in
   add ~deprecation kn b t
 | Some kn0 -> replace kn0 kn t
 
 let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
 | None ->
-  let () = if not local then push_tactic (Exactly i) sp kn in
+  let () = if not local then push_tactic (Nametab.Exactly i) sp kn in
   add ~deprecation kn b t
 | Some kn0 -> replace kn0 kn t
 
 let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with
 | None ->
-  let () = push_tactic (Until 1) sp kn in
+  let () = push_tactic (Nametab.Until 1) sp kn in
   add ~deprecation kn b t
 | Some kn0 -> replace kn0 kn t
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 5501cf92a5..55412c74bb 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -19,7 +19,6 @@ open Util
 open Names
 open Libnames
 open Globnames
-open Nametab
 open Smartlocate
 open Constrexpr
 open Termops
@@ -98,7 +97,7 @@ let intern_global_reference ist qid =
     ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
   else
     try ArgArg (qid.CAst.loc,locate_global_with_alias qid)
-    with Not_found -> error_global_not_found qid
+    with Not_found -> Nametab.error_global_not_found qid
 
 let intern_ltac_variable ist qid =
   if qualid_is_ident qid && find_var (qualid_basename qid) ist then
@@ -150,7 +149,7 @@ let intern_isolated_tactic_reference strict ist qid =
   try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid))
   with Not_found ->
   (* Reference not found *)
-  error_global_not_found qid
+  Nametab.error_global_not_found qid
 
 (* Internalize an applied tactic reference *)
 
@@ -169,7 +168,7 @@ let intern_applied_tactic_reference ist qid =
   try intern_applied_global_tactic_reference qid
   with Not_found ->
   (* Reference not found *)
-  error_global_not_found qid
+  Nametab.error_global_not_found qid
 
 (* Intern a reference parsed in a non-tactic entry *)
 
@@ -190,7 +189,7 @@ let intern_non_tactic_reference strict ist qid =
     TacGeneric ipat
   else
     (* Reference not found *)
-    error_global_not_found qid
+    Nametab.error_global_not_found qid
 
 let intern_message_token ist = function
   | (MsgString _ | MsgInt _ as x) -> x
@@ -302,7 +301,7 @@ let intern_evaluable_global_reference ist qid =
   try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid)
   with Not_found ->
   if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid)
-  else error_global_not_found qid
+  else Nametab.error_global_not_found qid
 
 let intern_evaluable_reference_or_by_notation ist = function
   | {v=AN r} -> intern_evaluable_global_reference ist r
@@ -377,7 +376,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
          subterm matched when a pattern *)
       let r = match r with
       | {v=AN r} -> r
-      | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in
+      | {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (smart_global r))) in
       let sign = {
         Constrintern.ltac_vars = ist.ltacvars;
         ltac_bound = Id.Set.empty;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f90e889678..b60b77595b 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -23,7 +23,6 @@ open Names
 open Nameops
 open Libnames
 open Globnames
-open Nametab
 open Refiner
 open Tacmach.New
 open Tactic_debug
@@ -358,7 +357,7 @@ let interp_reference ist env sigma = function
     with Not_found ->
       try
         VarRef (get_id (Environ.lookup_named id env))
-      with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
+      with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
 
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
@@ -374,14 +373,14 @@ let interp_evaluable ist env sigma = function
       with Not_found ->
         match r with
         | EvalConstRef _ -> r
-        | _ -> error_global_not_found (qualid_of_ident ?loc id)
+        | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
     end
   | ArgArg (r,None) -> r
   | ArgVar {loc;v=id} ->
     try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try try_interp_evaluable env (loc, id)
-      with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
+      with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
 
 (* Interprets an hypothesis name *)
 let interp_occurrences ist occs =
@@ -640,7 +639,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
         Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
      with Not_found ->
-       error_global_not_found (qualid_of_ident ?loc id))
+       Nametab.error_global_not_found (qualid_of_ident ?loc id))
   | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
   | Inr c -> Inr (interp_typed_pattern ist env sigma c) in
   interp_occurrences ist occs, p
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b026397abf..73141191cf 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -15,7 +15,6 @@ open Names
 open Constr
 open Libnames
 open Globnames
-open Nametab
 open Libobject
 open Mod_subst
 
@@ -228,14 +227,14 @@ let string_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
   | CL_CONST sp ->
-    string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+    string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp))
   | CL_PROJ sp ->
     let sp = Projection.Repr.constant sp in
-    string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+    string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp))
   | CL_IND sp ->
-      string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp))
+      string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp))
   | CL_SECVAR sp ->
-      string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp))
+      string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp))
 
 let pr_class x = str (string_of_class x)
 
@@ -520,7 +519,7 @@ module CoercionPrinting =
     let compare = GlobRef.Ordered.compare
     let encode = coercion_of_reference
     let subst = subst_coe_typ
-    let printer x = pr_global_env Id.Set.empty x
+    let printer x = Nametab.pr_global_env Id.Set.empty x
     let key = ["Printing";"Coercion"]
     let title = "Explicitly printed coercions: "
     let member_message x b =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 592057ab41..072ac9deed 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -25,7 +25,6 @@ open Termops
 open Namegen
 open Libnames
 open Globnames
-open Nametab
 open Mod_subst
 open Decl_kinds
 open Context.Named.Declaration
@@ -58,7 +57,7 @@ let add_name_opt na b t (nenv, env) =
 (* Tools for printing of Cases                                              *)
 
 let encode_inductive r =
-  let indsp = global_inductive r in
+  let indsp = Nametab.global_inductive r in
   let constr_lengths = constructors_nrealargs indsp in
   (indsp,constr_lengths)
 
@@ -97,7 +96,7 @@ module PrintingInductiveMake =
     let compare = ind_ord
     let encode = Test.encode
     let subst subst obj = subst_ind subst obj
-    let printer ind = pr_global_env Id.Set.empty (IndRef ind)
+    let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind)
     let key = ["Printing";Test.field]
     let title = Test.title
     let member_message x = Test.member_message (printer x)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index e49ba75b3f..89f64d328a 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -29,7 +29,6 @@ open Inductive
 open Inductiveops
 open Environ
 open Reductionops
-open Nametab
 open Context.Rel.Declaration
 
 type dep_flag = bool
@@ -618,6 +617,6 @@ let lookup_eliminator ind_sp s =
     user_err ~hdr:"default_elim"
       (strbrk "Cannot find the elimination combinator " ++
        Id.print id ++ strbrk ", the elimination of the inductive definition " ++
-       pr_global_env Id.Set.empty (IndRef ind_sp) ++
+       Nametab.pr_global_env Id.Set.empty (IndRef ind_sp) ++
        strbrk " on sort " ++ Termops.pr_sort_family s ++
        strbrk " is probably not allowed.")
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f8dc5ba4d6..5d74b59b27 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -20,7 +20,6 @@ open Util
 open Pp
 open Names
 open Globnames
-open Nametab
 open Constr
 open Libobject
 open Mod_subst
@@ -330,7 +329,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 let error_not_structure ref description =
   user_err ~hdr:"object_declare"
     (str"Could not declare a canonical structure " ++
-       (Id.print (basename_of_global ref) ++ str"." ++ spc() ++
+       (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++
           description))
 
 let check_and_decompose_canonical_structure ref =
diff --git a/printing/printer.ml b/printing/printer.ml
index 990bdaad7d..3cf995a005 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -15,7 +15,6 @@ open Names
 open Constr
 open Environ
 open Globnames
-open Nametab
 open Evd
 open Refiner
 open Constrextern
@@ -242,7 +241,7 @@ let pr_abstract_cumulativity_info sigma cumi =
 (**********************************************************************)
 (* Global references *)
 
-let pr_global_env = pr_global_env
+let pr_global_env = Nametab.pr_global_env
 let pr_global = pr_global_env Id.Set.empty
 
 let pr_universe_instance evd inst =
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 ->