diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 22:50:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 15:59:10 +0200 |
| commit | c51fb2fae0e196012de47203b8a71c61720d6c5c (patch) | |
| tree | e49c2d38b6c841dc6514944750d21ed08ab94bce /engine/namegen.ml | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
[api] Deprecate GlobRef constructors.
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
Diffstat (limited to 'engine/namegen.ml')
| -rw-r--r-- | engine/namegen.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index 77d45ce1e4..89c2fade62 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -24,7 +24,6 @@ open EConstr open Vars open Nameops open Libnames -open Globnames open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -72,7 +71,7 @@ let is_imported_modpath = function in find_prefix (Lib.current_mp ()) | _ -> false -let is_imported_ref = function +let is_imported_ref = let open GlobRef in function | VarRef _ -> false | IndRef (kn,_) | ConstructRef ((kn,_),_) -> @@ -90,7 +89,7 @@ let is_global id = let is_constructor id = try match Nametab.locate (qualid_of_ident id) with - | ConstructRef _ -> true + | GlobRef.ConstructRef _ -> true | _ -> false with Not_found -> false @@ -102,7 +101,7 @@ let is_section_variable id = (**********************************************************************) (* Generating "intuitive" names from its type *) -let global_of_constr = function +let global_of_constr = let open GlobRef in function | Const (c, _) -> ConstRef c | Ind (i, _) -> IndRef i | Construct (c, _) -> ConstructRef c @@ -149,8 +148,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 (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") + | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.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 -> |