[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.

3 files changed, 15 insertions, 18 deletions

diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 0a1cc8745d..a148a3bc73 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open Names
 open Libnames
-open Globnames
 open Constrexpr
 open Constrexpr_ops
 open Notation
@@ -31,7 +30,7 @@ let get_constructors ind =
   let mib,oib = Global.lookup_inductive ind in
   let mc = oib.Declarations.mind_consnames in
   Array.to_list
-    (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
+    (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc)
 
 let qualid_of_ref n =
   n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
@@ -40,7 +39,7 @@ let q_option () = qualid_of_ref "core.option.type"
 
 let unsafe_locate_ind q =
   match Nametab.locate q with
-  | IndRef i -> i
+  | GlobRef.IndRef i -> i
   | _ -> raise Not_found
 
 let locate_z () =
@@ -166,7 +165,7 @@ let vernac_numeral_notation local ty f g scope opts =
        { pt_local = local;
          pt_scope = scope;
          pt_interp_info = NumeralNotation o;
-         pt_required = Nametab.path_of_global (IndRef tyc),[];
+         pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
          pt_refs = constructors;
          pt_in_match = true }
   in
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 1cbc86b6fe..649b51cb0e 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -10,7 +10,6 @@
 
 open Util
 open Names
-open Globnames
 open Glob_term
 open Bigint
 open Constrexpr
@@ -40,9 +39,9 @@ let positive_kn = MutInd.make2 positive_modpath (Label.make "positive")
 let path_of_xI = ((positive_kn,0),1)
 let path_of_xO = ((positive_kn,0),2)
 let path_of_xH = ((positive_kn,0),3)
-let glob_xI = ConstructRef path_of_xI
-let glob_xO = ConstructRef path_of_xO
-let glob_xH = ConstructRef path_of_xH
+let glob_xI = GlobRef.ConstructRef path_of_xI
+let glob_xO = GlobRef.ConstructRef path_of_xO
+let glob_xH = GlobRef.ConstructRef path_of_xH
 
 let pos_of_bignat ?loc x =
   let ref_xI = DAst.make @@ GRef (glob_xI, None) in
@@ -74,9 +73,9 @@ let z_kn = MutInd.make2 positive_modpath (Label.make "Z")
 let path_of_ZERO = ((z_kn,0),1)
 let path_of_POS = ((z_kn,0),2)
 let path_of_NEG = ((z_kn,0),3)
-let glob_ZERO = ConstructRef path_of_ZERO
-let glob_POS = ConstructRef path_of_POS
-let glob_NEG = ConstructRef path_of_NEG
+let glob_ZERO = GlobRef.ConstructRef path_of_ZERO
+let glob_POS = GlobRef.ConstructRef path_of_POS
+let glob_NEG = GlobRef.ConstructRef path_of_NEG
 
 let z_of_int ?loc n =
   if not (Bigint.equal n zero) then
@@ -104,14 +103,14 @@ let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
 let r_modpath = MPfile (make_dir rdefinitions)
 let r_path = make_path rdefinitions "R"
 
-let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
-let glob_Rmult = ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult")
-let glob_Rdiv = ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv")
+let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
+let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult")
+let glob_Rdiv = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv")
 
 let binintdef = ["Coq";"ZArith";"BinIntDef"]
 let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z")
 
-let glob_pow_pos = ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos")
+let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos")
 
 let r_of_rawnum ?loc (sign,n) =
   let n, f, e = NumTok.(n.int, n.frac, n.exp) in
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index bc586acce7..8c0f9a3339 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open Names
 open Libnames
-open Globnames
 open Constrexpr
 open Constrexpr_ops
 open Notation
@@ -23,7 +22,7 @@ let get_constructors ind =
   let mib,oib = Global.lookup_inductive ind in
   let mc = oib.Declarations.mind_consnames in
   Array.to_list
-    (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
+    (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc)
 
 let qualid_of_ref n =
   n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
@@ -92,7 +91,7 @@ let vernac_string_notation local ty f g scope =
        { pt_local = local;
          pt_scope = scope;
          pt_interp_info = StringNotation o;
-         pt_required = Nametab.path_of_global (IndRef tyc),[];
+         pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
          pt_refs = constructors;
          pt_in_match = true }
   in