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/constrextern.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/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 98e1f6dd36..601099c6ff 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -26,7 +26,6 @@ open Notation_ops open Glob_term open Glob_ops open Pattern -open Nametab open Notation open Detyping open Decl_kinds @@ -213,7 +212,7 @@ let is_record indsp = with Not_found -> false let encode_record r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in if not (is_record indsp) then user_err ?loc:r.CAst.loc ~hdr:"encode_record" (str "This type is not a structure type."); @@ -279,7 +278,7 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - shortest_qualid_of_global ?loc vars r + Nametab.shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference @@ -481,7 +480,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key) end | SynDefRule kn -> - let qid = shortest_qualid_of_syndef ?loc vars kn in + let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in let l1 = List.rev_map (fun (c,(subentry,(scopt,scl))) -> extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) @@ -1136,7 +1135,7 @@ and extern_notation (custom,scopes as allscopes) vars t = function List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c, None) terms in - let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in + let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else |