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.
---
 plugins/syntax/z_syntax.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/syntax/z_syntax.ml')

diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index d5300e474c..09fe8bf70a 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -71,13 +71,13 @@ let interp_positive ?loc n =
 (**********************************************************************)
 
 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 rec bignat_of_pos x = DAst.with_val (function
   | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
   | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (a, _)                when Globnames.eq_gr a glob_xH -> Bigint.one
+  | GRef (a, _)                when GlobRef.equal a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
   ) x
 
@@ -132,7 +132,7 @@ let n_of_int ?loc n =
 
 let bignat_of_n n = DAst.with_val (function
   | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a
-  | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
+  | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
   ) n
 
@@ -180,7 +180,7 @@ let z_of_int ?loc n =
 let bigint_of_z z = DAst.with_val (function
   | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a
   | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
   ) z
 
-- 
cgit v1.2.3