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

8 files changed, 26 insertions, 31 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0efb27e3f0..08298bf02c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -14,7 +14,6 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Libnames
-open Globnames
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -1027,7 +1026,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
               update_Function
                 {finfos with
                    equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
-                                              ConstRef c -> c
+                                              GlobRef.ConstRef c -> c
                                             | _ -> CErrors.anomaly (Pp.str "Not a constant.")
                                          )
                 }
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index cb7a509829..d34faa22fa 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -84,7 +84,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in
   let rel_as_kn =
     fst (match princ_type_info.indref with
-           | Some (Globnames.IndRef ind) -> ind
+           | Some (GlobRef.IndRef ind) -> ind
            | _ -> user_err Pp.(str "Not a valid predicate")
         )
   in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index bcad6cedf1..6dc01a9f8f 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -6,7 +6,6 @@ open Context
 open Vars
 open Glob_term
 open Glob_ops
-open Globnames
 open Indfun_common
 open CErrors
 open Util
@@ -312,7 +311,7 @@ let build_constructors_of_type ind' argl =
   let npar = mib.Declarations.mind_nparams in
   Array.mapi (fun i _ ->
 		let construct = ind',i+1 in
-		let constructref = ConstructRef(construct) in
+                let constructref = GlobRef.ConstructRef(construct) in
 		let _implicit_positions_of_cst =
 		  Impargs.implicits_of_global constructref
 		in
@@ -328,7 +327,7 @@ let build_constructors_of_type ind' argl =
                     List.make npar (mkGHole ()) @ argl
 		in
 		let pat_as_term =
-		  mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
+                  mkGApp(mkGRef (GlobRef.ConstructRef(ind',i+1)),argl)
 		in
                 cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term
 	     )
@@ -438,7 +437,7 @@ let rec pattern_to_term_and_type env typ  = DAst.with_val (function
       let patl_as_term =
 	List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
       in
-      mkGApp(mkGRef(ConstructRef constr),
+      mkGApp(mkGRef(GlobRef.ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
   )
@@ -992,7 +991,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
-		    let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
+                    let jmeq = GlobRef.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
 		    let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
                     let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in
 		    let mib,_ = Global.lookup_inductive (fst ind) in
@@ -1001,7 +1000,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      ((Util.List.chop nparam args'))
 		    in
 		    let rt_typ = DAst.make @@
-		       GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None),
+                       GApp(DAst.make @@ GRef (GlobRef.IndRef (fst ind),None),
 			    (List.map
 			      (fun p -> Detyping.detype Detyping.Now false Id.Set.empty
 				 env (Evd.from_env env)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 7b758da8e8..d36d86a65b 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -375,7 +375,7 @@ let rec pattern_to_term pt = DAst.with_val (function
       let patl_as_term =
 	List.map pattern_to_term patternl
       in
-      mkGApp(mkGRef(Globnames.ConstructRef constr),
+      mkGApp(mkGRef(GlobRef.ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
   ) pt
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 48e3129599..99efe3e5e2 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -8,7 +8,6 @@ open EConstr
 open Pp
 open Indfun_common
 open Libnames
-open Globnames
 open Glob_term
 open Declarations
 open Tactypes
@@ -59,7 +58,7 @@ let functional_induction with_clean c princl pat =
               let princ,g' =  (* then we get the principle *)
                 try
                   let g',princ =
-                    Tacmach.pf_eapply (Evd.fresh_global) g  (Globnames.ConstRef (Option.get princ_option )) in
+                    Tacmach.pf_eapply (Evd.fresh_global) g  (GlobRef.ConstRef (Option.get princ_option )) in
                   princ,g'
                 with Option.IsNone ->
                   (*i If there is not default lemma defined then,
@@ -836,7 +835,7 @@ let make_graph (f_ref : GlobRef.t) =
   let sigma = Evd.from_env env in
   let c,c_body =
     match f_ref with
-    | ConstRef c ->
+    | GlobRef.ConstRef c ->
       begin try c,Global.lookup_constant c
         with Not_found ->
           raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) )
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c906670dc0..a119586f7b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -2,7 +2,6 @@ open Names
 open Pp
 open Constr
 open Libnames
-open Globnames
 open Refiner
 
 let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
@@ -31,12 +30,12 @@ let locate qid = Nametab.locate qid
 
 let locate_ind ref =
   match locate ref with
-    | IndRef x -> x
+    | GlobRef.IndRef x -> x
     | _ -> raise Not_found
 
 let locate_constant ref =
   match locate ref with
-    | ConstRef x -> x
+    | GlobRef.ConstRef x -> x
     | _ -> raise Not_found
 
 
@@ -129,10 +128,10 @@ let save name const ?hook uctx scope kind =
     | Discharge ->
       let c = SectionLocalDef const in
       let () = declare_variable ~name ~kind c in
-      VarRef name
+      GlobRef.VarRef name
     | Global local ->
       let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
-      ConstRef kn
+      GlobRef.ConstRef kn
   in
   DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
   definition_message name
@@ -275,7 +274,7 @@ let pr_info env sigma f_info =
   str "function_constant_type := " ++
   (try
      Printer.pr_lconstr_env env sigma
-       (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant)))
+       (fst (Typeops.type_of_global_in_context env (GlobRef.ConstRef f_info.function_constant)))
    with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
   str "equation_lemma := " ++ pr_ocst env sigma f_info.equation_lemma ++ fnl () ++
   str "completeness_lemma :=" ++ pr_ocst env sigma f_info.completeness_lemma ++ fnl () ++
@@ -299,7 +298,7 @@ let in_Function : function_info -> Libobject.obj =
 
 let find_or_none id =
   try Some
-    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
+    (match Nametab.locate (qualid_of_ident id) with GlobRef.ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
     )
   with Not_found -> None
 
@@ -328,7 +327,7 @@ let add_Function is_general f =
   and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
-    with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
+    with | GlobRef.IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
   in
   let finfos =
     { function_constant = f;
@@ -433,8 +432,8 @@ let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
 
 let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
   match r with
-      ConstRef sp -> EvalConstRef sp
-    | VarRef id -> EvalVarRef id
+      GlobRef.ConstRef sp -> EvalConstRef sp
+    | GlobRef.VarRef id -> EvalVarRef id
     | _ -> assert false;;
 
 let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8fa001278b..d4cc31c0af 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -19,7 +19,6 @@ open Context
 open EConstr
 open Vars
 open Pp
-open Globnames
 open Tacticals
 open Tactics
 open Indfun_common
@@ -93,7 +92,7 @@ let make_eq () =
 let generate_type evd g_to_f f graph i =
   (*i we deduce the number of arguments of the function and its returned type from the graph i*)
   let evd',graph =
-    Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd !evd graph)))
+    Evd.fresh_global  (Global.env ()) !evd  (GlobRef.IndRef (fst (destInd !evd graph)))
   in
   evd:=evd';
   let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in
@@ -165,7 +164,7 @@ let find_induction_principle evd f =
   match infos.rect_lemma with
     | None -> raise Not_found
     | Some rect_lemma ->
-       let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
+       let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (GlobRef.ConstRef rect_lemma) in
        let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
        evd:=evd';
        rect_lemma,typ
@@ -978,7 +977,7 @@ let error msg = user_err Pp.(str msg)
 let invfun qhyp f  =
   let f =
     match f with
-      | ConstRef f -> f
+      | GlobRef.ConstRef f -> f
       | _ -> raise (CErrors.UserError(None,str "Not a function"))
   in
   try
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f4edbda04a..2d8f075aba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -67,7 +67,7 @@ let find_reference sl s =
 
 let declare_fun name kind ?univs value =
   let ce = definition_entry ?univs value (*FIXME *) in
-  ConstRef(declare_constant ~name ~kind (DefinitionEntry ce))
+  GlobRef.ConstRef(declare_constant ~name ~kind (DefinitionEntry ce))
 
 let defined lemma =
   Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None
@@ -95,7 +95,7 @@ let type_of_const sigma t =
 let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s)
 
 let const_of_ref = function
-    ConstRef kn -> kn
+    GlobRef.ConstRef kn -> kn
   | _ -> anomaly (Pp.str "ConstRef expected.")
 
 (* Generic values *)
@@ -1312,7 +1312,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
       let na_ref = qualid_of_ident na in
       let na_global = Smartlocate.global_with_alias na_ref in
       match na_global with
-          ConstRef c -> is_opaque_constant c
+          GlobRef.ConstRef c -> is_opaque_constant c
         | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.")
     in
     let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
@@ -1455,7 +1455,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
     let open CVars in
     let opacity =
       match terminate_ref with
-        | ConstRef c -> is_opaque_constant c
+        | GlobRef.ConstRef c -> is_opaque_constant c
         | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
     in
     let evd = Evd.from_ctx uctx in