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

3 files changed, 15 insertions, 18 deletions

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