[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, 34 insertions, 35 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 047fc9fbf..a60a966ce 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -211,7 +211,7 @@ type left_pattern=
   | Lexists of pinductive
   | LA of constr*left_arrow_pattern
 
-type t={id:global_reference;
+type t={id:GlobRef.t;
 	constr:constr;
 	pat:(left_pattern,right_pattern) sum;
 	atoms:atoms}
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 2962d9230..e2c6f1c4b 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -8,9 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Names
 open Constr
 open EConstr
-open Globnames
 
 val qflag : bool ref
 
@@ -35,7 +35,7 @@ type atoms = {positive:constr list;negative:constr list}
 
 type side = Hyp | Concl | Hint
 
-val dummy_id: global_reference
+val dummy_id: GlobRef.t
 
 val build_atoms : Environ.env -> Evd.evar_map -> counter ->
   side -> constr -> bool * atoms
@@ -65,13 +65,13 @@ type left_pattern=
   | Lexists of pinductive
   | LA of constr*left_arrow_pattern
 
-type t={id: global_reference;
+type t={id: GlobRef.t;
 	constr: constr;
 	pat: (left_pattern,right_pattern) sum;
 	atoms: atoms}
 
 (*exception Is_atom of constr*)
 
-val build_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> types ->
+val build_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> types ->
   counter -> (t,types) sum
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index e8c0b927d..22a3e1f67 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -43,7 +43,7 @@ let compare_gr id1 id2 =
 
 module OrderedInstance=
 struct
-  type t=instance * Globnames.global_reference
+  type t=instance * GlobRef.t
   let compare (inst1,id1) (inst2,id2)=
     (compare_instance =? compare_gr) inst2 inst1 id2 id1
     (* we want a __decreasing__ total order *)
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 61786ffdc..9f9ade3aa 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -8,13 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Globnames
+open Names
 open Rules
 
 val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t
 
 val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t ->
-  (Unify.instance * global_reference) list
+  (Unify.instance * GlobRef.t) list
 
 val quantified_tac : Formula.t list -> seqtac with_backtracking
 
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index cfcd65619..2d7a3e37b 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -29,7 +29,7 @@ type tactic = unit Proofview.tactic
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
-type lseqtac= global_reference -> seqtac
+type lseqtac= GlobRef.t -> seqtac
 
 type 'a with_backtracking = tactic -> 'a
 
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 859388b30..924c26790 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -11,21 +11,20 @@
 open Names
 open Constr
 open EConstr
-open Globnames
 
 type tactic = unit Proofview.tactic
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
-type lseqtac= global_reference -> seqtac
+type lseqtac= GlobRef.t -> seqtac
 
 type 'a with_backtracking = tactic -> 'a
 
 val wrap : int -> bool -> seqtac
 
-val basename_of_global: global_reference -> Id.t
+val basename_of_global: GlobRef.t -> Id.t
 
-val clear_global: global_reference -> tactic
+val clear_global: GlobRef.t -> tactic
 
 val axiom_tac : constr -> Sequent.t -> tactic
 
@@ -41,7 +40,7 @@ val left_and_tac : pinductive -> lseqtac with_backtracking
 
 val left_or_tac : pinductive -> lseqtac with_backtracking
 
-val left_false_tac : global_reference -> tactic
+val left_false_tac : GlobRef.t -> tactic
 
 val ll_ind_tac : pinductive -> constr list -> lseqtac with_backtracking
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7c612c0d8..0c752d4a4 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -8,13 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open EConstr
-open CErrors
 open Util
+open Pp
+open CErrors
+open Names
+open EConstr
 open Formula
 open Unify
-open Globnames
-open Pp
 
 let newcnt ()=
   let cnt=ref (-1) in
@@ -56,7 +56,7 @@ struct
 	(priority e1.pat) - (priority e2.pat)
 end
 
-type h_item = global_reference * (int*Constr.t) option
+type h_item = GlobRef.t * (int*Constr.t) option
 
 module Hitem=
 struct
@@ -87,7 +87,7 @@ let cm_remove sigma typ nam cm=
   let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   try
     let l=CM.find typ cm in
-    let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
+    let l0=List.filter (fun id-> not (GlobRef.equal id nam)) l in
       match l0 with
 	  []->CM.remove typ cm
 	| _ ->CM.add typ l0 cm
@@ -97,7 +97,7 @@ module HP=Heap.Functional(OrderedFormula)
 
 type t=
     {redexes:HP.t;
-     context:(global_reference list) CM.t;
+     context:(GlobRef.t list) CM.t;
      latoms:constr list;
      gl:types;
      glatom:constr option;
@@ -117,7 +117,7 @@ let lookup sigma item seq=
 	let p (id2,o)=
 	  match o with
 	      None -> false
-	    | Some (m2, t2)-> Globnames.eq_gr id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
+            | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
 	  History.exists p seq.history
 
 let add_formula env sigma side nam t seq =
@@ -187,9 +187,9 @@ let empty_seq depth=
 
 let expand_constructor_hints =
   List.map_append (function
-    | IndRef ind ->
+    | GlobRef.IndRef ind ->
         List.init (Inductiveops.nconstructors ind)
-          (fun i -> ConstructRef (ind,i+1))
+          (fun i -> GlobRef.ConstructRef (ind,i+1))
     | gr ->
 	[gr])
 
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index c4ed3e21f..709b278ec 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -8,26 +8,26 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Names
 open EConstr
 open Formula
-open Globnames
 
 module CM: CSig.MapS with type key=Constr.t
 
-type h_item = global_reference * (int*Constr.t) option
+type h_item = GlobRef.t * (int*Constr.t) option
 
 module History: Set.S with type elt = h_item
 
-val cm_add : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t ->
-  global_reference list CM.t
+val cm_add : Evd.evar_map -> constr -> GlobRef.t -> GlobRef.t list CM.t ->
+  GlobRef.t list CM.t
 
-val cm_remove : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t ->
-  global_reference list CM.t
+val cm_remove : Evd.evar_map -> constr -> GlobRef.t -> GlobRef.t list CM.t ->
+  GlobRef.t list CM.t
 
 module HP: Heap.S with type elt=Formula.t
 
 type t = {redexes:HP.t;
-	  context: global_reference list CM.t;
+          context: GlobRef.t list CM.t;
 	  latoms:constr list;
 	  gl:types;
 	  glatom:constr option;
@@ -41,20 +41,20 @@ val record: h_item -> t -> t
 
 val lookup: Evd.evar_map -> h_item -> t -> bool
 
-val add_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> constr -> t -> t
+val add_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> constr -> t -> t
 
 val re_add_formula_list : Evd.evar_map -> Formula.t list -> t -> t
 
-val find_left : Evd.evar_map -> constr -> t -> global_reference
+val find_left : Evd.evar_map -> constr -> t -> GlobRef.t
 
 val take_formula : Evd.evar_map -> t -> Formula.t * t
 
 val empty_seq : int -> t
 
-val extend_with_ref_list : Environ.env -> Evd.evar_map -> global_reference list ->
+val extend_with_ref_list : Environ.env -> Evd.evar_map -> GlobRef.t list ->
   t -> t * Evd.evar_map
 
 val extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list ->
   t -> t * Evd.evar_map
 
-val print_cmap: global_reference list CM.t -> Pp.t
+val print_cmap: GlobRef.t list CM.t -> Pp.t