Fixing some generic equalities in Micromega.

6 files changed, 77 insertions, 80 deletions

diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 4f9129396..c81d141f6 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -76,7 +76,7 @@ let dev_form n_spec  p =
       let p = dev_form p in
       let n = C2Ml.n n in
       let rec pow n = 
-       if n = 0 
+       if Int.equal n 0 
        then Poly.constant (n_spec.number_to_num n_spec.unit)
        else Poly.product p (pow (n-1)) in
        pow n in
@@ -87,8 +87,8 @@ let monomial_to_polynomial mn =
  Monomial.fold 
   (fun v i acc -> 
      let v = Ml2C.positive v in
-     let mn = if i = 1 then Mc.PEX v else Mc.PEpow (Mc.PEX v ,Ml2C.n i) in
-       if acc = Mc.PEc (Mc.Zpos Mc.XH)
+     let mn = if Int.equal i 1 then Mc.PEX v else Mc.PEpow (Mc.PEX v ,Ml2C.n i) in
+       if Pervasives.(=) acc (Mc.PEc (Mc.Zpos Mc.XH)) (** FIXME *)
        then mn 
        else Mc.PEmul(mn,acc))
    mn 
@@ -105,10 +105,10 @@ let list_to_polynomial vars l =
   | c::l -> if c =/  (Int 0) then xtopoly p (i+1) l 
     else let c = Mc.PEc (Ml2C.bigint (numerator c)) in
     let mn = 
-     if c =  Mc.PEc (Mc.Zpos Mc.XH)
+     if Pervasives.(=) c (Mc.PEc (Mc.Zpos Mc.XH))
      then var i
      else Mc.PEmul (c,var i) in
-    let p' = if p = Mc.PEc Mc.Z0 then mn else
+    let p' = if Pervasives.(=) p (Mc.PEc Mc.Z0) then mn else
       Mc.PEadd (mn, p) in
      xtopoly p' (i+1) l in
   
@@ -116,7 +116,7 @@ let list_to_polynomial vars l =
 
 let rec fixpoint f x =
  let y' = f x in
-  if y' = x then y'
+  if Pervasives.(=) y' x then y'
   else fixpoint f y'
 
 let  rec_simpl_cone n_spec e = 
@@ -153,9 +153,9 @@ let factorise_linear_cone c =
  let factorise c1 c2 =
   match c1 , c2 with
    | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') -> 
-      if x = x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None
+      if Pervasives.(=) x x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None
    | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') -> 
-      if x = x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None
+      if Pervasives.(=) x x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None
    |  _     -> None in
   
  let rec rebuild_cone l pending  =
@@ -199,7 +199,7 @@ open Mfourier
 
 let constrain_monomial mn l  = 
  let coeffs = List.fold_left (fun acc p -> (Poly.get mn p)::acc) [] l in
-  if mn = Monomial.const
+  if Pervasives.(=) mn Monomial.const
   then  
    { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ; 
      op = Eq ; 
@@ -305,11 +305,11 @@ let primal l =
 
   let vect_of_poly map p =
     Poly.fold (fun mn vl (map,vect) -> 
-      if mn = Monomial.const 
+      if Pervasives.(=) mn Monomial.const 
       then (map,vect)
       else 
 	let (mn,m) = try (MonMap.find mn map,map) with Not_found -> let res = (!vr, MonMap.add mn !vr map) in incr vr ; res in
-	  (m,if sign_num vl = 0 then vect else (mn,vl)::vect)) p (map,[]) in
+	  (m,if Int.equal (sign_num vl) 0 then vect else (mn,vl)::vect)) p (map,[]) in
     
   let op_op = function Mc.NonStrict -> Ge |Mc.Equal -> Eq | _ -> raise Strict in
 
@@ -367,7 +367,7 @@ let linear_prover n_spec l  =
   let build_system n_spec l = 
     let li = List.combine l (interval 0 (List.length l -1)) in
     let (l1,l') = List.partition 
-      (fun (x,_) -> if snd x = Mc.NonEqual then true else false) li in
+      (fun (x,_) -> if Pervasives.(=) (snd x) Mc.NonEqual then true else false) li in
       List.map 
 	(fun ((x,y),i) -> match y with
              Mc.NonEqual -> failwith "cannot happen"
@@ -394,7 +394,7 @@ let make_linear_system l =
  let monomials = List.fold_left (fun acc p -> Poly.addition p acc) 
   (Poly.constant (Int 0)) l' in
  let monomials = Poly.fold 
-  (fun mn _ l -> if mn = Monomial.const then l else mn::l) monomials [] in
+  (fun mn _ l -> if Pervasives.(=) mn Monomial.const then l else mn::l) monomials [] in
   (List.map (fun (c,op) -> 
    {coeffs = Vect.from_list (List.map (fun mn ->  (Poly.get mn c)) monomials) ; 
     op = op ; 
@@ -415,7 +415,7 @@ let rec remove_assoc p x l =
  match l with [] -> [] | e::l -> if p x (fst e) then
   remove_assoc p x l else e::(remove_assoc p x l) 
 
-let eq x y = Vect.compare x y = 0
+let eq x y = Int.equal (Vect.compare x y) 0
 
 let  remove e  l  = List.fold_left (fun l x -> if eq x e then l else x::l) [] l
 
@@ -475,7 +475,7 @@ let rec scale_term t =
     let s1' = div_big_int s1 g in
     let s2' = div_big_int s2 g in
     let e = mult_big_int g (mult_big_int s1' s2') in
-     if (compare_big_int e unit_big_int) = 0
+     if Int.equal (compare_big_int e unit_big_int) 0
      then (unit_big_int, Add (y1,y2))
      else 	e, Add (Mul(Const (Big_int s2'), y1),
 		       Mul (Const (Big_int s1'), y2))
@@ -497,7 +497,7 @@ let get_index_of_ith_match f i l  =
    | [] -> failwith "bad index"
    | e::l -> if f e
      then 
-       (if j = i then res else get (j+1) (res+1) l )
+       (if Int.equal j i then res else get (j+1) (res+1) l )
      else get j (res+1) l in
   get 0 0 l
 
@@ -557,7 +557,7 @@ let  q_cert_of_pos  pos =
   | Axiom_lt i ->  Mc.PsatzIn (Ml2C.nat i)
   | Monoid l  -> product l
   | Rational_eq n | Rational_le n | Rational_lt n -> 
-     if compare_num n (Int 0) = 0 then Mc.PsatzZ else
+     if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ else
       Mc.PsatzC (Ml2C.q   n)
   | Square t -> Mc.PsatzSquare (term_to_q_pol  t)
   | Eqmul (t, y) -> Mc.PsatzMulC(term_to_q_pol t, _cert_of_pos y)
@@ -588,7 +588,7 @@ let  z_cert_of_pos  pos =
   | Axiom_lt i ->  Mc.PsatzIn (Ml2C.nat i)
   | Monoid l  -> product l
   | Rational_eq n | Rational_le n | Rational_lt n -> 
-     if compare_num n (Int 0) = 0 then Mc.PsatzZ else
+     if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ else
       Mc.PsatzC (Ml2C.bigint (big_int_of_num  n))
   | Square t -> Mc.PsatzSquare (term_to_z_pol  t)
   | Eqmul (t, y) -> 
@@ -629,7 +629,7 @@ struct
     let rec xid_of_hyp i l = 
       match l with
       | [] -> failwith "id_of_hyp"
-      | hyp'::l -> if hyp = hyp' then i else xid_of_hyp (i+1) l in
+      | hyp'::l -> if Pervasives.(=) hyp hyp' then i else xid_of_hyp (i+1) l in
       xid_of_hyp 0 l
 
 end
@@ -755,7 +755,7 @@ let check_sat (cstr,prf) =
 	  if eq_num gcd (Int 1)
 	  then Normalise(cstr,prf) 
 	  else
-	    if sign_num (mod_num cst gcd) = 0
+	    if Int.equal (sign_num (mod_num cst gcd)) 0
 	    then (* We can really normalise *)
 	      begin
 		assert (sign_num gcd >=1 ) ;
@@ -795,18 +795,18 @@ let pivot v (c1,p1) (c2,p2) =
     match Vect.get v v1 , Vect.get v v2 with
     | None , _ | _ , None -> None
     | Some a   , Some b   ->
-	if (sign_num a) * (sign_num b) = -1
+	if Int.equal ((sign_num a) * (sign_num b)) (-1)
 	then 
 	  let cv1 = abs_num b 
 	  and cv2 = abs_num a  in
 	    Some (xpivot cv1 cv2)
 	else 
-	  if op1 = Eq
+	  if op1 == Eq
           then 
 	    let cv1 = minus_num (b */ (Int (sign_num a)))
 	    and cv2 = abs_num a in
 	      Some (xpivot cv1 cv2)
-          else if op2 = Eq
+          else if op2 == Eq
 	  then
 	    let cv1 = abs_num b 
 	    and cv2 = minus_num (a */ (Int  (sign_num b))) in
@@ -829,7 +829,7 @@ let simpl_sys sys =
     Source: http://en.wikipedia.org/wiki/Extended_Euclidean_algorithm
 *)
 let rec ext_gcd a b = 
-  if sign_big_int b = 0 
+  if Int.equal (sign_big_int b) 0 
   then (unit_big_int,zero_big_int)
   else
     let (q,r) = quomod_big_int a b in
@@ -850,7 +850,7 @@ let pp_ext_gcd a b =
 exception Result of (int * (proof * cstr_compat))
 
 let split_equations psys = 
-  List.partition (fun (c,p) -> c.op = Eq)
+  List.partition (fun (c,p) -> c.op == Eq)
 
 
 let extract_coprime (c1,p1) (c2,p2) = 
@@ -858,9 +858,9 @@ let extract_coprime (c1,p1) (c2,p2) =
     match vect1 , vect2 with
     | _ , [] | [], _ -> None
     | (v1,n1)::vect1' , (v2, n2) :: vect2' -> 
-	if v1 = v2
+	if Pervasives.(=) v1 v2
 	then 
-	  if compare_big_int (gcd_big_int (numerator n1) (numerator n2)) unit_big_int  = 0
+	  if Int.equal (compare_big_int (gcd_big_int (numerator n1) (numerator n2)) unit_big_int) 0
 	  then Some (v1,n1,n2)
 	  else 
 	    exist2 vect1' vect2'
@@ -869,7 +869,7 @@ let extract_coprime (c1,p1) (c2,p2) =
 	  then exist2 vect1' vect2
 	  else exist2 vect1 vect2' in
     
-    if c1.op = Eq && c2.op = Eq 
+    if c1.op == Eq && c2.op == Eq 
     then exist2 c1.coeffs c2.coeffs
     else None
 
@@ -926,7 +926,7 @@ let reduce_coprime psys =
 (** If there is an equation [eq] of the form 1.x + e = c, do a pivot over x with equation [eq] *)
 let reduce_unary psys = 
   let is_unary_equation (cstr,prf) = 
-    if cstr.op = Eq 
+    if cstr.op == Eq 
     then 
       try 
 	Some (fst (List.find (fun (_,n) -> n =/ (Int 1) || n=/ (Int (-1))) cstr.coeffs))
@@ -942,12 +942,12 @@ let reduce_unary psys =
 let reduce_non_lin_unary psys = 
 
   let is_unary_equation (cstr,prf) = 
-    if cstr.op = Eq 
+    if cstr.op == Eq 
     then 
       try 
 	let x = fst (List.find (fun (x,n) ->  (n =/ (Int 1) || n=/ (Int (-1))) && Monomial.is_var (LinPoly.MonT.retrieve x) ) cstr.coeffs) in
 	let x' = LinPoly.MonT.retrieve x in
-	  if List.for_all (fun (y,_) -> y = x  || snd (Monomial.div (LinPoly.MonT.retrieve y) x') = 0) cstr.coeffs 
+	  if List.for_all (fun (y,_) -> Pervasives.(=) y x  || Int.equal (snd (Monomial.div (LinPoly.MonT.retrieve y) x')) 0) cstr.coeffs 
 	  then Some x
 	  else None
       with Not_found -> None
@@ -974,7 +974,7 @@ let reduce_var_change psys =
 	       Some ((x,v),(x',numerator v'))
 	   with Not_found -> rel_prime vect in
 
-  let rel_prime (cstr,prf) =  if cstr.op = Eq then rel_prime cstr.coeffs else None in
+  let rel_prime (cstr,prf) =  if cstr.op == Eq then rel_prime cstr.coeffs else None in
 
   let (oeq,sys) = extract rel_prime psys in
     
@@ -1005,7 +1005,7 @@ let reduce_var_change psys =
 
   let reduce_pivot psys = 
     let is_equation (cstr,prf) = 
-      if cstr.op = Eq
+      if cstr.op == Eq
       then
 	try 
 	  Some (fst (List.hd cstr.coeffs))
@@ -1065,7 +1065,7 @@ let reduce_var_change psys =
     (* For lia, there are no equations => these precautions are not needed *)
     (* For nlia, there are equations => do not enumerate over equations! *)
     let all_planes sys = 
-      let (eq,ineq) = List.partition (fun c -> c.op = Eq) sys in
+      let (eq,ineq) = List.partition (fun c -> c.op == Eq) sys in
 	match eq with
 	  | [] -> List.rev_map (fun c -> c.coeffs) ineq
 	  | _  -> 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 77d2d9ac8..db998f32b 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -623,7 +623,7 @@ struct
 
   let parse_q term =
      match Term.kind_of_term term with
-       | Term.App(c, args) -> if c = Lazy.force coq_Qmake then
+       | Term.App(c, args) -> if Constr.equal c (Lazy.force coq_Qmake) then
              {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
        else raise ParseError
    |  _ -> raise ParseError
@@ -809,7 +809,7 @@ struct
 
   let assoc_const x l =
    try
-   snd (List.find (fun (x',y) -> x = Lazy.force x') l)
+   snd (List.find (fun (x',y) -> Constr.equal x (Lazy.force x')) l)
    with
      Not_found -> raise ParseError
 
@@ -835,7 +835,7 @@ struct
    match kind_of_term op with
     | Const x -> (assoc_const op zop_table, args.(0) , args.(1))
     |  Ind(n,0) ->
-        if op = Lazy.force coq_Eq &&   args.(0) = Lazy.force coq_Z
+        if Constr.equal op (Lazy.force coq_Eq) && Constr.equal args.(0) (Lazy.force coq_Z)
         then (Mc.OpEq, args.(1), args.(2))
         else raise ParseError
     |   _ -> failwith "parse_zop"
@@ -844,7 +844,7 @@ struct
     match kind_of_term op with
      | Const x -> (assoc_const op rop_table, args.(0) , args.(1))
      |  Ind(n,0) ->
-        if op = Lazy.force coq_Eq &&   args.(0) = Lazy.force coq_R
+        if Constr.equal op (Lazy.force coq_Eq) && Constr.equal args.(0) (Lazy.force coq_R)
         then (Mc.OpEq, args.(1), args.(2))
         else raise ParseError
     |   _ -> failwith "parse_zop"
@@ -865,7 +865,7 @@ struct
 
   let assoc_ops x l =
    try
-     snd (List.find (fun (x',y) -> x = Lazy.force x') l)
+     snd (List.find (fun (x',y) -> Constr.equal x (Lazy.force x')) l)
    with
      Not_found -> Ukn "Oups"
 
@@ -992,9 +992,9 @@ struct
   let rec rconstant term =
    match Term.kind_of_term term with
     | Const x ->
-        if term = Lazy.force coq_R0
+        if Constr.equal term (Lazy.force coq_R0)
         then Mc.C0
-        else if term = Lazy.force coq_R1
+        else if Constr.equal term (Lazy.force coq_R1)
         then Mc.C1
         else raise ParseError
     | App(op,args) -> 
@@ -1008,8 +1008,8 @@ struct
 	  with
 	      ParseError -> 
 		match op with
-		  | op when op = Lazy.force coq_Rinv -> Mc.CInv(rconstant args.(0))
-		  | op when op = Lazy.force coq_IQR  -> Mc.CQ (parse_q args.(0))
+		  | op when Constr.equal op (Lazy.force coq_Rinv) -> Mc.CInv(rconstant args.(0))
+		  | op when Constr.equal op (Lazy.force coq_IQR)  -> Mc.CQ (parse_q args.(0))
 (*		  | op when op = Lazy.force coq_IZR  -> Mc.CZ (parse_z args.(0))*)
 		  | _ ->  raise ParseError
 	end
@@ -1188,7 +1188,7 @@ let same_proof sg cl1 cl2 =
   match sg with
    | [] -> true
    | n::sg ->
-     (try List.nth cl1 n = List.nth cl2 n with Invalid_argument _ -> false)
+     (try Int.equal (List.nth cl1 n) (List.nth cl2 n) with Invalid_argument _ -> false)
       && (xsame_proof sg ) in
   xsame_proof sg
 
@@ -1483,7 +1483,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
   let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
     let hyps_idx = prover.hyps prf in
     let hyps = selecti hyps_idx old_cl in
-      is_sublist hyps new_cl in
+      is_sublist Pervasives.(=) hyps new_cl in
 
   let cnf_res = List.combine cnf_ff res in (* we get pairs clause * proof *)
 
@@ -1745,7 +1745,7 @@ open Persistent_cache
 
 module Cache = PHashtable(struct
   type t = (provername * micromega_polys)
-  let equal = (=)
+  let equal = Pervasives.(=)
   let hash  = Hashtbl.hash
 end)
 
@@ -1939,7 +1939,7 @@ let non_linear_prover_Z str o  = {
 
 module CacheZ = PHashtable(struct
   type t = (Mc.z Mc.pol * Mc.op1) list
-  let equal = (=)
+  let equal = Pervasives.(=)
   let hash  = Hashtbl.hash
 end)
 
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index 6fd79f16b..dbad25ec1 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -17,7 +17,6 @@ open Sos
 open Sos_types
 open Sos_lib
 
-
 module Mc = Micromega
 module Ml2C = Mutils.CamlToCoq
 module C2Ml = Mutils.CoqToCaml
@@ -158,7 +157,7 @@ let pure_sos  l =
     I should nonetheless be able to try something - over Z  > is equivalent to -1  >= *)
  try
   let l = List.combine l (interval 0 (List.length l -1)) in
-  let (lt,i) =  try (List.find (fun (x,_) -> snd x =  Mc.Strict) l)
+  let (lt,i) =  try (List.find (fun (x,_) -> Pervasives.(=) (snd x) Mc.Strict) l)
    with Not_found -> List.hd l in
   let plt = poly_neg (poly_of_term (expr_to_term (fst lt))) in
   let (n,polys) = sumofsquares plt in (* n * (ci * pi^2) *)
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 7d08f2116..a6c2e0a59 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -3,7 +3,6 @@ module Utils = Mutils
 open Polynomial
 open Vect
 
-
 let map_option = Utils.map_option
 let from_option = Utils.from_option
 
@@ -197,7 +196,7 @@ let pp_split_cstr o (vl,v,c,_) =
 let merge_cstr_info i1 i2 =
   let { pos = p1 ; neg = n1 ; bound = i1 ; prf = prf1 } = i1
   and { pos = p2 ; neg = n2 ; bound = i2 ; prf = prf2 } = i2 in
-    assert (p1 = p2 && n1 = n2) ;
+    assert (Int.equal p1 p2 && Int.equal n1 n2) ;
     match inter i1 i2 with
       | None -> None (* Could directly raise a system contradiction exception *)
       | Some bnd ->
@@ -209,7 +208,7 @@ let merge_cstr_info i1 i2 =
 *)
 
 let xadd_cstr vect cstr_info sys =
-  if debug && System.length sys mod 1000 = 0 then (print_string "*" ; flush stdout) ;
+  if debug && Int.equal (System.length sys mod 1000) 0 then (print_string "*" ; flush stdout) ;
   try
     let info = System.find sys vect in
       match merge_cstr_info cstr_info !info with
@@ -237,7 +236,7 @@ let normalise_cstr vect cinfo =
 	  | (_,n)::_ ->  Cstr(
 	      (if n <>/ Int 1 then List.map (fun (x,nx) -> (x,nx // n)) vect else vect),
 			     let divn x = x // n in
-			       if sign_num n = 1
+			       if Int.equal (sign_num n) 1
 			       then{cinfo with bound = (map_option divn l , map_option  divn r) }
 			       else {cinfo with pos = cinfo.neg ; neg = cinfo.pos ; bound = (map_option divn r , map_option divn l)})
 
@@ -254,7 +253,7 @@ let count v =
       | [] -> (n,p)
       | (_,vl)::v -> let sg = sign_num vl in
 		       assert (sg <> 0) ;
-	  if sg = 1 then count n (p+1) v else count (n+1) p v in
+	  if Int.equal sg 1 then count n (p+1) v else count (n+1) p v in
     count 0 0 v
 
 
@@ -306,7 +305,7 @@ let add (v1,c1)  (v2,c2)  =
   let rec xadd v1 v2  =
     match v1 , v2 with
       | (x1,n1)::v1' , (x2,n2)::v2' ->
-	  if x1 = x2
+	  if Int.equal x1 x2
 	  then
 	    let n' = (n1 // c1) +/ (n2 // c2) in
 	      if n' =/ Int 0 then xadd v1' v2'
@@ -354,7 +353,7 @@ let split x (vect: vector) info (l,m,r) =
               | Some bnd -> (vl,vect,{info with bound = Some bnd,None})::lst in
 
           let lb,rb = info.bound in
-            if sign_num vl = 1
+            if Int.equal (sign_num vl) 1
             then  (cons_bound l lb,m,cons_bound r rb)
             else (* sign_num vl = -1 *)
               (cons_bound l rb,m,cons_bound r lb)
@@ -558,7 +557,7 @@ struct
             match  l1 with
             | [] -> xpart rl (([],info)::ltl) n (info.neg+info.pos+z) p
             | (vr,vl)::rl1 ->
-		if v = vr
+		if Int.equal v vr
 		then
 		  let cons_bound lst bd =
 		    match  bd with
@@ -566,7 +565,7 @@ struct
 		      | Some bnd -> info.neg+info.pos::lst in
 
 		  let lb,rb = info.bound in
-		    if sign_num vl = 1
+		    if Int.equal (sign_num vl) 1
 		    then  xpart rl ((rl1,info)::ltl) (cons_bound n lb) z (cons_bound p rb)
 		    else  xpart rl ((rl1,info)::ltl) (cons_bound n rb) z (cons_bound p lb)
 		else
@@ -617,7 +616,7 @@ struct
   let rec unroll_until v l =
     match l with
       | [] -> (false,[])
-      | (i,_)::rl -> if i = v
+      | (i,_)::rl -> if Int.equal i v
 	then (true,rl)
 	else if i < v then unroll_until v rl else (false,l)
 
@@ -648,7 +647,7 @@ struct
 	| [] -> None
 	| (i,_)::vect ->
 	    let nb_eq = is_primal_equation_var i in
-	      if nb_eq = 2 
+	      if Int.equal nb_eq 2 
 	      then Some i else find_var vect in
 
     let rec find_eq_var eqs =
@@ -795,18 +794,18 @@ struct
       match Vect.get v v1 , Vect.get v v2 with
         | None , _ | _ , None -> None
         | Some a   , Some b   ->
-            if (sign_num a) * (sign_num b) = -1
+            if Int.equal ((sign_num a) * (sign_num b)) (-1)
             then 
 	      Some (add (p1,abs_num a) (p2,abs_num b) ,
                       {coeffs = add (v1,abs_num a) (v2,abs_num b) ;
                        op = add_op op1 op2 ;
                        cst = n1 // (abs_num a) +/ n2 // (abs_num b) })
-            else if op1 = Eq
+            else if op1 == Eq
             then Some (add (p1,minus_num (a // b)) (p2,Int 1),
                       {coeffs = add (v1,minus_num (a// b)) (v2 ,Int 1) ;
                        op     = add_op op1 op2;
                        cst    = n1 // (minus_num (a// b)) +/ n2 // (Int 1)})
-            else if op2 = Eq
+            else if op2 == Eq
 	    then
 	      Some (add (p2,minus_num (b // a)) (p1,Int 1),
                    {coeffs = add (v2,minus_num (b// a)) (v1 ,Int 1) ;
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index ce7496fec..32816e878 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -74,13 +74,13 @@ let rec map3 f l1 l2 l3 =
     | e1::l1 , e2::l2 , e3::l3 -> (f e1 e2 e3)::(map3 f l1 l2 l3)
     |      _   -> invalid_arg "map3"
 
-let rec is_sublist l1 l2 =
+let rec is_sublist f l1 l2 =
   match l1 ,l2 with
     | [] ,_ -> true
     | e::l1', [] -> false
     | e::l1' , e'::l2' ->
-	if e = e' then is_sublist l1' l2'
-	else is_sublist l1 l2'
+	if f e e' then is_sublist f l1' l2'
+	else is_sublist f l1 l2'
 
 let list_try_find f =
   let rec try_find_f = function
@@ -144,7 +144,7 @@ let rec rec_gcd_list c l  =
 
 let gcd_list l =
  let res = rec_gcd_list zero_big_int l in
-  if compare_big_int res zero_big_int = 0
+  if Int.equal (compare_big_int res zero_big_int) 0
   then unit_big_int else res
 
 let rats_to_ints l =
@@ -192,7 +192,7 @@ let  select_pos lpos l =
       match l with
        | []   -> failwith "select_pos"
        | e::l ->
-	  if i = j
+	  if Int.equal i j
 	  then e:: (xselect (i+1) rpos l)
 	  else xselect (i+1) lpos l in
   xselect 0 lpos l
@@ -269,19 +269,19 @@ struct
 
 
  let rec positive n =
-  if n=1 then XH
-  else if n land 1 = 1 then XI (positive (n lsr 1))
+  if Int.equal n 1 then XH
+  else if Int.equal (n land 1) 1 then XI (positive (n lsr 1))
   else  XO (positive (n lsr 1))
 
  let n nt =
   if nt < 0
   then assert false
-  else if nt = 0 then N0
+  else if Int.equal nt 0 then N0
   else Npos (positive nt)
 
  let rec index  n =
-  if n=1 then XH
-  else if n land 1 = 1 then XI (index (n lsr 1))
+  if Int.equal n 1 then XH
+  else if Int.equal (n land 1) 1 then XI (index (n lsr 1))
   else  XO (index (n lsr 1))
 
 
@@ -289,8 +289,8 @@ struct
   (*a.k.a path_of_int *)
   (* returns the list of digits of n in reverse order with initial 1 removed *)
   let rec digits_of_int n =
-   if n=1 then []
-   else (n mod 2 = 1)::(digits_of_int (n lsr 1))
+   if Int.equal n 1 then []
+   else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1))
   in
    List.fold_right
     (fun b c -> (if b then XI c else XO c))
@@ -342,7 +342,7 @@ struct
    | [] -> 0 (* Equal *)
    | f::l ->
       let cmp = f () in
-       if cmp = 0 then compare_lexical l else cmp
+       if Int.equal cmp 0 then compare_lexical l else cmp
 
  let rec compare_list cmp l1 l2 =
   match l1 , l2 with
@@ -351,7 +351,7 @@ struct
    | _   , [] -> 1
    | e1::l1 , e2::l2 ->
       let c = cmp e1 e2 in
-       if c = 0 then compare_list cmp l1 l2 else c
+       if Int.equal c 0 then compare_list cmp l1 l2 else c
 
 (**
   * hash_list takes a hash function and a list, and computes an integer which
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 39a1b82b0..a6a45d6ec 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -12,7 +12,6 @@
 (*                                                                      *)
 (************************************************************************)
 
-
 module type PHashtable =
   sig
     type 'a t
@@ -172,7 +171,7 @@ let close t =
 
 let add t k e =
   let {outch = outch ; status = status ; htbl = tbl} = t in
-    if status = Closed
+    if status == Closed
     then raise UnboundTable
     else
       let fd = descr_of_out_channel outch in
@@ -187,7 +186,7 @@ let add t k e =
 
 let find t k =
   let {outch = outch ; status = status ; htbl = tbl} = t in
-    if status = Closed
+    if status == Closed
     then raise UnboundTable
     else
       let res = Table.find tbl k in