Removing generic equality in Syntax plugin.

3 files changed, 13 insertions, 13 deletions

diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 59180be81..c3dad0a10 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -50,8 +50,8 @@ let nat_of_int dloc n =
 exception Non_closed_number
 
 let rec int_of_nat = function
-  | GApp (_,GRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
-  | GRef (_,z) when z = glob_O -> zero
+  | GApp (_,GRef (_,s),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
+  | GRef (_,z) when Globnames.eq_gr z glob_O -> zero
   | _ -> raise Non_closed_number
 
 let uninterp_nat p =
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index b8c2b33fd..8e09c974a 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -110,12 +110,12 @@ let bigint_of_int31 =
   let rec args_parsing args cur =
     match args with
       | [] -> cur
-      | (GRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur)
-      | (GRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur))
+      | (GRef (_,b))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
+      | (GRef (_,b))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
       | _ -> raise Non_closed
   in
   function
-  | GApp (_, GRef (_, c), args) when c=int31_construct -> args_parsing args zero
+  | GApp (_, GRef (_, c), args) when eq_gr c int31_construct -> args_parsing args zero
   | _ -> raise Non_closed
 
 let uninterp_int31 i =
@@ -199,14 +199,14 @@ let interp_bigN dloc n =
 let bigint_of_word =
   let rec get_height rc =
     match rc with
-    | GApp (_,GRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
+    | GApp (_,GRef(_,c), [_;lft;rght]) when eq_gr c zn2z_WW ->
       1+max (get_height lft) (get_height rght)
     | _ -> 0
   in
   let rec transform hght rc =
     match rc with
-    | GApp (_,GRef(_,c),_) when c = zn2z_W0-> zero
-    | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW->
+    | GApp (_,GRef(_,c),_) when eq_gr c zn2z_W0-> zero
+    | GApp (_,GRef(_,c), [_;lft;rght]) when eq_gr c zn2z_WW->
       let new_hght = hght-1 in
       add (mult (rank new_hght)
              (transform new_hght lft))
@@ -262,8 +262,8 @@ let interp_bigZ dloc n =
 
 (* pretty printing functions for bigZ *)
 let bigint_of_bigZ = function
-  | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
-  | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_neg ->
+  | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
+  | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigZ_neg ->
       let opp_val = bigint_of_bigN one_arg in
       if equal opp_val zero then
 	raise Non_closed
@@ -294,7 +294,7 @@ let interp_bigQ dloc n =
 
 let uninterp_bigQ rc =
   try match rc with
-    | GApp (_, GRef(_,c), [one_arg]) when c = bigQ_z ->
+    | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigQ_z ->
 	Some (bigint_of_bigZ one_arg)
     | _ -> None (* we don't pretty-print yet fractions *)
   with Non_closed -> None
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index c9767a975..54206b453 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -41,11 +41,11 @@ let uninterp_string r =
   try
     let b = Buffer.create 16 in
     let rec aux = function
-    | GApp (_,GRef (_,k),[a;s]) when k = force glob_String ->
+    | GApp (_,GRef (_,k),[a;s]) when eq_gr k (force glob_String) ->
 	(match uninterp_ascii a with
 	  | Some c -> Buffer.add_char b (Char.chr c); aux s
 	  | _ -> raise Non_closed_string)
-    | GRef (_,z) when z = force glob_EmptyString ->
+    | GRef (_,z) when eq_gr z (force glob_EmptyString) ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string