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.
---
 pretyping/classops.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'pretyping/classops.ml')

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