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

3 files changed, 13 insertions, 16 deletions

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