From c51fb2fae0e196012de47203b8a71c61720d6c5c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Jun 2019 22:50:08 +0200
Subject: [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.
---
 dev/top_printers.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'dev')

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))
-- 
cgit v1.2.3