From 4ac1e342fe420e0b3f3adc9e619d2e98eba2111d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 18 Oct 2018 02:18:43 +0200
Subject: [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.
---
 interp/syntax_def.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'interp/syntax_def.ml')

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
-- 
cgit v1.2.3