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_ops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index a76f820941..6a282624e4 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -28,7 +28,7 @@ open Notation_term
 let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
 
 let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
-| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
 | NVar id1, NVar id2 -> (
    match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
    | Some n,Some m -> Int.equal n m
@@ -1123,7 +1123,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
 
   (* Matching compositionally *)
   | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
-  | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
+  | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma
   | GApp (f1,l1), NApp (f2,l2) ->
       let n1 = List.length l1 and n2 = List.length l2 in
       let f1,l1,f2,l2 =
-- 
cgit v1.2.3