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 /dev/top_printers.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 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 8343853af5..aa28bce018 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -15,7 +15,6 @@ open Util open Pp open Names open Libnames -open Globnames open Univ open Environ open Printer @@ -141,7 +140,7 @@ let ppclosedglobconstridmap x = pp (pr_closed_glob_constr_idmap x) let pP s = pp (hov 0 s) -let safe_pr_global = function +let safe_pr_global = let open GlobRef in function | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")") | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++ int i ++ str ")") @@ -558,7 +557,7 @@ let encode_path ?loc prefix mpdir suffix id = make_qualid ?loc (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id -let raw_string_of_ref ?loc _ = function +let raw_string_of_ref ?loc _ = let open GlobRef in function | ConstRef cst -> let (mp,id) = Constant.repr2 cst in encode_path ?loc "CST" (Some mp) [] (Label.to_id id) @@ -574,7 +573,7 @@ let raw_string_of_ref ?loc _ = function | VarRef id -> encode_path ?loc "SECVAR" None [] id -let short_string_of_ref ?loc _ = function +let short_string_of_ref ?loc _ = let open GlobRef in function | VarRef id -> qualid_of_ident ?loc id | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (Constant.label cst)) | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (MutInd.label kn)) |