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

6 files changed, 23 insertions, 19 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index a476381b17..d74935721f 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -13,7 +13,6 @@ open Constr
 open EConstr
 open Names
 open Pattern
-open Globnames
 
 (* Discrimination nets with bounded depth.
    See the module dn.ml for further explanations.
@@ -36,7 +35,7 @@ type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
 let decomp_pat =
   let rec decrec acc = function
     | PApp (f,args) -> decrec (Array.to_list args @ acc) f
-    | PProj (p, c) -> (PRef (ConstRef (Projection.constant p)), c :: acc)
+    | PProj (p, c) -> (PRef (GlobRef.ConstRef (Projection.constant p)), c :: acc)
     | c -> (c,acc)
   in
   decrec []
@@ -51,6 +50,7 @@ let decomp sigma t =
     decrec [] t
 
 let constr_val_discr sigma t =
+  let open GlobRef in
   let c, l = decomp sigma t in
     match EConstr.kind sigma c with
     | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
@@ -63,6 +63,7 @@ let constr_pat_discr t =
   if not (Patternops.occur_meta_pattern t) then
     None
   else
+    let open GlobRef in
     match decomp_pat t with
     | PRef ((IndRef _) as ref), args
     | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
@@ -71,6 +72,7 @@ let constr_pat_discr t =
 
 let constr_val_discr_st sigma ts t =
   let c, l = decomp sigma t in
+  let open GlobRef in
     match EConstr.kind sigma c with
     | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l)
     | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
@@ -86,6 +88,7 @@ let constr_val_discr_st sigma ts t =
     | _ -> Nothing
 
 let constr_pat_discr_st ts t =
+  let open GlobRef in
   match decomp_pat t with
   | PRef ((IndRef _) as ref), args
   | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 303ddacb67..ce06e656ed 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -25,7 +25,6 @@ open Tacmach
 open Tactics
 open Clenv
 open Typeclasses
-open Globnames
 open Evd
 open Locus
 open Proofview.Notations
@@ -517,8 +516,8 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
   let rec iscl env ty =
     let ctx, ar = decompose_prod_assum sigma ty in
       match EConstr.kind sigma (fst (decompose_app sigma ar)) with
-      | Const (c,_) -> is_class (ConstRef c)
-      | Ind (i,_) -> is_class (IndRef i)
+      | Const (c,_) -> is_class (GlobRef.ConstRef c)
+      | Ind (i,_) -> is_class (GlobRef.IndRef i)
       | _ ->
           let env' = push_rel_context ctx env in
           let ty' = Reductionops.whd_all env' sigma ar in
@@ -529,10 +528,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
   let keep = not only_classes || is_class in
     if keep then
       let c = mkVar id in
-      let name = PathHints [VarRef id] in
+      let name = PathHints [GlobRef.VarRef id] in
       let hints =
         if is_class then
-          let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in
+          let hints = build_subclasses ~check:false env sigma (GlobRef.VarRef id) empty_hint_info in
             (List.map_append
              (fun (path,info,c) ->
               make_resolves env sigma ~name:(PathHints path)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 98db6cbb97..7c90c59f61 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -380,7 +380,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
 	     Logic.eq or Jmeq just before *)
 	assert false
     in
-        pf_constr_of_global (ConstRef c)
+        pf_constr_of_global (GlobRef.ConstRef c)
   else
   let scheme_name = match dep, lft2rgt, inccl with
     (* Non dependent case *)
@@ -399,7 +399,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
       
       let c, eff = find_scheme scheme_name ind in 
       Proofview.tclEFFECTS eff <*>
-        pf_constr_of_global (ConstRef c) 
+        pf_constr_of_global (GlobRef.ConstRef c)
   | _ -> assert false
   end
 
@@ -989,7 +989,7 @@ let ind_scheme_of_eq lbeq to_kind =
   (* use ind rather than case by compatibility *)
   let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in
   let c, eff = find_scheme kind (destIndRef lbeq.eq) in
-    ConstRef c, eff
+    GlobRef.ConstRef c, eff
 
 
 let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 8d1c536db6..131832be89 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -48,6 +48,7 @@ let head_constr_bound sigma t =
   let t = strip_outer_cast sigma t in
   let _,ccl = decompose_prod_assum sigma t in
   let hd,args = decompose_app sigma ccl in
+  let open GlobRef in
   match EConstr.kind sigma hd with
   | Const (c, _) -> ConstRef c
   | Ind (i, _) -> IndRef i
@@ -65,6 +66,7 @@ let decompose_app_bound sigma t =
   let t = strip_outer_cast sigma t in
   let _,ccl = decompose_prod_assum sigma t in
   let hd,args = decompose_app_vect sigma ccl in
+  let open GlobRef in
   match EConstr.kind sigma hd with
     | Const (c,u) -> ConstRef c, args
     | Ind (i,u) -> IndRef i, args
@@ -295,7 +297,7 @@ let lookup_tacs sigma concl st se =
   let sl' = List.stable_sort pri_order_int l' in
   List.merge pri_order_int se.sentry_nopat sl'
 
-let is_transparent_gr ts = function
+let is_transparent_gr ts = let open GlobRef in function
   | VarRef id -> TransparentState.is_transparent_variable ts id
   | ConstRef cst -> TransparentState.is_transparent_constant ts cst
   | IndRef _ | ConstructRef _ -> false
@@ -919,7 +921,7 @@ let make_resolve_hyp env sigma decl =
   let c = mkVar hname in
   try
     [make_apply_entry env sigma (true, true, false) empty_hint_info ~poly:false
-       ~name:(PathHints [VarRef hname])
+       ~name:(PathHints [GlobRef.VarRef hname])
        (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
     | Failure _ -> []
@@ -1326,7 +1328,7 @@ let project_hint ~poly pri l2r r =
       ~name ~kind:Decls.(IsDefinition Definition) cb
   in
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
-    (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c))
+    (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c))
 
 let interp_hints ~poly =
   fun h ->
@@ -1376,7 +1378,7 @@ let interp_hints ~poly =
         Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
           List.init (nconstructors env ind)
 	    (fun i -> let c = (ind,i+1) in
-		      let gr = ConstructRef c in
+                      let gr = GlobRef.ConstructRef c in
 			empty_hint_info, 
                         (Declareops.inductive_is_polymorphic mib), true,
 			PathHints [gr], IsGlobRef gr)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9dabe56816..6fd18b83d1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -24,7 +24,6 @@ open Namegen
 open Declarations
 open Inductiveops
 open Reductionops
-open Globnames
 open Evd
 open Tacred
 open Genredexpr
@@ -921,14 +920,14 @@ let is_local_flag env flags =
   else
     let check = function
     | EvalVarRef _ -> false
-    | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c))
+    | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (GlobRef.ConstRef c))
     in
     List.for_all check flags.rConst
 
 let is_local_unfold env flags =
   let check (_, c) = match c with
   | EvalVarRef _ -> false
-  | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c))
+  | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (GlobRef.ConstRef c))
   in
   List.for_all check flags
 
@@ -975,8 +974,8 @@ let reduce redexp cl =
 (* Unfolding occurrences of a constant *)
 
 let unfold_constr = function
-  | ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp]
-  | VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id]
+  | GlobRef.ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp]
+  | GlobRef.VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id]
   | _ -> user_err ~hdr:"unfold_constr" (str "Cannot unfold a non-constant.")
 
 (*******************************************)
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index c3132ed6f0..ccd7a818b9 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -289,6 +289,7 @@ struct
   open TDnet
 
   let pat_of_constr c : term_pattern =
+    let open GlobRef in
     (* To each evar we associate a unique identifier. *)
     let metas = ref Evar.Map.empty in
     let rec pat_of_constr c = match Constr.kind c with