Renaming global_reference according to Coq PR #6156.

3 files changed, 15 insertions, 16 deletions

diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 1bf86b516a..d801c4f605 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -131,9 +131,9 @@ val of_constant : Constant.t -> valexpr
 val to_constant : valexpr -> Constant.t
 val constant : Constant.t repr
 
-val of_reference : Globnames.global_reference -> valexpr
-val to_reference : valexpr -> Globnames.global_reference
-val reference : Globnames.global_reference repr
+val of_reference : GlobRef.t -> valexpr
+val to_reference : valexpr -> GlobRef.t
+val reference : GlobRef.t repr
 
 val of_ext : 'a Val.tag -> 'a -> valexpr
 val to_ext : 'a Val.tag -> valexpr -> 'a
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 18533a8281..cc58144901 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -89,7 +89,7 @@ val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag
 
 val wit_ident : (Id.t, Id.t) Arg.tag
 
-val wit_reference : (Libnames.reference, Globnames.global_reference) Arg.tag
+val wit_reference : (Libnames.reference, GlobRef.t) Arg.tag
 (** Beware, at the raw level, [Qualid [id]] has not the same meaning as
     [Ident id]. The first is an unqualified global reference, the second is
     the dynamic reference to id. *)
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 631e36b5ae..026673acbf 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Tac2expr
 open EConstr
 open Genredexpr
@@ -57,16 +56,16 @@ val letin_pat_tac : evars_flag -> (bool * intro_pattern_naming) option ->
 
 val reduce : Redexpr.red_expr -> clause -> unit tactic
 
-val simpl : global_reference glob_red_flag ->
+val simpl : GlobRef.t glob_red_flag ->
   (Pattern.constr_pattern * occurrences) option -> clause -> unit tactic
 
-val cbv : global_reference glob_red_flag -> clause -> unit tactic
+val cbv : GlobRef.t glob_red_flag -> clause -> unit tactic
 
-val cbn : global_reference glob_red_flag -> clause -> unit tactic
+val cbn : GlobRef.t glob_red_flag -> clause -> unit tactic
 
-val lazy_ : global_reference glob_red_flag -> clause -> unit tactic
+val lazy_ : GlobRef.t glob_red_flag -> clause -> unit tactic
 
-val unfold : (global_reference * occurrences) list -> clause -> unit tactic
+val unfold : (GlobRef.t * occurrences) list -> clause -> unit tactic
 
 val pattern : (constr * occurrences) list -> clause -> unit tactic
 
@@ -78,16 +77,16 @@ val eval_red : constr -> constr tactic
 
 val eval_hnf : constr -> constr tactic
 
-val eval_simpl : global_reference glob_red_flag ->
+val eval_simpl : GlobRef.t glob_red_flag ->
   (Pattern.constr_pattern * occurrences) option -> constr -> constr tactic
 
-val eval_cbv : global_reference glob_red_flag -> constr -> constr tactic
+val eval_cbv : GlobRef.t glob_red_flag -> constr -> constr tactic
 
-val eval_cbn : global_reference glob_red_flag -> constr -> constr tactic
+val eval_cbn : GlobRef.t glob_red_flag -> constr -> constr tactic
 
-val eval_lazy : global_reference glob_red_flag -> constr -> constr tactic
+val eval_lazy : GlobRef.t glob_red_flag -> constr -> constr tactic
 
-val eval_unfold : (global_reference * occurrences) list -> constr -> constr tactic
+val eval_unfold : (GlobRef.t * occurrences) list -> constr -> constr tactic
 
 val eval_fold : constr list -> constr -> constr tactic
 
@@ -122,4 +121,4 @@ val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option ->
 
 val contradiction : constr_with_bindings option -> unit tactic
 
-val firstorder : unit thunk option -> global_reference list -> Id.t list -> unit tactic
+val firstorder : unit thunk option -> GlobRef.t list -> Id.t list -> unit tactic