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 /printing/printer.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 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 1f68018678..97b3233d12 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -15,7 +15,6 @@ open Names open Constr open Context open Environ -open Globnames open Evd open Refiner open Constrextern @@ -155,7 +154,7 @@ let pr_in_comment x = str "(* " ++ x ++ str " *)" the [mutual_inductive_body] for the inductives and constructors (needs an environment for this). *) -let id_of_global env = function +let id_of_global env = let open GlobRef in function | ConstRef kn -> Label.to_id (Constant.label kn) | IndRef (kn,0) -> Label.to_id (MutInd.label kn) | IndRef (kn,i) -> @@ -170,7 +169,7 @@ let rec dirpath_of_mp = function | MPdot (mp,l) -> Libnames.add_dirpath_suffix (dirpath_of_mp mp) (Label.to_id l) -let dirpath_of_global = function +let dirpath_of_global = let open GlobRef in function | ConstRef kn -> dirpath_of_mp (Constant.modpath kn) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> dirpath_of_mp (MutInd.modpath kn) @@ -251,7 +250,7 @@ let pr_puniverses f env sigma (c,u) = then f env c ++ pr_universe_instance sigma u else f env c -let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) +let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef cst) let pr_existential_key = Termops.pr_existential_key let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev) let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind) |