[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, 8 insertions, 10 deletions

diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index a05612c1b1..f6775ddd1f 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1094,7 +1094,7 @@ let () =
 let () =
   let intern self ist ref = match ref.CAst.v with
   | Tac2qexpr.QHypothesis id ->
-    GlbVal (Globnames.VarRef id), gtypref t_reference
+    GlbVal (GlobRef.VarRef id), gtypref t_reference
   | Tac2qexpr.QReference qid ->
     let gr =
       try Nametab.locate qid
@@ -1106,7 +1106,7 @@ let () =
   let subst s c = Globnames.subst_global_reference s c in
   let interp _ gr = return (Value.of_reference gr) in
   let print _ = function
-  | Globnames.VarRef id -> str "reference:(" ++ str "&" ++ Id.print id ++ str ")"
+  | GlobRef.VarRef id -> str "reference:(" ++ str "&" ++ Id.print id ++ str ")"
   | r -> str "reference:(" ++ Printer.pr_global r ++ str ")"
   in
   let obj = {
diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml
index ee61bdab71..0e6fb94095 100644
--- a/user-contrib/Ltac2/tac2ffi.ml
+++ b/user-contrib/Ltac2/tac2ffi.ml
@@ -10,7 +10,6 @@
 
 open Util
 open Names
-open Globnames
 open Tac2dyn
 open Tac2expr
 open Proofview.Notations
@@ -337,13 +336,13 @@ let of_constant c = of_ext val_constant c
 let to_constant c = to_ext val_constant c
 let constant = repr_ext val_constant
 
-let of_reference = function
+let of_reference = let open GlobRef in function
 | VarRef id -> ValBlk (0, [| of_ident id |])
 | ConstRef cst -> ValBlk (1, [| of_constant cst |])
 | IndRef ind -> ValBlk (2, [| of_ext val_inductive ind |])
 | ConstructRef cstr -> ValBlk (3, [| of_ext val_constructor cstr |])
 
-let to_reference = function
+let to_reference = let open GlobRef in function
 | ValBlk (0, [| id |]) -> VarRef (to_ident id)
 | ValBlk (1, [| cst |]) -> ConstRef (to_constant cst)
 | ValBlk (2, [| ind |]) -> IndRef (to_ext val_inductive ind)
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 6c96ef7742..561bd9c0c5 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -11,7 +11,6 @@
 open Pp
 open Util
 open Names
-open Globnames
 open Tac2types
 open Tac2extffi
 open Genredexpr
@@ -209,13 +208,13 @@ let letin_pat_tac ev ipat na c cl =
     Instead, we parse indifferently any pattern and dispatch when the tactic is
     called. *)
 let map_pattern_with_occs (pat, occ) = match pat with
-| Pattern.PRef (ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst))
-| Pattern.PRef (VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id))
+| Pattern.PRef (GlobRef.ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst))
+| Pattern.PRef (GlobRef.VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id))
 | _ -> (mk_occurrences_expr occ, Inr pat)
 
 let get_evaluable_reference = function
-| VarRef id -> Proofview.tclUNIT (EvalVarRef id)
-| ConstRef cst -> Proofview.tclUNIT (EvalConstRef cst)
+| GlobRef.VarRef id -> Proofview.tclUNIT (EvalVarRef id)
+| GlobRef.ConstRef cst -> Proofview.tclUNIT (EvalConstRef cst)
 | r ->
   Tacticals.New.tclZEROMSG (str "Cannot coerce" ++ spc () ++
     Nametab.pr_global_env Id.Set.empty r ++ spc () ++