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 /engine/namegen.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 'engine/namegen.ml')
| -rw-r--r-- | engine/namegen.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index 7ce759a3fb..db72dc8ec3 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -21,7 +21,6 @@ open Constr open Environ open EConstr open Vars -open Nametab open Nameops open Libnames open Globnames @@ -82,14 +81,14 @@ let is_imported_ref = function let is_global id = try - let ref = locate (qualid_of_ident id) in + let ref = Nametab.locate (qualid_of_ident id) in not (is_imported_ref ref) with Not_found -> false let is_constructor id = try - match locate (qualid_of_ident id) with + match Nametab.locate (qualid_of_ident id) with | ConstructRef _ -> true | _ -> false with Not_found -> @@ -116,7 +115,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *) | Cast (c,_,_) | App (c,_) -> hdrec c | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn))) | Const _ | Ind _ | Construct _ | Var _ as c -> - Some (basename_of_global (global_of_constr c)) + Some (Nametab.basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i) with Name id -> id | _ -> assert false) | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None @@ -148,8 +147,8 @@ let hdchar env sigma c = | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn)) - | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") - | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") | Var id -> lowercase_first_char id | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> @@ -267,7 +266,7 @@ let visible_ids sigma (nenv, c) = begin try let gseen = GlobRef.Set_env.add g gseen in - let short = shortest_qualid_of_global Id.Set.empty g in + let short = Nametab.shortest_qualid_of_global Id.Set.empty g in let dir, id = repr_qualid short in let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in accu := (gseen, vseen, ids) |