diff options
| author | Emilio Jesus Gallego Arias | 2018-10-18 02:18:43 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-18 14:13:50 +0200 |
| commit | 4ac1e342fe420e0b3f3adc9e619d2e98eba2111d (patch) | |
| tree | 26858f7d70c27f0140273686c560f60db0761d58 /vernac/class.ml | |
| parent | 88ecdf6b51b0d7b4cde335cf94297c102d7d551e (diff) | |
[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.
Diffstat (limited to 'vernac/class.ml')
| -rw-r--r-- | vernac/class.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/class.ml b/vernac/class.ml index 614b2181d9..526acd40b5 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -21,7 +21,6 @@ open Environ open Classops open Declare open Globnames -open Nametab open Decl_kinds let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL @@ -310,7 +309,7 @@ let add_coercion_hook poly local ref = | Global -> false in let () = try_add_new_coercion ref ~local poly in - let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in + let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) |