[api] Qualify access to `Nametab`

In general, `Nametab` is not a module you want to open globally as it
exposes very generic identifiers such as `push` or `global`.

Thus, we remove all global opens and qualify `Nametab` access. The
patch is small and confirms the hypothesis that `Nametab` access
happens in few places thus it doesn't need a global open.

It is also very convenient to be able to use `grep` to see accesses to
the namespace table.

1 files changed, 6 insertions, 7 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)