From afceace455a4b37ced7e29175ca3424996195f7b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 14 Nov 2017 22:36:47 +0100
Subject: [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.
---
 interp/notation.mli | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 6803a7e517..eac87414f3 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -11,7 +11,6 @@
 open Bigint
 open Names
 open Libnames
-open Globnames
 open Constrexpr
 open Glob_term
 open Notation_term
@@ -91,7 +90,7 @@ val declare_string_interpreter : scope_name -> required_module ->
 val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes ->
   glob_constr * (notation_location * scope_name option)
 (* This function returns a glob_const representing a pattern *)
-val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> unit) -> prim_token ->
+val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> prim_token ->
   local_scopes -> glob_constr * (notation_location * scope_name option)
 
 (** Return the primitive token associated to a [term]/[cases_pattern];
@@ -143,8 +142,8 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *)
 
 (** {6 Miscellaneous} *)
 
-val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> bool) ->
-      notation -> delimiters option -> global_reference
+val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
+      notation -> delimiters option -> GlobRef.t
 
 (** Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
@@ -152,9 +151,9 @@ val exists_notation_in_scope : scope_name option -> notation ->
 
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
-  bool (** true=local *) -> global_reference -> scope_name option list -> unit
+  bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit
 
-val find_arguments_scope : global_reference -> scope_name option list
+val find_arguments_scope : GlobRef.t -> scope_name option list
 
 type scope_class
 
@@ -165,7 +164,7 @@ val subst_scope_class :
   Mod_subst.substitution -> scope_class -> scope_class option
 
 val declare_scope_class : scope_name -> scope_class -> unit
-val declare_ref_arguments_scope : Evd.evar_map -> global_reference -> unit
+val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit
 
 val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list
 val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
-- 
cgit v1.2.3