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

4 files changed, 9 insertions, 13 deletions

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 =