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

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 990bdaad7d..3cf995a005 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -15,7 +15,6 @@ open Names
 open Constr
 open Environ
 open Globnames
-open Nametab
 open Evd
 open Refiner
 open Constrextern
@@ -242,7 +241,7 @@ let pr_abstract_cumulativity_info sigma cumi =
 (**********************************************************************)
 (* Global references *)
 
-let pr_global_env = pr_global_env
+let pr_global_env = Nametab.pr_global_env
 let pr_global = pr_global_env Id.Set.empty
 
 let pr_universe_instance evd inst =
-- 
cgit v1.2.3