Delete trailing whitespaces in all *.{v,ml*} files

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

1 files changed, 179 insertions, 179 deletions

diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 2a1c2fe22..c5760229c 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -47,28 +47,28 @@ struct
  (* A monomial is represented by a multiset of variables  *)
  module Map = Map.Make(struct type t = var let compare = Pervasives.compare end)
  open Map
- 
+
  type t = int Map.t
 
  (* The monomial that corresponds to a constant *)
  let const = Map.empty
-  
+
  (* The monomial 'x' *)
  let var x = Map.add x 1 Map.empty
 
  (* Get the degre of a variable in a monomial *)
  let find x m = try find x m with Not_found -> 0
-  
+
  (* Multiply a monomial by a variable *)
  let mult x m = add x (  (find x m) + 1) m
-  
+
  (* Product of monomials *)
  let prod m1 m2 = Map.fold (fun k d m -> add k ((find k m) + d) m) m1 m2
-  
+
  (* Total ordering of monomials *)
  let compare m1 m2 = Map.compare Pervasives.compare m1 m2
 
- let pp o m = Map.iter (fun k v -> 
+ let pp o m = Map.iter (fun k v ->
   if v = 1 then Printf.fprintf o "x%i." (C2Ml.index k)
   else     Printf.fprintf o "x%i^%i." (C2Ml.index k) v) m
 
@@ -79,8 +79,8 @@ end
 
 module Poly :
  (* A polynomial is a map of monomials *)
- (* 
-    This is probably a naive implementation 
+ (*
+    This is probably a naive implementation
     (expected to be fast enough - Coq is probably the bottleneck)
     *The new ring contribution is using a sparse Horner representation.
  *)
@@ -106,22 +106,22 @@ struct
 
  type t = num P.t
 
- let pp o p = P.iter (fun k v -> 
+ let pp o p = P.iter (fun k v ->
   if compare_num v (Int 0) <> 0
-  then 
+  then
    if Monomial.compare Monomial.const k = 0
    then         Printf.fprintf o "%s " (string_of_num v)
-   else Printf.fprintf o "%s*%a " (string_of_num v) Monomial.pp k) p  
+   else Printf.fprintf o "%s*%a " (string_of_num v) Monomial.pp k) p
 
  (* Get the coefficient of monomial mn *)
- let get : Monomial.t -> t -> num = 
+ let get : Monomial.t -> t -> num =
   fun mn p -> try find mn p with Not_found -> (Int 0)
 
 
  (* The polynomial 1.x *)
  let variable : var -> t =
   fun  x ->  add (Monomial.var x) (Int 1) empty
-   
+
  (*The constant polynomial *)
  let constant : num -> t =
   fun c -> add (Monomial.const) c empty
@@ -129,27 +129,27 @@ struct
  (* The addition of a monomial *)
 
  let add : Monomial.t -> num -> t -> t =
-  fun mn v p -> 
+  fun mn v p ->
    let vl = (get mn p) <+> v in
     add mn vl p
 
 
- (** Design choice: empty is not a polynomial 
-     I do not remember why .... 
+ (** Design choice: empty is not a polynomial
+     I do not remember why ....
  **)
 
  (* The product by a monomial *)
  let mult : Monomial.t -> num -> t -> t =
-  fun mn v p -> 
+  fun mn v p ->
    fold (fun mn' v' res -> P.add (Monomial.prod mn mn') (v<*>v') res) p empty
 
 
  let  addition : t -> t -> t =
   fun p1 p2 -> fold (fun mn v p -> add mn v p) p1 p2
-   
+
 
  let product : t -> t -> t =
-  fun p1 p2 -> 
+  fun p1 p2 ->
    fold (fun mn v res -> addition (mult mn v p2) res ) p1 empty
 
 
@@ -181,7 +181,7 @@ let z_spec = {
  mult = Mc.zmult;
  eqb  = Mc.zeq_bool
 }
- 
+
 
 let q_spec = {
  bigint_to_number = (fun x -> {Mc.qnum = Ml2C.bigint x; Mc.qden = Mc.XH});
@@ -198,53 +198,53 @@ let r_spec = z_spec
 
 
 let dev_form n_spec  p =
- let rec dev_form p = 
+ let rec dev_form p =
   match p with
    | Mc.PEc z ->  Poly.constant (n_spec.number_to_num z)
    | Mc.PEX v ->  Poly.variable v
-   | Mc.PEmul(p1,p2) -> 
+   | Mc.PEmul(p1,p2) ->
       let p1 = dev_form p1 in
       let p2 = dev_form p2 in
-       Poly.product p1 p2 
+       Poly.product p1 p2
    | Mc.PEadd(p1,p2) -> Poly.addition (dev_form p1) (dev_form p2)
    | Mc.PEopp p ->  Poly.uminus (dev_form p)
    | Mc.PEsub(p1,p2) ->  Poly.addition (dev_form p1) (Poly.uminus (dev_form p2))
-   | Mc.PEpow(p,n)   ->  
+   | Mc.PEpow(p,n)   ->
       let p = dev_form p in
       let n = C2Ml.n n in
-      let rec pow n = 
-       if n = 0 
+      let rec pow n =
+       if n = 0
        then Poly.constant (n_spec.number_to_num n_spec.unit)
        else Poly.product p (pow (n-1)) in
        pow n in
   dev_form p
 
 
-let monomial_to_polynomial mn = 
- Monomial.fold 
-  (fun v i acc -> 
+let monomial_to_polynomial mn =
+ Monomial.fold
+  (fun v i acc ->
    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)
-    then mn 
+    then mn
     else Mc.PEmul(mn,acc))
-  mn 
+  mn
   (Mc.PEc (Mc.Zpos Mc.XH))
-  
-let list_to_polynomial vars l = 
+
+let list_to_polynomial vars l =
  assert (List.for_all (fun x -> ceiling_num x =/ x) l);
- let var x = monomial_to_polynomial (List.nth vars x)  in 
+ let var x = monomial_to_polynomial (List.nth vars x)  in
  let rec xtopoly p i = function
   | [] -> p
-  | c::l -> if c =/  (Int 0) then xtopoly p (i+1) 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 = 
+    let mn =
      if 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
       Mc.PEadd (mn, p) in
      xtopoly p' (i+1) l in
-  
+
   xtopoly (Mc.PEc Mc.Z0) 0 l
 
 let rec fixpoint f x =
@@ -259,54 +259,54 @@ let rec fixpoint f x =
 
 
 
-let  rec_simpl_cone n_spec e = 
- let simpl_cone = 
+let  rec_simpl_cone n_spec e =
+ let simpl_cone =
   Mc.simpl_cone n_spec.zero n_spec.unit n_spec.mult n_spec.eqb in
 
  let rec rec_simpl_cone  = function
- | Mc.PsatzMulE(t1, t2) -> 
+ | Mc.PsatzMulE(t1, t2) ->
     simpl_cone  (Mc.PsatzMulE (rec_simpl_cone t1, rec_simpl_cone t2))
- | Mc.PsatzAdd(t1,t2)  -> 
+ | Mc.PsatzAdd(t1,t2)  ->
     simpl_cone (Mc.PsatzAdd (rec_simpl_cone t1, rec_simpl_cone t2))
  |  x           -> simpl_cone x in
   rec_simpl_cone e
-   
-   
+
+
 let simplify_cone n_spec c = fixpoint (rec_simpl_cone n_spec) c
- 
-type cone_prod = 
-  Const of cone 
-  | Ideal of cone *cone 
-  | Mult of cone * cone 
+
+type cone_prod =
+  Const of cone
+  | Ideal of cone *cone
+  | Mult of cone * cone
   | Other of cone
 and cone =   Mc.zWitness
 
 
 
 let factorise_linear_cone c =
- 
- let rec cone_list  c l = 
+
+ let rec cone_list  c l =
   match c with
    | Mc.PsatzAdd (x,r) -> cone_list  r (x::l)
    |  _        ->  c :: l in
-  
+
  let factorise c1 c2 =
   match c1 , c2 with
-   | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') -> 
+   | Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') ->
       if x = x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None
-   | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') -> 
+   | Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') ->
       if x = x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None
    |  _     -> None in
-  
+
  let rec rebuild_cone l pending  =
   match l with
    | [] -> (match pending with
       | None -> Mc.PsatzZ
       | Some p -> p
      )
-   | e::l -> 
+   | e::l ->
       (match pending with
-       | None -> rebuild_cone l (Some e) 
+       | None -> rebuild_cone l (Some e)
        | Some p -> (match factorise p e with
           | None -> Mc.PsatzAdd(p, rebuild_cone l (Some e))
           | Some f -> rebuild_cone l (Some f) )
@@ -316,15 +316,15 @@ let factorise_linear_cone c =
 
 
 
-(* The binding with Fourier might be a bit obsolete 
+(* The binding with Fourier might be a bit obsolete
    -- how does it handle equalities ? *)
 
 (* Certificates are elements of the cone such that P = 0  *)
 
 (* To begin with, we search for certificates of the form:
-   a1.p1 + ... an.pn + b1.q1 +... + bn.qn + c = 0   
+   a1.p1 + ... an.pn + b1.q1 +... + bn.qn + c = 0
    where pi >= 0 qi > 0
-   ai >= 0 
+   ai >= 0
    bi >= 0
    Sum bi + c >= 1
    This is a linear problem: each monomial is considered as a variable.
@@ -343,96 +343,96 @@ open Mfourier
 
 (* fold_left followed by a rev ! *)
 
-let constrain_monomial mn l  = 
+let constrain_monomial mn l  =
  let coeffs = List.fold_left (fun acc p -> (Poly.get mn p)::acc) [] l in
   if mn = Monomial.const
-  then  
-   { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ; 
-     op = Eq ; 
+  then
+   { coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ;
+     op = Eq ;
      cst = Big_int zero_big_int  }
   else
-   { coeffs = Vect.from_list ((Big_int zero_big_int):: (List.rev coeffs)) ; 
-     op = Eq ; 
+   { coeffs = Vect.from_list ((Big_int zero_big_int):: (List.rev coeffs)) ;
+     op = Eq ;
      cst = Big_int zero_big_int  }
 
-    
-let positivity l = 
- let rec xpositivity i l = 
+
+let positivity l =
+ let rec xpositivity i l =
   match l with
    | [] -> []
    | (_,Mc.Equal)::l -> xpositivity (i+1) l
-   | (_,_)::l -> 
-      {coeffs = Vect.update (i+1) (fun _ -> Int 1) Vect.null ; 
-       op = Ge ; 
+   | (_,_)::l ->
+      {coeffs = Vect.update (i+1) (fun _ -> Int 1) Vect.null ;
+       op = Ge ;
        cst = Int 0 }  :: (xpositivity (i+1) l)
  in
   xpositivity 0 l
 
 
 let string_of_op = function
- | Mc.Strict -> "> 0" 
- | Mc.NonStrict -> ">= 0" 
+ | Mc.Strict -> "> 0"
+ | Mc.NonStrict -> ">= 0"
  | Mc.Equal -> "= 0"
  | Mc.NonEqual -> "<> 0"
 
 
 
-(* If the certificate includes at least one strict inequality, 
+(* If the certificate includes at least one strict inequality,
    the obtained polynomial can also be 0 *)
 let build_linear_system l =
 
  (* Gather the monomials:  HINT add up of the polynomials *)
  let l' = List.map fst l in
- let monomials = 
+ let monomials =
   List.fold_left (fun acc p -> Poly.addition p acc) (Poly.constant (Int 0)) l'
  in  (* For each monomial, compute a constraint *)
- let s0 = 
+ let s0 =
   Poly.fold (fun mn _ res -> (constrain_monomial mn l')::res) monomials [] in
   (* I need at least something strictly positive *)
  let strict = {
   coeffs = Vect.from_list ((Big_int unit_big_int)::
-                            (List.map (fun (x,y) -> 
-			      match y with Mc.Strict -> 
-				  Big_int unit_big_int 
+                            (List.map (fun (x,y) ->
+			      match y with Mc.Strict ->
+				  Big_int unit_big_int
                               | _ -> Big_int zero_big_int) l));
   op = Ge ; cst = Big_int unit_big_int } in
   (* Add the positivity constraint *)
-  {coeffs = Vect.from_list ([Big_int unit_big_int]) ; 
-   op = Ge ; 
+  {coeffs = Vect.from_list ([Big_int unit_big_int]) ;
+   op = Ge ;
    cst = Big_int zero_big_int}::(strict::(positivity l)@s0)
 
 
 let big_int_to_z = Ml2C.bigint
- 
-(* For Q, this is a pity that the certificate has been scaled 
+
+(* For Q, this is a pity that the certificate has been scaled
    -- at a lower layer, certificates are using nums... *)
-let make_certificate n_spec (cert,li) = 
+let make_certificate n_spec (cert,li) =
  let bint_to_cst = n_spec.bigint_to_number in
   match cert with
    | [] -> failwith "empty_certificate"
-   | e::cert' -> 
+   | e::cert' ->
       let cst = match compare_big_int e zero_big_int with
        | 0 -> Mc.PsatzZ
-       | 1 ->  Mc.PsatzC (bint_to_cst e) 
-       | _ -> failwith "positivity error" 
+       | 1 ->  Mc.PsatzC (bint_to_cst e)
+       | _ -> failwith "positivity error"
       in
       let rec scalar_product cert l =
        match cert with
         | [] -> Mc.PsatzZ
         | c::cert -> match l with
            | [] -> failwith "make_certificate(1)"
-           | i::l ->  
+           | i::l ->
               let r = scalar_product cert l in
                match compare_big_int c  zero_big_int with
                 | -1 -> Mc.PsatzAdd (
-                   Mc.PsatzMulC (Mc.Pc ( bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)), 
+                   Mc.PsatzMulC (Mc.Pc ( bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)),
                    r)
                 | 0  -> r
                 | _ ->  Mc.PsatzAdd (
                    Mc.PsatzMulE (Mc.PsatzC (bint_to_cst c), Mc.PsatzIn (Ml2C.nat i)),
                    r) in
-       
-        ((factorise_linear_cone 
+
+        ((factorise_linear_cone
              (simplify_cone n_spec (Mc.PsatzAdd (cst, scalar_product cert' li)))))
 
 
@@ -440,59 +440,59 @@ exception Found of Monomial.t
 
 exception Strict
 
-let primal l = 
+let primal l =
   let vr = ref 0 in
   let module Mmn = Map.Make(Monomial) in
 
   let vect_of_poly map p =
-    Poly.fold (fun mn vl (map,vect) -> 
-      if mn = Monomial.const 
+    Poly.fold (fun mn vl (map,vect) ->
+      if mn = Monomial.const
       then (map,vect)
-      else 
+      else
 	let (mn,m) = try (Mmn.find mn map,map) with Not_found -> let res = (!vr, Mmn.add mn !vr map) in incr vr ; res in
 	  (m,if 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
 
   let cmp x y = Pervasives.compare (fst x) (fst y) in
 
    snd (List.fold_right (fun  (p,op) (map,l) ->
-      let (mp,vect) = vect_of_poly map p in  
+      let (mp,vect) = vect_of_poly map p in
       let cstr = {coeffs = List.sort cmp vect; op = op_op op ; cst = minus_num (Poly.get Monomial.const p)} in
 
 	(mp,cstr::l)) l (Mmn.empty,[]))
 
-let dual_raw_certificate (l:  (Poly.t * Mc.op1) list) = 
+let dual_raw_certificate (l:  (Poly.t * Mc.op1) list) =
 (*  List.iter (fun (p,op) -> Printf.fprintf stdout "%a %s 0\n" Poly.pp p (string_of_op op) ) l ; *)
-    
-    
+
+
  let sys = build_linear_system l in
 
-   try 
+   try
    match Fourier.find_point sys with
     | Inr _ -> None
-    | Inl cert ->  Some (rats_to_ints (Vect.to_list cert)) 
+    | Inl cert ->  Some (rats_to_ints (Vect.to_list cert))
        (* should not use rats_to_ints *)
-  with x -> 
-   if debug 
-   then (Printf.printf "raw certificate %s" (Printexc.to_string x);   
+  with x ->
+   if debug
+   then (Printf.printf "raw certificate %s" (Printexc.to_string x);
          flush stdout) ;
    None
 
 
-let raw_certificate l = 
-  try 
+let raw_certificate l =
+  try
     let p = primal l in
       match Fourier.find_point p with
-	| Inr prf -> 
-	    if debug then Printf.printf "AProof : %a\n" pp_proof prf ; 
+	| Inr prf ->
+	    if debug then Printf.printf "AProof : %a\n" pp_proof prf ;
 	    let cert = List.map (fun (x,n) -> x+1,n) (fst (List.hd (Proof.mk_proof p prf))) in
-	      if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ; 
+	      if debug then Printf.printf "CProof : %a" Vect.pp_vect cert ;
 	      Some (rats_to_ints (Vect.to_list cert))
 	| Inl _   -> None
-  with Strict -> 
+  with Strict ->
     (* Fourier elimination should handle > *)
-    dual_raw_certificate l 
+    dual_raw_certificate l
 
 
 let simple_linear_prover (*to_constant*) l =
@@ -500,26 +500,26 @@ let simple_linear_prover (*to_constant*) l =
   match raw_certificate lc with
    |  None -> None (* No certificate *)
    | Some cert -> (* make_certificate to_constant*)Some (cert,li)
-      
-      
+
+
 
 let linear_prover n_spec l  =
  let li = List.combine l (interval 0 (List.length l -1)) in
- let (l1,l') = List.partition 
+ let (l1,l') = List.partition
   (fun (x,_) -> if snd x = Mc.NonEqual then true else false) li in
- let l' = List.map 
+ let l' = List.map
   (fun ((x,y),i) -> match y with
                    Mc.NonEqual -> failwith "cannot happen"
                   |  y -> ((dev_form n_spec x, y),i)) l' in
-  
-  simple_linear_prover (*n_spec*) l' 
+
+  simple_linear_prover (*n_spec*) l'
 
 
 let linear_prover n_spec l  =
  try linear_prover n_spec l with
    x -> (print_string (Printexc.to_string x); None)
 
-let linear_prover_with_cert spec l = 
+let linear_prover_with_cert spec l =
   match linear_prover spec l with
     | None -> None
     | Some cert -> Some (make_certificate spec cert)
@@ -529,21 +529,21 @@ let linear_prover_with_cert spec l =
 (* zprover.... *)
 
 (* I need to gather the set of variables --->
-   Then go for fold 
+   Then go for fold
    Once I have an interval, I need a certificate : 2 other fourier elims.
-   (I could probably get the certificate directly 
+   (I could probably get the certificate directly
    as it is done in the fourier contrib.)
 *)
 
 let make_linear_system l =
  let l' = List.map fst l in
- let monomials = List.fold_left (fun acc p -> Poly.addition p acc) 
+ let monomials = List.fold_left (fun acc p -> Poly.addition p acc)
   (Poly.constant (Int 0)) l' in
- let monomials = Poly.fold 
+ let monomials = Poly.fold
   (fun mn _ l -> if 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 ; 
+  (List.map (fun (c,op) ->
+   {coeffs = Vect.from_list (List.map (fun mn ->  (Poly.get mn c)) monomials) ;
+    op = op ;
     cst = minus_num ( (Poly.get Monomial.const c))}) l
     ,monomials)
 
@@ -552,106 +552,106 @@ let pplus x y = Mc.PEadd(x,y)
 let pmult x y = Mc.PEmul(x,y)
 let pconst x = Mc.PEc x
 let popp x = Mc.PEopp x
- 
+
 let debug = false
- 
+
 (* keep track of enumerated vectors *)
-let rec mem p x  l = 
+let rec mem p x  l =
  match l with  [] -> false | e::l -> if p x e then true else mem p x l
 
-let rec remove_assoc p x l = 
+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) 
+  remove_assoc p x l else e::(remove_assoc p x l)
 
 let eq x y = 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
 
 
-(* The prover is (probably) incomplete -- 
+(* The prover is (probably) incomplete --
    only searching for naive cutting planes *)
 
-let candidates sys = 
+let candidates sys =
  let ll = List.fold_right (
   fun (e,k) r ->
-   match k with 
+   match k with
     | Mc.NonStrict -> (dev_form z_spec e , Ge)::r
-    | Mc.Equal     ->  (dev_form z_spec e , Eq)::r 
+    | Mc.Equal     ->  (dev_form z_spec e , Eq)::r
        (* we already know the bound -- don't compute it again *)
     | _     -> failwith "Cannot happen candidates") sys [] in
 
  let (sys,var_mn) = make_linear_system ll in
  let vars = mapi (fun _ i -> Vect.set i (Int 1) Vect.null) var_mn in
-  (List.fold_left (fun l cstr ->   
+  (List.fold_left (fun l cstr ->
    let gcd = Big_int (Vect.gcd cstr.coeffs) in
-    if gcd =/ (Int 1) && cstr.op = Eq 
-    then l 
+    if gcd =/ (Int 1) && cstr.op = Eq
+    then l
     else  (Vect.mul (Int 1 // gcd) cstr.coeffs)::l) [] sys) @ vars
 
 
 
 
-let rec xzlinear_prover planes sys = 
+let rec xzlinear_prover planes sys =
  match linear_prover z_spec sys with
   | Some prf ->  Some (Mc.RatProof (make_certificate z_spec prf,Mc.DoneProof))
   | None     -> (* find the candidate with the smallest range *)
      (* Grrr - linear_prover is also calling 'make_linear_system' *)
      let ll = List.fold_right (fun (e,k) r -> match k with
-       Mc.NonEqual -> r  
-      | k -> (dev_form z_spec e , 
+       Mc.NonEqual -> r
+      | k -> (dev_form z_spec e ,
              match k with
-               Mc.NonStrict -> Ge 
+               Mc.NonStrict -> Ge
               | Mc.Equal              -> Eq
               | Mc.Strict | Mc.NonEqual -> failwith "Cannot happen") :: r) sys [] in
      let (ll,var) = make_linear_system ll in
-     let candidates = List.fold_left (fun  acc vect -> 
+     let candidates = List.fold_left (fun  acc vect ->
       match Fourier.optimise vect ll with
        | None -> acc
-       | Some i -> 
+       | Some i ->
 (*	  Printf.printf "%s in %s\n" (Vect.string vect) (string_of_intrvl i) ; *)
-	  flush stdout ; 
+	  flush stdout ;
 	  (vect,i) ::acc)  [] planes in
 
-     let smallest_interval = 
-      match List.fold_left (fun (x1,i1) (x2,i2) -> 
-       if Itv.smaller_itv i1 i2 
-       then (x1,i1) else (x2,i2)) (Vect.null,(None,None)) candidates 
+     let smallest_interval =
+      match List.fold_left (fun (x1,i1) (x2,i2) ->
+       if Itv.smaller_itv i1 i2
+       then (x1,i1) else (x2,i2)) (Vect.null,(None,None)) candidates
       with
        | (x,(Some i, Some j))  -> Some(i,x,j)
        |   x        ->   None (* This might be a cutting plane *)
       in
       match smallest_interval with
-       | Some (lb,e,ub) -> 
-          let (lbn,lbd) = 
+       | Some (lb,e,ub) ->
+          let (lbn,lbd) =
            (Ml2C.bigint (sub_big_int (numerator lb)  unit_big_int),
            Ml2C.bigint (denominator lb)) in
-          let (ubn,ubd) = 
-           (Ml2C.bigint (add_big_int unit_big_int (numerator ub)) , 
+          let (ubn,ubd) =
+           (Ml2C.bigint (add_big_int unit_big_int (numerator ub)) ,
            Ml2C.bigint (denominator ub)) in
           let expr = list_to_polynomial var (Vect.to_list e) in
-           (match 
+           (match
              (*x <= ub ->  x  > ub *)
-             linear_prover  z_spec 
+             linear_prover  z_spec
               ((pplus (pmult (pconst ubd) expr) (popp (pconst  ubn)),
                       Mc.NonStrict) :: sys),
             (* lb <= x  -> lb > x *)
-            linear_prover z_spec 
+            linear_prover z_spec
              ((pplus (popp (pmult  (pconst lbd) expr)) (pconst lbn),
-                     Mc.NonStrict)::sys) 
+                     Mc.NonStrict)::sys)
             with
-             | Some cub , Some clb  ->   
-                (match zlinear_enum  (remove e planes)   expr 
-                  (ceiling_num lb)  (floor_num ub) sys 
+             | Some cub , Some clb  ->
+                (match zlinear_enum  (remove e planes)   expr
+                  (ceiling_num lb)  (floor_num ub) sys
                  with
                   | None -> None
-                  | Some prf -> 
-		      let bound_proof (c,l) = make_certificate z_spec (List.tl c , List.tl (List.map (fun x -> x -1) l)) in 
-		      
+                  | Some prf ->
+		      let bound_proof (c,l) = make_certificate z_spec (List.tl c , List.tl (List.map (fun x -> x -1) l)) in
+
                      Some (Mc.EnumProof((*Ml2C.q lb,expr,Ml2C.q ub,*) bound_proof clb, bound_proof cub,prf)))
              | _ -> None
            )
        |  _ -> None
-and zlinear_enum  planes expr clb cub l = 
+and zlinear_enum  planes expr clb cub l =
  if clb >/  cub
  then Some []
  else
@@ -665,9 +665,9 @@ and zlinear_enum  planes expr clb cub l =
      | None -> None
      | Some prfl -> Some (prf :: prfl)
 
-let zlinear_prover sys =  
+let zlinear_prover sys =
  let candidates = candidates sys in
- (*  Printf.printf "candidates %d" (List.length candidates) ; *) 
+ (*  Printf.printf "candidates %d" (List.length candidates) ; *)
  (*let t0 = Sys.time () in*)
  let res = xzlinear_prover candidates sys in
    (*Printf.printf "Time prover : %f" (Sys.time () -. t0) ;*) res
@@ -675,7 +675,7 @@ let zlinear_prover sys =
 open Sos_types
 open Mutils
 
-let rec scale_term t = 
+let rec scale_term t =
  match t with
   | Zero    -> unit_big_int , Zero
   | Const n ->  (denominator n) , Const (Big_int (numerator n))
@@ -708,7 +708,7 @@ let get_index_of_ith_match f i l  =
   match l with
    | [] -> failwith "bad index"
    | e::l -> if f e
-     then 
+     then
        (if j = i then res else get (j+1) (res+1) l )
      else get j (res+1) l in
   get 0 0 l
@@ -722,19 +722,19 @@ let rec scale_certificate pos = match pos with
  | Rational_eq n ->  (denominator n) , Rational_eq (Big_int (numerator n))
  | Rational_le n ->  (denominator n) , Rational_le (Big_int (numerator n))
  | Rational_lt n ->  (denominator n) , Rational_lt (Big_int (numerator n))
- | Square t -> let s,t' =  scale_term t in 
+ | Square t -> let s,t' =  scale_term t in
 		mult_big_int s s , Square t'
  | Eqmul (t, y) -> let s1,y1 = scale_term t and s2,y2 = scale_certificate y in
 		    mult_big_int s1 s2 , Eqmul (y1,y2)
- | Sum (y, z) -> let s1,y1 = scale_certificate y 
+ | Sum (y, z) -> let s1,y1 = scale_certificate y
    and s2,y2 = scale_certificate z in
    let g = gcd_big_int s1 s2 in
    let s1' = div_big_int s1 g in
    let s2' = div_big_int s2 g in
-    mult_big_int g (mult_big_int s1' s2'), 
+    mult_big_int g (mult_big_int s1' s2'),
     Sum (Product(Rational_le (Big_int s2'), y1),
 	Product (Rational_le (Big_int s1'), y2))
- | Product (y, z) -> 
+ | Product (y, z) ->
     let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in
      mult_big_int s1 s2 , Product (y1,y2)
 
@@ -743,7 +743,7 @@ open Micromega
  let rec term_to_q_expr = function
   | Const n ->  PEc (Ml2C.q n)
   | Zero   ->  PEc ( Ml2C.q (Int 0))
-  | Var s   ->  PEX (Ml2C.index 
+  | Var s   ->  PEX (Ml2C.index
 		      (int_of_string (String.sub s 1 (String.length s - 1))))
   | Mul(p1,p2) ->  PEmul(term_to_q_expr p1, term_to_q_expr p2)
   | Add(p1,p2) ->   PEadd(term_to_q_expr p1, term_to_q_expr p2)
@@ -755,20 +755,20 @@ open Micromega
  let term_to_q_pol e = Mc.norm_aux (Ml2C.q (Int 0)) (Ml2C.q (Int 1)) Mc.qplus  Mc.qmult Mc.qminus Mc.qopp Mc.qeq_bool (term_to_q_expr e)
 
 
- let rec product l = 
+ let rec product l =
    match l with
      | [] -> Mc.PsatzZ
      | [i] -> Mc.PsatzIn (Ml2C.nat i)
      | i ::l -> Mc.PsatzMulE(Mc.PsatzIn (Ml2C.nat i), product l)
 
 
-let  q_cert_of_pos  pos = 
+let  q_cert_of_pos  pos =
  let rec _cert_of_pos = function
    Axiom_eq i ->  Mc.PsatzIn (Ml2C.nat i)
   | Axiom_le i ->  Mc.PsatzIn (Ml2C.nat i)
   | Axiom_lt i ->  Mc.PsatzIn (Ml2C.nat i)
   | Monoid l  -> product l
-  | Rational_eq n | Rational_le n | Rational_lt n -> 
+  | Rational_eq n | Rational_le n | Rational_lt n ->
      if compare_num n (Int 0) = 0 then Mc.PsatzZ else
       Mc.PsatzC (Ml2C.q   n)
   | Square t -> Mc.PsatzSquare (term_to_q_pol  t)
@@ -781,7 +781,7 @@ let  q_cert_of_pos  pos =
  let rec term_to_z_expr = function
   | Const n ->  PEc (Ml2C.bigint (big_int_of_num n))
   | Zero   ->  PEc ( Z0)
-  | Var s   ->  PEX (Ml2C.index 
+  | Var s   ->  PEX (Ml2C.index
 		      (int_of_string (String.sub s 1 (String.length s - 1))))
   | Mul(p1,p2) ->  PEmul(term_to_z_expr p1, term_to_z_expr p2)
   | Add(p1,p2) ->   PEadd(term_to_z_expr p1, term_to_z_expr p2)
@@ -792,14 +792,14 @@ let  q_cert_of_pos  pos =
 
  let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.zplus  Mc.zmult Mc.zminus Mc.zopp Mc.zeq_bool (term_to_z_expr e)
 
-let  z_cert_of_pos  pos = 
+let  z_cert_of_pos  pos =
  let s,pos = (scale_certificate pos) in
  let rec _cert_of_pos = function
    Axiom_eq i ->  Mc.PsatzIn (Ml2C.nat i)
   | Axiom_le i ->  Mc.PsatzIn (Ml2C.nat i)
   | Axiom_lt i ->  Mc.PsatzIn (Ml2C.nat i)
   | Monoid l  -> product l
-  | Rational_eq n | Rational_le n | Rational_lt n -> 
+  | Rational_eq n | Rational_le n | Rational_lt n ->
      if 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)