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

5 files changed, 14 insertions, 17 deletions

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index db8d09b79e..0e38ce575b 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -194,7 +194,7 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_evaluable_reference = function
     | EvalVarRef id -> pr_id id
-    | EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
+    | EvalConstRef sp -> pr_global (GlobRef.ConstRef sp)
 
   let pr_quantified_hypothesis = function
     | AnonHyp n -> int n
@@ -385,7 +385,7 @@ let string_of_genarg_arg (ArgumentType arg) =
   let pr_evaluable_reference_env env = function
     | EvalVarRef id -> pr_id id
     | EvalConstRef sp ->
-      Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
+      Nametab.pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef sp)
 
   let pr_as_disjunctive_ipat prc ipatl =
     keyword "as" ++ spc () ++
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 13844c2707..726752a2bf 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -24,7 +24,6 @@ open Tactics
 open Pretype_errors
 open Typeclasses
 open Constrexpr
-open Globnames
 open Evd
 open Tactypes
 open Locus
@@ -1983,8 +1982,8 @@ let add_morphism_as_parameter atts m n : unit =
       (Declare.ParameterEntry (None,(instance,uctx),None))
   in
   Classes.add_instance (Classes.mk_instance
-                  (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
-  declare_projection n instance_id (ConstRef cst)
+                  (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (GlobRef.ConstRef cst));
+  declare_projection n instance_id (GlobRef.ConstRef cst)
 
 let add_morphism_interactive atts m n : Lemmas.t =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
@@ -1997,11 +1996,11 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let kind = Decls.(IsDefinition Instance) in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
   let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
-    | Globnames.ConstRef cst ->
+    | GlobRef.ConstRef cst ->
       Classes.add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info
-                      atts.global (ConstRef cst));
-      declare_projection n instance_id (ConstRef cst)
+                      atts.global (GlobRef.ConstRef cst));
+      declare_projection n instance_id (GlobRef.ConstRef cst)
     | _ -> assert false
   in
   let hook = DeclareDef.Hook.make hook in
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4e79bab28e..e64129d204 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -203,11 +203,11 @@ let id_of_name = function
         end
        | Const (cst,_) -> Label.to_id (Constant.label cst)
        | Construct (cstr,_) ->
-	  let ref = Globnames.ConstructRef cstr in
+          let ref = GlobRef.ConstructRef cstr in
 	  let basename = Nametab.basename_of_global ref in
 	  basename
        | Ind (ind,_) ->
-	  let ref = Globnames.IndRef ind in
+          let ref = GlobRef.IndRef ind in
 	  let basename = Nametab.basename_of_global ref in
 	  basename
        | Sort s ->
@@ -290,7 +290,7 @@ let coerce_to_evaluable_ref env sigma v =
     if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
     else fail ()
   else if has_type v (topwit wit_ref) then
-    let open Globnames in
+    let open GlobRef in
     let r = out_gen (topwit wit_ref) v in
     match r with
     | VarRef var -> EvalVarRef var
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 3ed5b1aab2..63559cf488 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -18,7 +18,6 @@ open Tacred
 open Util
 open Names
 open Libnames
-open Globnames
 open Smartlocate
 open Constrexpr
 open Termops
@@ -304,7 +303,7 @@ let intern_evaluable_reference_or_by_notation ist = function
   | {v=ByNotation (ntn,sc);loc} ->
       evaluable_of_global_reference ist.genv
       (Notation.interp_notation_as_global_reference ?loc
-        (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
+        GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
 (* Globalize a reduction expression *)
 let intern_evaluable ist r =
@@ -383,7 +382,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       | GRef (r,None) ->
           Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
       | GVar id ->
-          let r = evaluable_of_global_reference ist.genv (VarRef id) in
+          let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in
           Inl (ArgArg (r,None))
       | _ ->
           let bound_names = Glob_ops.bound_glob_vars c in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 8ddf17ca14..c252372f21 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -22,7 +22,6 @@ open Util
 open Names
 open Nameops
 open Libnames
-open Globnames
 open Refiner
 open Tacmach.New
 open Tactic_debug
@@ -369,14 +368,14 @@ let interp_reference ist env sigma = function
     try try_interp_ltac_var (coerce_to_reference sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try
-        VarRef (get_id (Environ.lookup_named id env))
+        GlobRef.VarRef (get_id (Environ.lookup_named id env))
       with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
 
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
   match v with
   | LocalDef _ -> EvalVarRef id
-  | _ -> error_not_evaluable (VarRef id)
+  | _ -> error_not_evaluable (GlobRef.VarRef id)
 
 let interp_evaluable ist env sigma = function
   | ArgArg (r,Some {loc;v=id}) ->