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/constrextern.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'interp/constrextern.ml')

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