Removing a bunch of generic equalities.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 31 insertions, 31 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 180d15009..790e1970b 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -35,17 +35,17 @@ open Lazy
 
 let interp_ascii dloc p =
   let rec aux n p =
-     if n = 0 then [] else
+     if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     GRef (dloc,if mp = 0 then glob_false else glob_true)
+     GRef (dloc,if Int.equal mp 0 then glob_false else glob_true)
      :: (aux (n-1) (p/2)) in
   GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p)
 
 let interp_ascii_string dloc s =
   let p =
-    if String.length s = 1 then int_of_char s.[0]
+    if Int.equal (String.length s) 1 then int_of_char s.[0]
     else
-      if String.length s = 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
+      if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
       then int_of_string s
       else
 	user_err_loc (dloc,"interp_ascii_string",
@@ -54,13 +54,13 @@ let interp_ascii_string dloc s =
 
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
-    | [] when n = 0 -> 0
-    | GRef (_,k)::l when k = glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | GRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
+    | [] when Int.equal n 0 -> 0
+    | GRef (_,k)::l when Globnames.eq_gr k glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | GRef (_,k)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
   try
     let aux = function
-    | GApp (_,GRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
+    | GApp (_,GRef (_,k),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
   with
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index efbd140ee..545f205db 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -55,7 +55,7 @@ let r_of_posint dloc n =
       let (q,r) = div2_with_rest n in
       let b = GApp(dloc,GRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
       if r then GApp(dloc,GRef(dloc,glob_Rplus),[r1;b]) else b in
-  if n <> zero then r_of_pos n else GRef(dloc,glob_R0)
+  if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0)
 
 let r_of_int dloc z =
   if is_strictly_neg z then
@@ -72,34 +72,34 @@ let bignat_of_r =
 let rec bignat_of_pos = function
   (* 1+1 *)
   | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)])
-      when p = glob_Rplus && o1 = glob_R1 && o2 = glob_R1 -> two
+      when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two
   (* 1+(1+1) *)
   | GApp (_,GRef (_,p1), [GRef (_,o1);
       GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])])
-      when p1 = glob_Rplus && p2 = glob_Rplus &&
-           o1 = glob_R1 && o2 = glob_R1 && o3 = glob_R1 -> three
+      when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus &&
+           Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three
   (* (1+1)*b *)
-  | GApp (_,GRef (_,p), [a; b]) when p = glob_Rmult ->
-      if bignat_of_pos a <> two then raise Non_closed_number;
+  | GApp (_,GRef (_,p), [a; b]) when Globnames.eq_gr p glob_Rmult ->
+      if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number;
       mult_2 (bignat_of_pos b)
   (* 1+(1+1)*b *)
   | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])])
-      when p1 = glob_Rplus && p2 = glob_Rmult && o = glob_R1  ->
-      if bignat_of_pos a <> two then raise Non_closed_number;
+      when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1  ->
+      if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number;
         add_1 (mult_2 (bignat_of_pos b))
   | _ -> raise Non_closed_number
 in
 let bignat_of_r = function
-  | GRef (_,a) when a = glob_R0 -> zero
-  | GRef (_,a) when a = glob_R1 -> one
+  | GRef (_,a) when Globnames.eq_gr a glob_R0 -> zero
+  | GRef (_,a) when Globnames.eq_gr a glob_R1 -> one
   | r -> bignat_of_pos r
 in
 bignat_of_r
 
 let bigint_of_r = function
-  | GApp (_,GRef (_,o), [a]) when o = glob_Ropp ->
+  | GApp (_,GRef (_,o), [a]) when Globnames.eq_gr o glob_Ropp ->
       let n = bignat_of_r a in
-      if n = zero then raise Non_closed_number;
+      if Bigint.equal n zero then raise Non_closed_number;
       neg n
   | a -> bignat_of_r a
 
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index e5e4e9331..67e54c017 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -47,7 +47,7 @@ let pos_of_bignat dloc x =
   let rec pos_of x =
     match div2_with_rest x with
       | (q,false) -> GApp (dloc, ref_xO,[pos_of q])
-      | (q,true) when q <> zero -> GApp (dloc,ref_xI,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -65,9 +65,9 @@ let interp_positive dloc n =
 (**********************************************************************)
 
 let rec bignat_of_pos = function
-  | GApp (_, GRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
-  | GApp (_, GRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (_, a) when a = glob_xH -> Bigint.one
+  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | GRef (_, a) when Globnames.eq_gr a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
 
 let uninterp_positive p =
@@ -103,7 +103,7 @@ let glob_Npos = ConstructRef path_of_Npos
 let n_path = make_path binnums "N"
 
 let n_of_binnat dloc pos_or_neg n =
-  if n <> zero then
+  if not (Bigint.equal n zero) then
     GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n])
   else
     GRef (dloc, glob_N0)
@@ -120,8 +120,8 @@ let n_of_int dloc n =
 (**********************************************************************)
 
 let bignat_of_n = function
-  | GApp (_, GRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
-  | GRef (_, a) when a = glob_N0 -> Bigint.zero
+  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
+  | GRef (_, a) when Globnames.eq_gr a glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_n p =
@@ -154,7 +154,7 @@ let glob_POS = ConstructRef path_of_POS
 let glob_NEG = ConstructRef path_of_NEG
 
 let z_of_int dloc n =
-  if n <> zero then
+  if not (Bigint.equal n zero) then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
     GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n])
@@ -166,9 +166,9 @@ let z_of_int dloc n =
 (**********************************************************************)
 
 let bigint_of_z = function
-  | GApp (_, GRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a
-  | GApp (_, GRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (_, a) when a = glob_ZERO -> Bigint.zero
+  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | GRef (_, a) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_z p =