[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.

In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.

This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.

A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.

8 files changed, 16 insertions, 15 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 319b410df..3ba3bafa4 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -885,7 +885,7 @@ let is_res r = match DAst.get r with
 | _ -> false
 
 let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> Globnames.eq_gr r gr
+| GRef (r, _) -> GlobRef.equal r gr
 | _ -> false
 
 let is_gvar c = match DAst.get c with
@@ -894,7 +894,7 @@ let is_gvar c = match DAst.get c with
 
 let same_raw_term rt1 rt2 = 
   match DAst.get rt1, DAst.get rt2 with 
-    | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2
+    | GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2
     | GHole _, GHole _ -> true
     | _ -> false
 let decompose_raw_eq lhs rhs = 
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index e331dc014..ae238b846 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -576,7 +576,7 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
              (fun _ evi _ ->
                match evi.evar_source with
                | (loc_evi,ImplicitArg(gr_evi,p_evi,b_evi)) ->
-                  if Globnames.eq_gr grk gr_evi && pk=p_evi && bk=b_evi  && rt.CAst.loc = loc_evi
+                  if GlobRef.equal grk gr_evi && pk=p_evi && bk=b_evi  && rt.CAst.loc = loc_evi
                   then raise (Found evi)
                | _ -> ()
              )
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 7088ae596..481a8be3b 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -13,7 +13,7 @@ val pattern_to_term : cases_pattern -> glob_constr
    Some basic functions to rebuild glob_constr
    In each of them the location is Util.Loc.ghost
 *)
-val mkGRef : Globnames.global_reference -> glob_constr
+val mkGRef : GlobRef.t -> glob_constr
 val mkGVar : Id.t -> glob_constr
 val mkGApp  : glob_constr*(glob_constr list) -> glob_constr
 val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 748d8add2..7df57b577 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -846,7 +846,7 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
     | _ -> [],b,t
 
 
-let make_graph (f_ref:global_reference) =
+let make_graph (f_ref : GlobRef.t) =
   let c,c_body =
     match f_ref with
     | ConstRef c ->
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index dcc1c2ea6..24304e361 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,3 +1,4 @@
+open Names
 open Misctypes
 
 val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
@@ -18,4 +19,4 @@ val functional_induction :
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 
-val make_graph :  Globnames.global_reference -> unit
+val make_graph : GlobRef.t -> unit
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 5cc7163aa..346b21ef2 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -41,7 +41,7 @@ val chop_rprod_n : int -> Glob_term.glob_constr ->
 val def_of_const : Constr.t -> Constr.t
 val eq : EConstr.constr Lazy.t
 val refl_equal : EConstr.constr Lazy.t
-val const_of_id: Id.t ->  Globnames.global_reference(* constantyes *)
+val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
 val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
 
@@ -107,11 +107,11 @@ val h_intros: Names.Id.t list -> Tacmach.tactic
 val h_id :  Names.Id.t
 val hrec_id :  Names.Id.t
 val acc_inv_id :  EConstr.constr Util.delayed
-val ltof_ref : Globnames.global_reference Util.delayed
+val ltof_ref : GlobRef.t Util.delayed
 val well_founded_ltof : EConstr.constr Util.delayed
 val acc_rel : EConstr.constr Util.delayed
 val well_founded : EConstr.constr Util.delayed
-val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
+val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_reference
 val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic
 
 val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index ad306ab25..9151fd0e2 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -10,7 +10,7 @@
 
 val invfun :
   Misctypes.quantified_hypothesis ->
-  Globnames.global_reference option ->
+  Names.GlobRef.t option ->
   Evar.t Evd.sigma -> Evar.t list Evd.sigma
 val derive_correctness :
   (Evd.evar_map ref ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e41bf71dd..2a3a85fcc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -181,7 +181,7 @@ let simpl_iter clause =
     clause
 
 (* Others ugly things ... *)
-let (value_f: Constr.t list -> global_reference -> Constr.t) =
+let (value_f: Constr.t list -> GlobRef.t -> Constr.t) =
   let open Term in
   let open Constr in
   fun al fterm ->
@@ -215,7 +215,7 @@ let (value_f: Constr.t list -> global_reference -> Constr.t) =
     let body = EConstr.Unsafe.to_constr body in
     it_mkLambda_or_LetIn body context
 
-let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) =
+let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) =
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
@@ -356,7 +356,7 @@ type 'a infos =
       f_id : Id.t;  (* function name *)
       f_constr : constr;  (* function term *)
       f_terminate : constr; (* termination proof term *)
-      func : global_reference; (* functional reference *)
+      func : GlobRef.t; (* functional reference *)
       info : 'a;
       is_main_branch : bool; (* on the main branch or on a matched expression *)
       is_final : bool; (* final first order term or not *)
@@ -1456,7 +1456,7 @@ let com_terminate
 
 
 
-let start_equation (f:global_reference) (term_f:global_reference)
+let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
   (cont_tactic:Id.t list -> tactic) g =
   let sigma = project g in
   let ids = pf_ids_of_hyps g in
@@ -1473,7 +1473,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
     observe_tac (str "prove_eq") (cont_tactic x)]) g;;
 
 let (com_eqn : int -> Id.t ->
-       global_reference -> global_reference -> global_reference
+       GlobRef.t -> GlobRef.t -> GlobRef.t
 	 -> Constr.t -> unit) =
   fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
     let open CVars in