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 /pretyping/classops.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 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 11 |
1 files changed, 5 insertions, 6 deletions
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 = |