Removing a bunch of generic equalities.

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

2 files changed, 36 insertions, 36 deletions

diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index e31eba4e0..286fa6335 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -136,7 +136,7 @@ type term =
 
 let const n =
   if eq_num n num_0 then Zero else Const n
-let pow(p,i) = if i=1 then p else Pow(p,i)
+let pow(p,i) = if Int.equal i 1 then p else Pow(p,i)
 let add = function
     (Zero,q) -> q
   | (p,Zero) -> p
@@ -192,7 +192,7 @@ let rec mkt_pos n =
     mkt_app pxI [mkt_pos (quo_num n num_2)]
 
 let mkt_n n =
-  if n=num_0
+  if Num.eq_num n num_0
   then Lazy.force nN0
   else mkt_app nNpos [mkt_pos n]
 
@@ -212,7 +212,7 @@ let rec mkt_term t  =  match t with
 | Add (t1,t2) -> mkt_app  ttadd [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Sub (t1,t2) -> mkt_app  ttsub [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Mul (t1,t2) -> mkt_app  ttmul [Lazy.force tz; mkt_term t1; mkt_term t2]
-| Pow (t1,n) ->  if (n = 0) then
+| Pow (t1,n) ->  if Int.equal n 0 then
     mkt_app ttconst [Lazy.force tz; mkt_z num_1]
 else
     mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)]
@@ -311,7 +311,7 @@ let term_pol_sparse np t=
     match t with
     | Zero -> zeroP
     | Const r ->
-	if r = num_0
+	if Num.eq_num r num_0
 	then zeroP
 	else polconst d (Poly.Pint (Coef.of_num r))
     | Var v ->
@@ -365,19 +365,19 @@ let pol_sparse_to_term n2 p =
 		if m.(k)>0
 		then i0:=k
 	      done;
-	      if !i0 = 0
+	      if Int.equal !i0 0
 	      then (r,d)
 	      else if !i0 > r
 	      then (!i0, m.(!i0))
-	      else if !i0 = r && m.(!i0)<d
+	      else if Int.equal !i0 r && m.(!i0)<d
 	      then (!i0, m.(!i0))
 	      else (r,d))
 	  (0,0)
 	  p in
-      if i0=0
+      if Int.equal i0 0
       then
 	let mp = ref (polrec_to_term a) in
-        if p1=[]
+        if List.is_empty p1
 	then !mp
 	else add(!mp,aux p1)
       else (
@@ -391,7 +391,7 @@ let pol_sparse_to_term n2 p =
 	     else p2:=(a,m)::(!p2))
 	  p;
 	let vm =
-	  if e0=1
+	  if Int.equal e0 1
 	  then Var (string_of_int (i0))
 	  else pow (Var (string_of_int (i0)),e0) in
 	add(mul(vm, aux (List.rev (!p1))), aux (List.rev (!p2))))
@@ -401,11 +401,11 @@ let pol_sparse_to_term n2 p =
 
 let remove_list_tail l i =
   let rec aux l i =
-    if l=[]
+    if List.is_empty l
     then []
     else if i<0
     then l
-    else if i=0
+    else if Int.equal i 0
     then List.tl l
     else
       match l with
@@ -523,7 +523,7 @@ let theoremedeszeros_termes lp =
 	  let (cert,lp0,p,_lct) = theoremedeszeros lpol p in
           info "cert ok\n";
 	  let lc = cert.last_comb::List.rev cert.gb_comb in
-	  match remove_zeros (fun x -> x=zeroP) lc with
+	  match remove_zeros (fun x -> equal x zeroP) lc with
 	  | [] -> assert false
 	  | (lq::lci) ->
 	      (* lci commence par les nouveaux polynomes *)
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index ca6d305e8..78883a660 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -168,7 +168,7 @@ exception Failed
 let rec equal p q =
   match (p,q) with
       (Pint a,Pint b) -> C.equal a b
-    |(Prec(x,p1),Prec(y,q1)) -> (x=y) && Array.for_all2 equal p1 q1
+    |(Prec(x,p1),Prec(y,q1)) -> (Int.equal x y) && Array.for_all2 equal p1 q1
     | (_,_) -> false
 
 (* normalize polynomial: remove head zeros, coefficients are normalized
@@ -184,8 +184,8 @@ let norm p = match p with
 	 n:=!n-1;
        done;
        if !n<0 then Pint coef0
-       else if !n=0 then a.(0)
-       else if !n=d then p
+       else if Int.equal !n 0 then a.(0)
+       else if Int.equal !n d then p
        else (let b=Array.make (!n+1) (Pint coef0) in
                for i=0 to !n do b.(i)<-a.(i);done;
                Prec(x,b))
@@ -194,7 +194,7 @@ let norm p = match p with
 (* degree in v, v >= max var of p *)
 let deg v p =
   match p with
-      Prec(x,p1) when x=v -> Array.length p1 -1
+      Prec(x,p1) when Int.equal x v -> Array.length p1 -1
     |_ -> 0
 
 
@@ -214,8 +214,8 @@ let rec copyP p =
 (* coefficient of degree i in v, v >= max var of p *)
 let coef v i p =
   match p with
-      Prec (x,p1) when x=v  -> if i<(Array.length p1) then p1.(i) else Pint coef0
-    |_ -> if i=0 then p else Pint coef0
+      Prec (x,p1) when Int.equal x v  -> if i<(Array.length p1) then p1.(i) else Pint coef0
+    |_ -> if Int.equal i 0 then p else Pint coef0
 
 (* addition *)
 
@@ -272,7 +272,7 @@ let rec vars=function
 (* multiply p by v^n, v >= max_var p *)
 let multx n v p =
   match p with
-      Prec (x,p1) when x=v -> let p2= Array.make ((Array.length p1)+n) (Pint coef0) in
+      Prec (x,p1) when Int.equal x v -> let p2= Array.make ((Array.length p1)+n) (Pint coef0) in
         for i=0 to (Array.length p1)-1 do
           p2.(i+n)<-p1.(i);
         done;
@@ -311,9 +311,9 @@ let rec multP p q =
 let deriv v p =
   match p with
       Pint a -> Pint coef0
-    | Prec(x,p1) when x=v ->
+    | Prec(x,p1) when Int.equal x v ->
        let d = Array.length p1 -1 in
-         if d=1 then p1.(1)
+         if Int.equal d 1 then p1.(1)
          else
            (let p2 = Array.make d (Pint coef0) in
               for i=0 to d-1 do
@@ -410,7 +410,7 @@ let rec string_of_Pcut p =
       and s=ref ""
       and sp=ref "" in
     let st0 = string_of_Pcut t.(0) in
-      if st0<>"0"
+      if not (String.equal st0 "0")
       then s:=st0;
     let fin = ref false in
     for i=(Array.length t)-1 downto 1 do
@@ -421,31 +421,31 @@ let rec string_of_Pcut p =
       else (
 	let si=string_of_Pcut  t.(i) in
 	sp:="";
-	if i=1
+	if Int.equal i 1
 	then (
-	  if si<>"0"
+	  if not (String.equal si "0")
 	  then (nsP:=(!nsP)-1;
-		if si="1"
+		if String.equal si "1"
 		then sp:=v
 		else
 		  (if (String.contains si '+')
 		  then sp:="("^si^")*"^v
 		  else sp:=si^"*"^v)))
 	else (
-	  if si<>"0"
+	  if not (String.equal si "0")
 	  then (nsP:=(!nsP)-1;
-		if si="1"
+		if String.equal si "1"
 		then sp:=v^"^"^(string_of_int i)
 		else (if (String.contains si '+')
 		then sp:="("^si^")*"^v^"^"^(string_of_int i)
 		else  sp:=si^"*"^v^"^"^(string_of_int i))));
-	if !sp<>"" && not (!fin)
+	if not (String.is_empty !sp) && not (!fin)
 	then (nsP:=(!nsP)-1;
-	      if !s=""
+	      if String.is_empty !s
 	      then s:=!sp
 	      else s:=(!s)^"+"^(!sp)));
     done;
-    if !s="" then (nsP:=(!nsP)-1;
+    if String.is_empty !s then (nsP:=(!nsP)-1;
 		   (s:="0"));
     !s
 
@@ -468,7 +468,7 @@ let print_lpoly lp = print_tpoly (Array.of_list lp)
 
 (* return (s,r) s.t. p = s*q+r *)
 let rec quo_rem_pol p q x =
-  if x=0
+  if Int.equal x 0
   then (match (p,q) with
           |(Pint a, Pint b) ->
 	     if C.equal (C.modulo a b) coef0
@@ -532,7 +532,7 @@ let div_pol_rat p q=
 let pseudo_div p q x =
   match q with
       Pint _ -> (cf0, q,1, p)
-    | Prec (v,q1) when x<>v -> (cf0, q,1, p)
+    | Prec (v,q1) when not (Int.equal x v) -> (cf0, q,1, p)
     | Prec (v,q1) ->
 	(
 	  (*  pr "pseudo_division: c^d*p = s*q + r";*)
@@ -569,13 +569,13 @@ and pgcd_pol p q x =
 
 and content_pol p x =
   match p with
-      Prec(v,p1) when v=x ->
+      Prec(v,p1) when Int.equal v x ->
         Array.fold_left (fun a b -> pgcd_pol_rec a b (x-1)) cf0 p1
     | _ -> p
 
 and pgcd_coef_pol c p x =
   match p with
-      Prec(v,p1) when x=v ->
+      Prec(v,p1) when Int.equal x v ->
         Array.fold_left (fun a b -> pgcd_pol_rec a b (x-1)) c  p1
     |_ -> pgcd_pol_rec c p (x-1)
 
@@ -587,9 +587,9 @@ and pgcd_pol_rec p q x =
 	  then q
 	  else if equal q cf0
 	  then p
-	  else if (deg x q) = 0
+	  else if Int.equal (deg x q) 0
 	  then pgcd_coef_pol q p x
-	  else if (deg x p) = 0
+	  else if Int.equal (deg x p) 0
 	  then pgcd_coef_pol p q x
 	  else (
 	    let a = content_pol p x in