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.
---
 library/coqlib.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/coqlib.ml b/library/coqlib.ml
index 677515981a..a044a9a395 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -14,7 +14,6 @@ open Pp
 open Names
 open Libnames
 open Globnames
-open Nametab
 
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
@@ -79,7 +78,7 @@ let register_ref s c =
 (* Generic functions to find Coq objects *)
 
 let has_suffix_in_dirs dirs ref =
-  let dir = dirpath (path_of_global ref) in
+  let dir = dirpath (Nametab.path_of_global ref) in
   List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
 
 let gen_reference_in_modules locstr dirs s =
-- 
cgit v1.2.3