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 /interp/syntax_def.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 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index e3d490a1ad..b73d238c22 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -15,7 +15,6 @@ open Names open Libnames open Libobject open Lib -open Nametab open Notation_term (* Syntactic definitions. *) @@ -38,7 +37,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = let is_alias_of_already_visible_name sp = function | _,NRef ref -> - let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in + let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in DirPath.is_empty dir && Id.equal id (basename sp) | _ -> false @@ -83,11 +82,11 @@ let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () -let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) +let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) let pr_compat_warning (kn, def, v) = let pp_def = match def with - | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r + | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r | _ -> strbrk " is a compatibility notation" in pr_syndef kn ++ pp_def |