diff options
| author | Gaëtan Gilbert | 2019-07-11 12:18:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-11 12:18:18 +0200 |
| commit | b424691372a61de64b8b9a8c94ef0c9cb61c7274 (patch) | |
| tree | 60c2cc24ad7550f07cb06aedfb2a3c5402f016ce /dev | |
| parent | 195772efccbac6663501bd5fff63c318d22ee191 (diff) | |
| parent | c51fb2fae0e196012de47203b8a71c61720d6c5c (diff) | |
Merge PR #10498: [api] Deprecate GlobRef constructors.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Diffstat (limited to 'dev')
| -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)) |