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

22 files changed, 1174 insertions, 1174 deletions

diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v
index 631417e0e9..231004bca2 100644
--- a/plugins/micromega/Env.v
+++ b/plugins/micromega/Env.v
@@ -17,9 +17,9 @@ Require Import Coq.Arith.Max.
 Require Import List.
 Set Implicit Arguments.
 
-(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v) 
+(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v)
    -- this is harmless and spares a lot of Empty.
-   This means smaller proof-terms. 
+   This means smaller proof-terms.
    BTW, by dropping the  polymorphism, I get small (yet noticeable) speed-up.
 *)
 
@@ -40,7 +40,7 @@ Section S.
   Lemma psucc : forall p,  (match p with
                               | xI y' => xO (Psucc y')
                               | xO y' => xI y'
-                              | 1%positive => 2%positive 
+                              | 1%positive => 2%positive
                             end) = (p+1)%positive.
   Proof.
     destruct p.
@@ -50,7 +50,7 @@ Section S.
     reflexivity.
   Qed.
 
-  Lemma jump_Pplus : forall i j l, 
+  Lemma jump_Pplus : forall i j l,
     forall x, jump (i + j) l x = jump i (jump j l) x.
   Proof.
     unfold jump.
@@ -60,7 +60,7 @@ Section S.
   Qed.
 
   Lemma jump_simpl : forall p l,
-    forall x, jump p l x = 
+    forall x, jump p l x =
     match p with
       | xH => tail l x
       | xO p => jump p (jump p l) x
@@ -80,15 +80,15 @@ Section S.
   Qed.
 
   Ltac jump_s :=
-    repeat 
+    repeat
       match goal with
         | |- context [jump xH ?e] => rewrite (jump_simpl xH)
         | |- context [jump (xO ?p) ?e] => rewrite (jump_simpl (xO p))
         | |- context [jump (xI ?p) ?e] => rewrite (jump_simpl (xI p))
       end.
-    
+
   Lemma jump_tl : forall j l, forall x, tail (jump j l) x = jump j (tail l) x.
-  Proof. 
+  Proof.
     unfold tail.
     intros.
     repeat rewrite <- jump_Pplus.
@@ -96,7 +96,7 @@ Section S.
     reflexivity.
   Qed.
 
-  Lemma jump_Psucc : forall j l, 
+  Lemma jump_Psucc : forall j l,
     forall x, (jump (Psucc j) l x) = (jump 1 (jump j l) x).
   Proof.
     intros.
@@ -129,13 +129,13 @@ Section S.
     reflexivity.
   Qed.
 
-  Lemma nth_spec : forall p l x, 
-    nth p l = 
+  Lemma nth_spec : forall p l x,
+    nth p l =
     match p with
       | xH => hd x l
       | xO p => nth p (jump p l)
       | xI p => nth p (jump p (tail l))
-    end. 
+    end.
   Proof.
     unfold nth.
     destruct p.
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 04e68272ee..e58f8e6868 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -55,12 +55,12 @@ Section MakeRingPol.
  Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
  Notation "x == y" := (req x y).
 
- (* C notations *)		
+ (* C notations *)
  Notation "x +! y" := (cadd x y). Notation "x *! y " := (cmul x y).
  Notation "x -! y " := (csub x y). Notation "-! x" := (copp x).
  Notation " x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x).
 
- (* Usefull tactics *)		
+ (* Usefull tactics *)
   Add Setoid R req Rsth as R_set1.
  Ltac rrefl := gen_reflexivity Rsth.
   Add Morphism radd : radd_ext.  exact (Radd_ext Reqe). Qed.
@@ -554,7 +554,7 @@ Section MakeRingPol.
   intros;simpl;apply (morph0 CRmorph).
  Qed.
 
-Lemma env_morph : forall p e1 e2, (forall x, e1 x = e2 x) -> 
+Lemma env_morph : forall p e1 e2, (forall x, e1 x = e2 x) ->
  p @ e1 = p @ e2.
 Proof.
   induction p ; simpl.
@@ -578,7 +578,7 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma Pjump_xO_tail : forall P p l, 
+Lemma Pjump_xO_tail : forall P p l,
   P @ (jump (xO p) (tail l)) = P @ (jump (xI p) l).
 Proof.
   intros.
@@ -743,9 +743,9 @@ Qed.
    induction P;simpl;intros;try apply (ARadd_comm ARth).
    destruct p2; simpl; try apply (ARadd_comm ARth).
    rewrite Pjump_xO_tail.
-   apply (ARadd_comm ARth).   
+   apply (ARadd_comm ARth).
    rewrite Pjump_Pdouble_minus_one.
-   apply (ARadd_comm ARth).   
+   apply (ARadd_comm ARth).
     assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2.
     rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl.
     rewrite IHP'1;simpl;Esimpl.
@@ -785,7 +785,7 @@ Qed.
   destruct p0;simpl;Esimpl2.
   rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));trivial.
   rewrite Pjump_xO_tail.
-  add_push (P @ ((jump (xI p0) l)));rrefl.  
+  add_push (P @ ((jump (xI p0) l)));rrefl.
   rewrite IHP'2;simpl;rewrite Pjump_Pdouble_minus_one;rsimpl.
   add_push (- (P'1 @ l * pow_pos  rmul (hd 0 l) p));rrefl.
   unfold tail.
@@ -931,7 +931,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
   rrefl.
  Qed.
 
- Lemma Mphi_morph : forall P env env', (forall x, env x = env' x ) -> 
+ Lemma Mphi_morph : forall P env env', (forall x, env x = env' x ) ->
    Mphi env P = Mphi env' P.
  Proof.
    induction P ; simpl.
@@ -952,7 +952,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
    intros. symmetry. apply H.
  Qed.
 
-Lemma Mjump_xO_tail : forall M p l, 
+Lemma Mjump_xO_tail : forall M p l,
   Mphi  (jump (xO p) (tail l)) M = Mphi (jump (xI p) l) M.
 Proof.
   intros.
@@ -1117,7 +1117,7 @@ Qed.
    rewrite Padd_ok; rewrite PmulC_ok; rsimpl.
  intros i P5 H; rewrite H.
    intros HH H1; injection HH; intros; subst; rsimpl.
-   rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl. 
+   rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl.
  intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
    assert (P4 = Q1 ++ P3 ** PX i P5 P6).
    injection H2; intros; subst;trivial.
@@ -1385,13 +1385,13 @@ Section POWER.
    intros.
    induction pe;simpl;Esimpl3.
    apply mkX_ok.
-   rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. 
+   rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3.
    rewrite IHpe1;rewrite IHpe2;rrefl.
    rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl.
    rewrite IHpe;rrefl.
-   rewrite Ppow_N_ok by reflexivity. 
+   rewrite Ppow_N_ok by reflexivity.
    rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
-   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; 
+   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok;
       repeat rewrite Pmul_ok;rrefl.
   Qed.
 
diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index 149b773167..803dd903a9 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.v
@@ -162,7 +162,7 @@ Qed.
 Theorem Rminus_eq_0 : forall n m : R, n - m == 0 <-> n == m.
 Proof.
 intros n m.
-split; intro H. setoid_replace n with ((n - m) + m) by ring. rewrite H. 
+split; intro H. setoid_replace n with ((n - m) + m) by ring. rewrite H.
 now rewrite Rplus_0_l.
 rewrite H; ring.
 Qed.
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 9e675165fa..a2b10ebaa3 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -26,20 +26,20 @@ Declare ML Module "micromega_plugin".
 
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
-  | Z => 
+  | Z =>
     (sos_Z || psatz_Z d) ;
-    intros __wit __varmap __ff ; 
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; 
+    intros __wit __varmap __ff ;
+    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
     apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | R =>
     (sos_R || psatz_R d) ;
-    intros __wit __varmap __ff ; 
-    change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; 
+    intros __wit __varmap __ff ;
+    change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
     apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | Q =>
       (sos_Q || psatz_Q d) ;
-    intros __wit __varmap __ff ; 
-    change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; 
+    intros __wit __varmap __ff ;
+    change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
     apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | _ => fail "Unsupported domain"
   end in tac.
@@ -52,27 +52,27 @@ Ltac psatzl dom :=
   | Z =>
     psatzl_Z ;
     intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; 
+    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
     apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | Q =>
-    psatzl_Q ; 
-    intros __wit __varmap __ff ; 
-    change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; 
+    psatzl_Q ;
+    intros __wit __varmap __ff ;
+    change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
     apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity
-  | R => 
+  | R =>
     psatzl_R ;
     intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; 
+    change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
     apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | _ => fail "Unsupported domain"
   end in tac.
 
 
 
-Ltac lia := 
+Ltac lia :=
   xlia ;
   intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; 
+    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
       apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
 
 
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index b266a1ab80..ae22b0c78c 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
@@ -80,7 +80,7 @@ Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q :=
   end.
 
 Lemma Qeval_expr_simpl : forall env e,
-  Qeval_expr env e = 
+  Qeval_expr env e =
   match e with
     | PEc c =>  c
     | PEX j =>  env j
@@ -179,7 +179,7 @@ Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
 Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
 
 Definition QTautoChecker (f : BFormula (Formula Q)) (w: list QWitness)  : bool :=
-  @tauto_checker (Formula Q) (NFormula Q) 
+  @tauto_checker (Formula Q) (NFormula Q)
   Qnormalise
   Qnegate QWitness QWeakChecker f w.
 
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 2e8c3daec0..21f991ef87 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -159,7 +159,7 @@ Definition Rnormalise := @cnf_normalise Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bo
 Definition Rnegate := @cnf_negate Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool.
 
 Definition RTautoChecker (f : BFormula (Formula Z)) (w: list RWitness)  : bool :=
-  @tauto_checker (Formula Z) (NFormula Z) 
+  @tauto_checker (Formula Z) (NFormula Z)
   Rnormalise Rnegate
   RWitness RWeakChecker f w.
 
diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v
index 801d8b2122..c86fe8fb64 100644
--- a/plugins/micromega/Refl.v
+++ b/plugins/micromega/Refl.v
@@ -107,7 +107,7 @@ Proof.
 Qed.
 
 Lemma not_make_conj_app : forall (A:Type) (t:list A) a eval
-  (no_middle_eval : forall d, eval d \/ ~ eval d) , 
+  (no_middle_eval : forall d, eval d \/ ~ eval d) ,
   ~ make_conj  eval (t ++ a) -> (~ make_conj  eval t) \/ (~ make_conj eval a).
 Proof.
   induction t.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 88b53583d5..d556cd03e9 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -170,10 +170,10 @@ let (p, op) := f in eval_op1 op (eval_pol env p).
 Definition OpMult (o o' : Op1) : option Op1 :=
 match o with
 | Equal => Some Equal
-| NonStrict => 
+| NonStrict =>
   match o' with
     | Equal => Some Equal
-    | NonEqual  => None 
+    | NonEqual  => None
     | Strict    => Some NonStrict
     | NonStrict => Some NonStrict
   end
@@ -203,20 +203,20 @@ Definition OpAdd (o o': Op1) : option Op1 :=
                 end
     | NonEqual => match o' with
                     | Equal  => Some NonEqual
-                    | _      => None   
+                    | _      => None
                   end
   end.
 
 
 Lemma OpMult_sound :
-  forall (o o' om: Op1) (x y : R), 
+  forall (o o' om: Op1) (x y : R),
     eval_op1 o x -> eval_op1 o' y -> OpMult o o' = Some om -> eval_op1 om (x * y).
 Proof.
 unfold eval_op1; destruct o; simpl; intros o' om x y H1 H2 H3.
 (* x == 0 *)
 inversion H3. rewrite H1. now rewrite (Rtimes_0_l sor).
 (* x ~= 0 *)
-destruct o' ; inversion H3.  
+destruct o' ; inversion H3.
  (* y == 0 *)
  rewrite H2. now rewrite (Rtimes_0_r sor).
  (* y ~= 0 *)
@@ -240,7 +240,7 @@ destruct o' ; inversion H3.
 Qed.
 
 Lemma OpAdd_sound :
-  forall (o o' oa : Op1) (e e' : R), 
+  forall (o o' oa : Op1) (e e' : R),
     eval_op1 o e -> eval_op1 o' e' -> OpAdd o o' = Some oa -> eval_op1 oa (e + e').
 Proof.
 unfold eval_op1; destruct o; simpl; intros o' oa e e' H1 H2 Hoa.
@@ -298,7 +298,7 @@ Inductive Psatz : Type :=
 (** Given a list [l] of NFormula and an extended polynomial expression
    [e], if [eval_Psatz l e] succeeds (= Some f) then [f] is a
    logic consequence of the conjunction of the formulae in l.
-   Moreover, the polynomial expression is obtained by replacing the (PsatzIn n) 
+   Moreover, the polynomial expression is obtained by replacing the (PsatzIn n)
    by the nth polynomial expression in [l] and the sign is computed by the "rule of sign" *)
 
 (* Might be defined elsewhere *)
@@ -310,12 +310,12 @@ Definition map_option (A B:Type) (f : A -> option B) (o : option A) : option B :
 
 Implicit Arguments map_option [A B].
 
-Definition map_option2 (A B C : Type) (f : A -> B -> option C) 
-  (o: option A) (o': option B) : option C := 
-  match o , o' with 
-    | None , _ => None 
-    | _ , None => None 
-    | Some x , Some x' => f x x' 
+Definition map_option2 (A B C : Type) (f : A -> B -> option C)
+  (o: option A) (o': option B) : option C :=
+  match o , o' with
+    | None , _ => None
+    | _ , None => None
+    | Some x , Some x' => f x x'
   end.
 
 Implicit Arguments map_option2 [A B C].
@@ -344,51 +344,51 @@ Definition nformula_times_nformula (f1 f2 : NFormula) : option NFormula :=
 
 
 Fixpoint eval_Psatz (l : list NFormula) (e : Psatz) {struct e} : option NFormula :=
-  match e with 
+  match e with
     | PsatzIn n => Some (nth n l (Pc cO, Equal))
     | PsatzSquare e => Some (Psquare cO cI cplus ctimes ceqb e  , NonStrict)
     | PsatzMulC re e => map_option (pexpr_times_nformula re) (eval_Psatz l e)
     | PsatzMulE f1 f2 => map_option2 nformula_times_nformula  (eval_Psatz l f1) (eval_Psatz l f2)
     | PsatzAdd f1 f2  => map_option2 nformula_plus_nformula  (eval_Psatz l f1) (eval_Psatz l f2)
-    | PsatzC  c  => if cltb cO c then Some (Pc c, Strict) else None 
+    | PsatzC  c  => if cltb cO c then Some (Pc c, Strict) else None
 (* This could be 0, or <> 0 -- but these cases are useless *)
     | PsatzZ     => Some (Pc cO, Equal) (* Just to make life easier *)
   end.
 
 Lemma pexpr_times_nformula_correct : forall (env: PolEnv) (e: PolC) (f f' : NFormula),
-  eval_nformula env f -> pexpr_times_nformula e f = Some f' -> 
+  eval_nformula env f -> pexpr_times_nformula e f = Some f' ->
    eval_nformula env f'.
 Proof.
   unfold pexpr_times_nformula.
   destruct f.
   intros. destruct o ; inversion H0 ; try discriminate.
-  simpl in *.    unfold eval_pol in *.   
-  rewrite (Pmul_ok sor.(SORsetoid) Rops_wd 
+  simpl in *.    unfold eval_pol in *.
+  rewrite (Pmul_ok sor.(SORsetoid) Rops_wd
     (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))  addon.(SORrm)).
   rewrite H. apply (Rtimes_0_r sor).
 Qed.
-  
+
 Lemma nformula_times_nformula_correct : forall (env:PolEnv)
-  (f1 f2 f : NFormula), 
-  eval_nformula env f1 -> eval_nformula env f2 -> 
-  nformula_times_nformula f1 f2 = Some f  -> 
+  (f1 f2 f : NFormula),
+  eval_nformula env f1 -> eval_nformula env f2 ->
+  nformula_times_nformula f1 f2 = Some f  ->
    eval_nformula env f.
 Proof.
   unfold nformula_times_nformula.
   destruct f1 ; destruct f2.
   case_eq (OpMult o o0) ; simpl ; try discriminate.
   intros. inversion H2 ; simpl.
-  unfold eval_pol. 
+  unfold eval_pol.
   destruct o1; simpl;
-  rewrite (Pmul_ok sor.(SORsetoid) Rops_wd 
+  rewrite (Pmul_ok sor.(SORsetoid) Rops_wd
     (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))  addon.(SORrm));
   apply OpMult_sound with (3:= H);assumption.
 Qed.
 
 Lemma nformula_plus_nformula_correct : forall (env:PolEnv)
-  (f1 f2 f : NFormula), 
-  eval_nformula env f1 -> eval_nformula env f2 -> 
-  nformula_plus_nformula f1 f2 = Some f  -> 
+  (f1 f2 f : NFormula),
+  eval_nformula env f1 -> eval_nformula env f2 ->
+  nformula_plus_nformula f1 f2 = Some f  ->
    eval_nformula env f.
 Proof.
   unfold nformula_plus_nformula.
@@ -397,15 +397,15 @@ Proof.
   intros. inversion H2 ; simpl.
   unfold eval_pol.
   destruct o1; simpl;
-  rewrite (Padd_ok sor.(SORsetoid) Rops_wd 
+  rewrite (Padd_ok sor.(SORsetoid) Rops_wd
     (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))  addon.(SORrm));
   apply OpAdd_sound with (3:= H);assumption.
 Qed.
 
-Lemma eval_Psatz_Sound : 
+Lemma eval_Psatz_Sound :
   forall (l : list NFormula) (env : PolEnv),
     (forall (f : NFormula), In f l -> eval_nformula env f) ->
-      forall (e : Psatz) (f : NFormula), eval_Psatz l e = Some f -> 
+      forall (e : Psatz) (f : NFormula), eval_Psatz l e = Some f ->
         eval_nformula env f.
 Proof.
   induction e.
@@ -416,17 +416,17 @@ Proof.
   apply H ; congruence.
   (* index is out-of-bounds *)
   inversion H0.
-  rewrite e. simpl.  
+  rewrite e. simpl.
   now apply  addon.(SORrm).(morph0).
   (* PsatzSquare *)
   simpl. intros. inversion H0.
   simpl. unfold eval_pol.
-  rewrite (Psquare_ok sor.(SORsetoid) Rops_wd 
+  rewrite (Psquare_ok sor.(SORsetoid) Rops_wd
     (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))  addon.(SORrm));
   now apply (Rtimes_square_nonneg sor).
   (* PsatzMulC *)
   simpl.
-  intro. 
+  intro.
   case_eq  (eval_Psatz l e) ; simpl ; intros.
   apply IHe in H0.
   apply pexpr_times_nformula_correct with (1:=H0) (2:= H1).
@@ -441,7 +441,7 @@ Proof.
   (* PsatzAdd *)
   simpl ; intro.
   case_eq (eval_Psatz l e1) ; simpl ; try discriminate.
-  case_eq (eval_Psatz l e2) ; simpl ; try discriminate.  
+  case_eq (eval_Psatz l e2) ; simpl ; try discriminate.
   intros.
   apply IHe1 in H1. apply IHe2 in H0.
   apply (nformula_plus_nformula_correct env n0 n) ; assumption.
@@ -457,14 +457,14 @@ Proof.
 Qed.
 
 Fixpoint ge_bool (n m  : nat) : bool :=
- match n with 
-   | O   => match m with 
+ match n with
+   | O   => match m with
             |  O => true
             | S _ => false
           end
-   | S n  => match m with 
+   | S n  => match m with
                | O => true
-               | S m => ge_bool n m 
+               | S m => ge_bool n m
              end
    end.
 
@@ -483,7 +483,7 @@ Qed.
 
 
 Fixpoint xhyps_of_psatz (base:nat) (acc : list nat) (prf : Psatz)  : list nat :=
-  match prf with 
+  match prf with
     | PsatzC _ | PsatzZ | PsatzSquare _ => acc
     | PsatzMulC _ prf => xhyps_of_psatz base acc prf
     | PsatzAdd e1 e2 | PsatzMulE e1 e2 => xhyps_of_psatz base (xhyps_of_psatz base acc e2) e1
@@ -495,7 +495,7 @@ Fixpoint xhyps_of_psatz (base:nat) (acc : list nat) (prf : Psatz)  : list nat :=
   forall env p, eval_pexpr env p == eval_pol env (normalise_pexpr p) *)
 
 (*****)
-Definition paddC := PaddC cplus. 
+Definition paddC := PaddC cplus.
 Definition psubC := PsubC cminus.
 
 Definition PsubC_ok : forall c P env, eval_pol env (psubC  P c) == eval_pol env P - [c] :=
@@ -536,7 +536,7 @@ Lemma check_inconsistent_sound :
     check_inconsistent (p, op) = true -> forall env, ~ eval_op1 op (eval_pol env p).
 Proof.
 intros p op H1 env. unfold check_inconsistent in H1.
-destruct op; simpl ; 
+destruct op; simpl ;
 (*****)
 destruct p ; simpl; try discriminate H1;
 try rewrite <- addon.(SORrm).(morph0); trivial.
@@ -547,7 +547,7 @@ apply cltb_sound in H1. now apply -> (Rlt_nge sor).
 Qed.
 
 Definition check_normalised_formulas : list NFormula -> Psatz -> bool :=
-  fun l cm => 
+  fun l cm =>
     match eval_Psatz l cm with
       | None => false
       | Some f => check_inconsistent f
@@ -640,14 +640,14 @@ let (lhs, op, rhs) := f in
 Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub  lhs rhs) == eval_pol env lhs - eval_pol env rhs.
 Proof.
   intros.
-  apply (Psub_ok  sor.(SORsetoid) Rops_wd 
+  apply (Psub_ok  sor.(SORsetoid) Rops_wd
     (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
 Qed.
 
 Lemma eval_pol_add : forall env lhs rhs, eval_pol env (padd  lhs rhs) == eval_pol env lhs + eval_pol env rhs.
 Proof.
   intros.
-  apply (Padd_ok  sor.(SORsetoid) Rops_wd 
+  apply (Padd_ok  sor.(SORsetoid) Rops_wd
     (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
 Qed.
 
@@ -656,7 +656,7 @@ Proof.
   intros.
   apply  (norm_aux_spec sor.(SORsetoid) Rops_wd   (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm) addon.(SORpower) ).
 Qed.
-  
+
 
 Theorem normalise_sound :
   forall (env : PolEnv) (f : Formula),
@@ -694,7 +694,7 @@ Definition xnormalise (t:Formula) : list (NFormula)  :=
   let lhs := norm lhs in
     let rhs := norm rhs in
     match o with
-      | OpEq => 
+      | OpEq =>
         (psub lhs  rhs, Strict)::(psub rhs lhs , Strict)::nil
       | OpNEq => (psub lhs rhs,Equal) :: nil
       | OpGt   => (psub rhs lhs,NonStrict) :: nil
@@ -716,7 +716,7 @@ Proof.
   unfold cnf_normalise, xnormalise ; simpl ; intros env t.
   unfold eval_cnf.
   destruct t as [lhs o rhs]; case_eq o ; simpl;
-    repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ; 
+    repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ;
     generalize (eval_pexpr  env lhs);
       generalize (eval_pexpr  env rhs) ; intros z1 z2 ; intros.
   (**)
@@ -751,7 +751,7 @@ Proof.
   unfold cnf_negate, xnegate ; simpl ; intros env t.
   unfold eval_cnf.
   destruct t as [lhs o rhs]; case_eq o ; simpl;
-    repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ; 
+    repeat rewrite eval_pol_sub ; repeat rewrite <- eval_pol_norm in * ;
     generalize (eval_pexpr  env lhs);
       generalize (eval_pexpr  env rhs) ; intros z1 z2 ; intros ; intuition.
   (**)
@@ -774,7 +774,7 @@ Proof.
   intros.
   destruct d ; simpl.
   generalize (eval_pol env p); intros.
-  destruct o ; simpl. 
+  destruct o ; simpl.
   apply (Req_em sor r 0).
   destruct (Req_em sor r 0) ; tauto.
   rewrite <- (Rle_ngt sor r 0). generalize (Rle_gt_cases sor r 0). tauto.
@@ -787,7 +787,7 @@ Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C :=
   match p with
     | Pc c => PEc c
     | Pinj j p => xdenorm  (Pplus j jmp ) p
-    | PX p j q   => PEadd 
+    | PX p j q   => PEadd
       (PEmul (xdenorm jmp p) (PEpow (PEX _  jmp) (Npos j)))
       (xdenorm (Psucc jmp) q)
   end.
@@ -802,7 +802,7 @@ Proof.
   intros.
   rewrite Pplus_succ_permute_r.
   rewrite <- IHp.
-  symmetry. 
+  symmetry.
   rewrite Pplus_comm.
   rewrite Pjump_Pplus. reflexivity.
   (* PX *)
@@ -821,7 +821,7 @@ Proof.
 Qed.
 
 Definition denorm (p : Pol C)  := xdenorm xH p.
-  
+
 Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p).
 Proof.
   unfold denorm.
@@ -836,25 +836,25 @@ Proof.
   unfold Env.tail.
   rewrite xdenorm_correct.
   change (Psucc xH) with 2%positive.
-  rewrite addon.(SORpower).(rpow_pow_N).  
+  rewrite addon.(SORpower).(rpow_pow_N).
   simpl. reflexivity.
 Qed.
-  
+
 
 (** Some syntactic simplifications of expressions  *)
 
 
 Definition simpl_cone (e:Psatz) : Psatz :=
   match e with
-    | PsatzSquare t => 
+    | PsatzSquare t =>
                     match t with
                       | Pc c   => if ceqb cO c then PsatzZ else PsatzC (ctimes c c)
                       | _ => PsatzSquare t
                     end
-    | PsatzMulE t1 t2 => 
+    | PsatzMulE t1 t2 =>
       match t1 , t2 with
-        | PsatzZ      , x        => PsatzZ 
-        |    x     , PsatzZ      => PsatzZ 
+        | PsatzZ      , x        => PsatzZ
+        |    x     , PsatzZ      => PsatzZ
         | PsatzC c ,  PsatzC c' => PsatzC (ctimes c c')
         | PsatzC p1 , PsatzMulE (PsatzC p2)  x => PsatzMulE (PsatzC (ctimes p1 p2)) x
         | PsatzC p1 , PsatzMulE x (PsatzC p2)  => PsatzMulE (PsatzC (ctimes p1 p2)) x
@@ -865,7 +865,7 @@ Definition simpl_cone (e:Psatz) : Psatz :=
         | _ ,  PsatzC c        => if ceqb cI c then t1 else PsatzMulE t1 t2
         |     _     , _   => e
       end
-    | PsatzAdd t1 t2 => 
+    | PsatzAdd t1 t2 =>
       match t1 ,  t2 with
         | PsatzZ     , x => x
         |   x     , PsatzZ => x
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 42e0acb582..b1d0217685 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -20,14 +20,14 @@ Set Implicit Arguments.
 
 
   Inductive BFormula (A:Type) : Type :=
-  | TT   : BFormula A 
+  | TT   : BFormula A
   | FF   : BFormula A
   | X : Prop -> BFormula A
-  | A : A -> BFormula A 
+  | A : A -> BFormula A
   | Cj  : BFormula A -> BFormula A -> BFormula A
   | D   : BFormula A-> BFormula A -> BFormula A
   | N  : BFormula A -> BFormula A
-  | I : BFormula A-> BFormula A-> BFormula A. 
+  | I : BFormula A-> BFormula A-> BFormula A.
 
   Fixpoint eval_f (A:Type)  (ev:A -> Prop ) (f:BFormula A) {struct f}: Prop :=
     match f with
@@ -42,7 +42,7 @@ Set Implicit Arguments.
     end.
 
 
-  Lemma map_simpl : forall A B f l, @map A B f l = match l with 
+  Lemma map_simpl : forall A B f l, @map A B f l = match l with
                                                  | nil => nil
                                                  | a :: l=> (f a) :: (@map A B f l)
                                                end.
@@ -57,7 +57,7 @@ Set Implicit Arguments.
     Variable Env   : Type.
     Variable Term  : Type.
     Variable eval  : Env -> Term -> Prop.
-    Variable Term' : Type.  
+    Variable Term' : Type.
     Variable eval'  : Env -> Term' -> Prop.
 
 
@@ -78,17 +78,17 @@ Set Implicit Arguments.
 
     Definition or_clause_cnf (t:clause) (f:cnf) : cnf :=
       List.map (fun x => (t++x)) f.
-    
+
     Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf :=
       match f with
         | nil => tt
         | e :: rst => (or_cnf rst f') ++ (or_clause_cnf e f')
       end.
-    
+
 
     Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf :=
       f1 ++ f2.
-    
+
     Fixpoint xcnf (pol : bool) (f : BFormula Term)  {struct f}: cnf :=
       match f with
         | TT => if pol then tt else ff
@@ -96,14 +96,14 @@ Set Implicit Arguments.
         | X p => if pol then ff else ff (* This is not complete - cannot negate any proposition *)
         | A x => if pol then normalise x else negate x
         | N e  => xcnf (negb pol) e
-        | Cj e1 e2 => 
+        | Cj e1 e2 =>
           (if pol then and_cnf else or_cnf) (xcnf pol e1) (xcnf pol e2)
         | D e1 e2  => (if pol then or_cnf else and_cnf) (xcnf pol e1) (xcnf pol e2)
         | I e1 e2 => (if pol then or_cnf else and_cnf) (xcnf (negb pol) e1) (xcnf pol e2)
       end.
 
   Definition eval_cnf (env : Term' -> Prop) (f:cnf) := make_conj  (fun cl => ~ make_conj  env cl) f.
-  
+
 
   Lemma eval_cnf_app : forall env x y, eval_cnf (eval' env) (x++y) -> eval_cnf (eval' env) x /\ eval_cnf (eval' env) y.
   Proof.
@@ -111,7 +111,7 @@ Set Implicit Arguments.
     intros.
     rewrite make_conj_app in H ; auto.
   Qed.
-    
+
 
   Lemma or_clause_correct : forall env t f, eval_cnf (eval' env) (or_clause_cnf t f) -> (~ make_conj  (eval' env) t) \/ (eval_cnf (eval' env) f).
   Proof.
@@ -258,8 +258,8 @@ Set Implicit Arguments.
     unfold and_cnf in H.
     simpl in H.
     destruct (eval_cnf_app _ _ _ H).
-    generalize (IHf1 _ _ H0).    
-    generalize (IHf2 _ _ H1).    
+    generalize (IHf1 _ _ H0).
+    generalize (IHf2 _ _ H1).
     simpl.
     tauto.
   Qed.
@@ -267,13 +267,13 @@ Set Implicit Arguments.
 
   Variable Witness : Type.
   Variable checker : list Term' -> Witness -> bool.
-  
+
   Variable checker_sound : forall t  w, checker t w = true -> forall env, make_impl (eval' env)  t False.
 
   Fixpoint cnf_checker (f : cnf) (l : list Witness)  {struct f}: bool :=
     match f with
       | nil => true
-      | e::f => match l with 
+      | e::f => match l with
                   | nil => false
                   | c::l => match checker e c with
                               | true => cnf_checker f l
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index ed204d92b6..c0b86f5ed3 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -17,21 +17,21 @@ Require Import Coq.Arith.Max.
 Require Import List.
 Set Implicit Arguments.
 
-(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v) 
+(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v)
    -- this is harmless and spares a lot of Empty.
-   This means smaller proof-terms. 
+   This means smaller proof-terms.
    BTW, by dropping the  polymorphism, I get small (yet noticeable) speed-up.
 *)
 
 Section MakeVarMap.
   Variable A : Type.
   Variable default : A.
-  
+
   Inductive t  : Type :=
-  | Empty : t 
-  | Leaf : A -> t 
+  | Empty : t
+  | Leaf : A -> t
   | Node : t  -> A -> t  -> t .
-  
+
   Fixpoint find   (vm : t ) (p:positive) {struct vm} : A :=
     match vm with
       | Empty => default
@@ -49,7 +49,7 @@ Section MakeVarMap.
 
 
 
-  Definition jump  (j:positive) (l:off_map ) := 
+  Definition jump  (j:positive) (l:off_map ) :=
     let (o,m) := l in
       match o with
         | None => (Some j,m)
@@ -74,7 +74,7 @@ Section MakeVarMap.
   Lemma psucc : forall p,  (match p with
                               | xI y' => xO (Psucc y')
                               | xO y' => xI y'
-                              | 1%positive => 2%positive 
+                              | 1%positive => 2%positive
                             end) = (p+1)%positive.
   Proof.
     destruct p.
@@ -84,7 +84,7 @@ Section MakeVarMap.
     reflexivity.
   Qed.
 
-  Lemma jump_Pplus : forall i j l, 
+  Lemma jump_Pplus : forall i j l,
     (jump (i + j) l) = (jump i (jump j l)).
   Proof.
     unfold jump.
@@ -96,7 +96,7 @@ Section MakeVarMap.
   Qed.
 
   Lemma jump_simpl : forall p l,
-    jump p l = 
+    jump p l =
     match p with
       | xH => tail l
       | xO p => jump p (jump p l)
@@ -116,15 +116,15 @@ Section MakeVarMap.
   Qed.
 
   Ltac jump_s :=
-    repeat 
+    repeat
       match goal with
         | |- context [jump xH ?e] => rewrite (jump_simpl xH)
         | |- context [jump (xO ?p) ?e] => rewrite (jump_simpl (xO p))
         | |- context [jump (xI ?p) ?e] => rewrite (jump_simpl (xI p))
       end.
-    
+
   Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l).
-  Proof. 
+  Proof.
     unfold tail.
     intros.
     repeat rewrite <- jump_Pplus.
@@ -132,7 +132,7 @@ Section MakeVarMap.
     reflexivity.
   Qed.
 
-  Lemma jump_Psucc : forall j l, 
+  Lemma jump_Psucc : forall j l,
     (jump (Psucc j) l) = (jump 1 (jump j l)).
   Proof.
     intros.
@@ -162,14 +162,14 @@ Section MakeVarMap.
     reflexivity.
   Qed.
 
-  
-  Lemma nth_spec : forall p l, 
-    nth p l = 
+
+  Lemma nth_spec : forall p l,
+    nth p l =
     match p with
       | xH => hd  l
       | xO p => nth p (jump p l)
       | xI p => nth p (jump p (tail l))
-    end. 
+    end.
   Proof.
     unfold nth.
     destruct l.
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index ced67e39d0..f27cd15e3b 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -56,7 +56,7 @@ Proof.
   destruct sor.(SORsetoid).
   apply Equivalence_Transitive.
 Qed.
-  
+
 
 Add Relation R req
   reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 70eb2331c7..b02a9850eb 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -33,7 +33,7 @@ Ltac inv H := inversion H ; try subst ; clear H.
 Require Import EnvRing.
 
 Open Scope Z_scope.
-  
+
 Lemma Zsor : SOR 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt.
 Proof.
   constructor ; intros ; subst ; try (intuition (auto  with zarith)).
@@ -100,7 +100,7 @@ match o with
 | OpGt => Zgt
 end.
 
-Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):=   
+Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):=
   let (lhs, op, rhs) := f in
     (Zeval_op2 op) (Zeval_expr env lhs) (Zeval_expr env rhs).
 
@@ -109,16 +109,16 @@ Definition Zeval_formula' :=
 
 Lemma Zeval_formula_compat : forall env f, Zeval_formula env f <-> Zeval_formula' env f.
 Proof.
-  destruct f ; simpl. 
+  destruct f ; simpl.
   rewrite Zeval_expr_compat. rewrite Zeval_expr_compat.
   unfold eval_expr.
-  generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) 
+  generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x)
         (fun x : N => x) (pow_N 1 Zmult) env Flhs).
-  generalize ((eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x) 
+  generalize ((eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x)
         (fun x : N => x) (pow_N 1 Zmult) env Frhs)).
   destruct Fop ; simpl; intros ; intuition (auto with zarith).
 Qed.
-  
+
 
 Definition eval_nformula :=
   eval_nformula 0 Zplus Zmult  (@eq Z) Zle Zlt (fun x => x) .
@@ -131,7 +131,7 @@ match o with
 | NonStrict => fun x : Z => 0 <= x
 end.
 
-  
+
 Lemma Zeval_nformula_dec : forall env d, (eval_nformula env d) \/ ~ (eval_nformula env d).
 Proof.
   intros.
@@ -179,13 +179,13 @@ Proof.
   intros.
   apply (eval_pol_norm Zsor ZSORaddon).
 Qed.
-  
+
 Definition xnormalise (t:Formula Z) : list (NFormula Z)  :=
   let (lhs,o,rhs) := t in
     let lhs := norm lhs in
       let rhs := norm rhs in
     match o with
-      | OpEq => 
+      | OpEq =>
         ((psub lhs (padd  rhs (Pc 1))),NonStrict)::((psub rhs (padd lhs (Pc 1))),NonStrict)::nil
       | OpNEq => (psub lhs rhs,Equal) :: nil
       | OpGt   => (psub rhs lhs,NonStrict) :: nil
@@ -218,7 +218,7 @@ Proof.
     intuition (auto with zarith).
   Transparent padd.
 Qed.
-  
+
 Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z)  :=
   let (lhs,o,rhs) := t in
     let lhs := norm lhs in
@@ -331,11 +331,11 @@ Definition makeLbCut (v:PExprC Z) (q:Q) : NFormula Z :=
 Definition neg_nformula (f : NFormula Z) :=
   let (e,o) := f in
     (PEopp (PEadd e (PEc 1%Z)), o).
-    
+
 Lemma neg_nformula_sound : forall env f, snd f = NonStrict ->( ~ (Zeval_nformula env (neg_nformula f)) <-> Zeval_nformula env f).
 Proof.
   unfold neg_nformula.
-  destruct f. 
+  destruct f.
   simpl.
   intros ; subst ; simpl in *.
   split;  auto with zarith.
@@ -346,9 +346,9 @@ Qed.
    - b is the constant
    - a is the gcd of the other coefficient.
 *)
-Require Import Znumtheory. 
+Require Import Znumtheory.
 
-Definition isZ0 (x:Z) := 
+Definition isZ0 (x:Z) :=
   match x with
     | Z0 => true
     | _  => false
@@ -371,7 +371,7 @@ Fixpoint Zgcd_pol (p : PolC Z) : (Z * Z) :=
   match p with
     | Pc c => (0,c)
     | Pinj _ p => Zgcd_pol p
-    | PX p _ q => 
+    | PX p _ q =>
       let (g1,c1) := Zgcd_pol p in
         let (g2,c2) := Zgcd_pol q in
           (ZgcdM (ZgcdM g1 c1) g2 , c2)
@@ -393,7 +393,7 @@ Inductive Zdivide_pol (x:Z): PolC Z -> Prop :=
 | Zdiv_PX   : forall p q, Zdivide_pol x p -> Zdivide_pol x q -> forall j, Zdivide_pol x (PX p j q).
 
 
-Lemma Zdiv_pol_correct : forall a p, 0 < a -> Zdivide_pol a p  -> 
+Lemma Zdiv_pol_correct : forall a p, 0 < a -> Zdivide_pol a p  ->
   forall env, eval_pol env p =  a * eval_pol env (Zdiv_pol p a).
 Proof.
   intros until 2.
@@ -441,7 +441,7 @@ Proof.
   constructor. auto.
   constructor ; auto.
 Qed.
-  
+
 Lemma Zdivide_pol_one : forall p, Zdivide_pol 1 p.
 Proof.
   induction p ; constructor ; auto.
@@ -458,15 +458,15 @@ Proof.
   rewrite <- Hq, Hb, Ha. ring.
 Qed.
 
-Lemma Zdivide_pol_sub : forall p a b, 
-  0 < Zgcd a b -> 
-  Zdivide_pol a (PsubC Zminus p b) -> 
+Lemma Zdivide_pol_sub : forall p a b,
+  0 < Zgcd a b ->
+  Zdivide_pol a (PsubC Zminus p b) ->
    Zdivide_pol (Zgcd a b) p.
 Proof.
   induction p.
   simpl.
   intros. inversion H0.
-  constructor. 
+  constructor.
   apply Zgcd_minus ; auto.
   intros.
   constructor.
@@ -480,8 +480,8 @@ Proof.
   apply IHp2 ; assumption.
 Qed.
 
-Lemma Zdivide_pol_sub_0 : forall p a, 
-  Zdivide_pol a (PsubC Zminus p 0) -> 
+Lemma Zdivide_pol_sub_0 : forall p a,
+  Zdivide_pol a (PsubC Zminus p 0) ->
    Zdivide_pol a p.
 Proof.
   induction p.
@@ -499,7 +499,7 @@ Proof.
 Qed.
 
 
-Lemma Zgcd_pol_div : forall p g c, 
+Lemma Zgcd_pol_div : forall p g c,
   Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Zminus p c).
 Proof.
   induction p ; simpl.
@@ -541,7 +541,7 @@ Proof.
 Qed.
 
 
-  
+
 
 Lemma Zgcd_pol_correct_lt : forall p env g c, Zgcd_pol p = (g,c) -> 0 < g -> eval_pol env p = g * (eval_pol env (Zdiv_pol (PsubC Zminus p c) g))  + c.
 Proof.
@@ -555,9 +555,9 @@ Qed.
 
 
 
-Definition makeCuttingPlane (p : PolC Z) : PolC  Z * Z := 
+Definition makeCuttingPlane (p : PolC Z) : PolC  Z * Z :=
   let (g,c) := Zgcd_pol p in
-    if Zgt_bool g Z0 
+    if Zgt_bool g Z0
       then (Zdiv_pol (PsubC Zminus p c) g , Zopp (ceiling (Zopp c) g))
       else (p,Z0).
 
@@ -594,7 +594,7 @@ Proof.
   destruct z ; try discriminate.
   reflexivity.
 Qed.
-  
+
 
 
 
@@ -609,37 +609,37 @@ Definition check_inconsistent := check_inconsistent 0 Zeq_bool Zle_bool.
 
 Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof)  {struct pf} : bool :=
   match pf with
-    | DoneProof => false 
-    | RatProof w pf => 
+    | DoneProof => false
+    | RatProof w pf =>
       match eval_Psatz l w  with
         | None => false
-        | Some f => 
+        | Some f =>
           if check_inconsistent f then true
             else ZChecker (f::l) pf
       end
-    | CutProof w pf => 
+    | CutProof w pf =>
       match eval_Psatz l w with
         | None => false
-        | Some f => 
+        | Some f =>
           match genCuttingPlane f with
             | None => true
             | Some cp => ZChecker (nformula_of_cutting_plane cp::l) pf
           end
       end
-    | EnumProof w1 w2 pf => 
+    | EnumProof w1 w2 pf =>
       match eval_Psatz l w1 , eval_Psatz l w2 with
-        |  Some f1 , Some f2 => 
+        |  Some f1 , Some f2 =>
           match genCuttingPlane f1 , genCuttingPlane f2 with
-            |Some (e1,z1,op1) , Some (e2,z2,op2) => 
+            |Some (e1,z1,op1) , Some (e2,z2,op2) =>
               match op1 , op2 with
-                | NonStrict , NonStrict => 
+                | NonStrict , NonStrict =>
                   if is_pol_Z0 (padd e1 e2)
                     then
                       (fix label (pfs:list ZArithProof) :=
-                        fun lb ub => 
+                        fun lb ub =>
                           match pfs with
                             | nil => if Zgt_bool lb ub then true else false
-                            | pf::rsr => andb (ZChecker  ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub) 
+                            | pf::rsr => andb (ZChecker  ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub)
                           end)
                       pf (Zopp z1)  z2
                     else false
@@ -693,18 +693,18 @@ Proof.
 Qed.
 
 
-Lemma eval_Psatz_sound : forall env w l f', 
-  make_conj (eval_nformula env) l -> 
+Lemma eval_Psatz_sound : forall env w l f',
+  make_conj (eval_nformula env) l ->
   eval_Psatz l w  = Some f' ->  eval_nformula env f'.
 Proof.
   intros.
   apply (eval_Psatz_Sound Zsor ZSORaddon) with (l:=l) (e:= w) ; auto.
-  apply make_conj_in ; auto.  
+  apply make_conj_in ; auto.
 Qed.
 
-Lemma makeCuttingPlane_sound : forall env e e' c, 
-  eval_nformula env (e, NonStrict) -> 
-  makeCuttingPlane e = (e',c) -> 
+Lemma makeCuttingPlane_sound : forall env e e' c,
+  eval_nformula env (e, NonStrict) ->
+  makeCuttingPlane e = (e',c) ->
   eval_nformula env (nformula_of_cutting_plane (e', c, NonStrict)).
 Proof.
   unfold nformula_of_cutting_plane.
@@ -728,10 +728,10 @@ Proof.
   (* g <= 0 *)
   intros. inv H2. auto with zarith.
 Qed.
-  
 
-Lemma cutting_plane_sound : forall env f p, 
-  eval_nformula env f -> 
+
+Lemma cutting_plane_sound : forall env f p,
+  eval_nformula env f ->
   genCuttingPlane f = Some p ->
    eval_nformula env (nformula_of_cutting_plane p).
 Proof.
@@ -758,25 +758,25 @@ Proof.
   rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
   simpl. auto with zarith.
   (* Strict *)
-  destruct p as [[e' z] op].  
+  destruct p as [[e' z] op].
   case_eq (makeCuttingPlane (PsubC Zminus e 1)).
   intros.
   inv H1.
   apply makeCuttingPlane_sound with (env:=env) (2:= H).
   simpl in *.
-  rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).  
+  rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).
   auto with zarith.
   (* NonStrict *)
-  destruct p as [[e' z] op].  
+  destruct p as [[e' z] op].
   case_eq (makeCuttingPlane e).
   intros.
   inv H1.
   apply makeCuttingPlane_sound with (env:=env) (2:= H).
   assumption.
-Qed.  
+Qed.
 
-Lemma  genCuttingPlaneNone : forall env f, 
-  genCuttingPlane f = None -> 
+Lemma  genCuttingPlaneNone : forall env f,
+  genCuttingPlane f = None ->
   eval_nformula env f -> False.
 Proof.
   unfold genCuttingPlane.
@@ -784,7 +784,7 @@ Proof.
   destruct o.
   case_eq (Zgcd_pol p) ; intros g c.
   case_eq (Zgt_bool g 0 && (Zgt_bool c 0 && negb (Zeq_bool (Zgcd g c) g))).
-  intros. 
+  intros.
   flatten_bool.
   rewrite negb_true_iff in H5.
   apply Zeq_bool_neq in H5.
@@ -805,7 +805,7 @@ Proof.
   destruct (makeCuttingPlane p) ; discriminate.
 Qed.
 
-  
+
 Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl  (eval_nformula env)  l False.
 Proof.
   induction w    using (well_founded_ind (well_founded_ltof _ bdepth)).
@@ -815,7 +815,7 @@ Proof.
   (* RatProof *)
   simpl.
   intro l. case_eq (eval_Psatz l w) ; [| discriminate].
-  intros f Hf. 
+  intros f Hf.
   case_eq (check_inconsistent f).
   intros.
   apply (checker_nf_sound Zsor ZSORaddon l w).
@@ -831,7 +831,7 @@ Proof.
   rewrite <- make_conj_impl in H2.
   rewrite make_conj_cons in H2.
   rewrite <- make_conj_impl.
-  intro. 
+  intro.
   apply H2.
   split ; auto.
   apply eval_Psatz_sound with (2:= Hf) ; assumption.
@@ -840,7 +840,7 @@ Proof.
   intro l.
   case_eq (eval_Psatz l w) ; [ | discriminate].
   intros f' Hlc.
-  case_eq (genCuttingPlane f'). 
+  case_eq (genCuttingPlane f').
   intros.
   assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False).
    eapply (H pf) ; auto.
@@ -850,7 +850,7 @@ Proof.
   rewrite <- make_conj_impl in H2.
   rewrite make_conj_cons in H2.
   rewrite <- make_conj_impl.
-  intro. 
+  intro.
   apply H2.
   split ; auto.
   apply eval_Psatz_sound with (env:=env) in Hlc.
@@ -887,7 +887,7 @@ Proof.
    unfold RingMicromega.eval_nformula in H4.
    change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in H4.
    unfold eval_op1 in H4.
-   rewrite eval_pol_add in H4. simpl in H4. 
+   rewrite eval_pol_add in H4. simpl in H4.
    auto with zarith.
    (**)
    apply is_pol_Z0_eval_pol with (env := env) in H0.
@@ -900,7 +900,7 @@ Proof.
    unfold RingMicromega.eval_nformula in H3.
    change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in H3.
    unfold eval_op1 in H3.
-   rewrite eval_pol_add in H3. simpl in H3. 
+   rewrite eval_pol_add in H3. simpl in H3.
    omega.
   revert H5.
   set (FF := (fix label (pfs : list ZArithProof) (lb ub : Z) {struct pfs} : bool :=
@@ -911,7 +911,7 @@ Proof.
           label rsr (lb + 1)%Z ub)%bool
     end)).
   intros.
-  assert (HH :forall x, -z1 <= x <= z2 -> exists pr, 
+  assert (HH :forall x, -z1 <= x <= z2 -> exists pr,
     (In pr pf /\
       ZChecker  ((PsubC Zminus p1 x,Equal) :: l) pr = true)%Z).
   clear H.
@@ -972,7 +972,7 @@ Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof)  : list nat :=
     | DoneProof => acc
     | RatProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt
     | CutProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt
-    | EnumProof c1 c2 l => 
+    | EnumProof c1 c2 l =>
       let acc := xhyps_of_psatz base (xhyps_of_psatz base acc c2) c1 in
         List.fold_left (xhyps_of_pt (S base)) l acc
   end.
@@ -989,7 +989,7 @@ Definition hyps_of_pt (pt : ZArithProof) : list nat := xhyps_of_pt 0 nil pt.
 
 Open Scope Z_scope.
 
-  
+
 (** To ease bindings from ml code **)
 (*Definition varmap := Quote.varmap.*)
 Definition make_impl := Refl.make_impl.
@@ -1019,5 +1019,5 @@ Definition n_of_Z (z:Z) : BinNat.N :=
 (* Local Variables: *)
 (* coding: utf-8 *)
 (* End: *)
- 
+
 
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 2a1c2fe225..c5760229c5 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)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 5e13db1b69..d10ae00c82 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -15,12 +15,12 @@
 open Mutils
 let debug = false
 
-let time str f x = 
+let time str f x =
  let t0 = (Unix.times()).Unix.tms_utime in
- let res = f x in 
- let t1 = (Unix.times()).Unix.tms_utime in 
-  (*if debug then*) (Printf.printf "time %s %f\n" str (t1 -. t0) ; 
-		     flush stdout); 
+ let res = f x in
+ let t1 = (Unix.times()).Unix.tms_utime in
+  (*if debug then*) (Printf.printf "time %s %f\n" str (t1 -. t0) ;
+		     flush stdout);
   res
 
 
@@ -28,30 +28,30 @@ type tag = Tag.t
 type 'cst atom = 'cst Micromega.formula
 
 type 'cst formula =
-  | TT 
-  | FF 
+  | TT
+  | FF
   | X of Term.constr
   | A of 'cst atom * tag * Term.constr
-  | C of 'cst  formula * 'cst formula 
-  | D of 'cst formula * 'cst formula 
-  | N of 'cst formula 
-  | I of 'cst formula * Names.identifier option * 'cst formula 
+  | C of 'cst  formula * 'cst formula
+  | D of 'cst formula * 'cst formula
+  | N of 'cst formula
+  | I of 'cst formula * Names.identifier option * 'cst formula
 
 
-let rec pp_formula o f = 
+let rec pp_formula o f =
   match f with
     | TT -> output_string  o "tt"
     | FF -> output_string  o "ff"
-    | X c -> output_string o "X " 
+    | X c -> output_string o "X "
     | A(_,t,_) -> Printf.fprintf o "A(%a)" Tag.pp t
     | C(f1,f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2
     | D(f1,f2) -> Printf.fprintf o "D(%a,%a)" pp_formula f1 pp_formula f2
-    | I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)" 
-	pp_formula f1 
-	  (match n with 
-	    | Some id -> Names.string_of_id id 
+    | I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)"
+	pp_formula f1
+	  (match n with
+	    | Some id -> Names.string_of_id id
 	    | None -> "") pp_formula f2
-    | N(f) -> Printf.fprintf o "N(%a)" pp_formula f 
+    | N(f) -> Printf.fprintf o "N(%a)" pp_formula f
 
 let rec ids_of_formula f =
   match f with
@@ -60,15 +60,15 @@ let rec ids_of_formula f =
 
 module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end)
 
-let selecti s m = 
-  let rec xselect i m = 
+let selecti s m =
+  let rec xselect i m =
     match m with
       | [] -> []
       | e::m -> if ISet.mem i s then e:: (xselect (i+1) m) else xselect (i+1) m in
     xselect 0 m
 
 
-type 'cst clause = ('cst Micromega.nFormula * tag) list 
+type 'cst clause = ('cst Micromega.nFormula * tag) list
 
 type 'cst cnf = ('cst clause) list
 
@@ -78,7 +78,7 @@ let ff : 'cst cnf = [ [] ]
 
 type 'cst mc_cnf = ('cst Micromega.nFormula) list list
 
-let cnf (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) (f:'cst formula) = 
+let cnf (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) (f:'cst formula) =
  let negate a t =
   List.map (fun cl -> List.map (fun x -> (x,t)) cl) (negate a) in
 
@@ -88,12 +88,12 @@ let cnf (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf)
  let and_cnf x y = x @ y in
 
  let or_clause_cnf t f =  List.map (fun x -> t@x) f in
-  
+
  let rec or_cnf f f'  =
   match f with
    | [] -> tt
    | e :: rst -> (or_cnf rst f') @ (or_clause_cnf e f') in
-  
+
  let rec xcnf  (pol : bool) f    =
   match f with
    | TT -> if pol then tt else ff (* ?? *)
@@ -101,11 +101,11 @@ let cnf (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf)
    | X p -> if pol then ff else ff (* ?? *)
    | A(x,t,_) -> if pol then normalise  x t else negate x t
    | N(e)  -> xcnf  (not pol) e
-   | C(e1,e2) -> 
+   | C(e1,e2) ->
       (if pol then and_cnf else or_cnf) (xcnf  pol e1) (xcnf  pol e2)
-   | D(e1,e2)  -> 
+   | D(e1,e2)  ->
       (if pol then or_cnf else and_cnf) (xcnf  pol e1) (xcnf  pol e2)
-   | I(e1,_,e2) -> 
+   | I(e1,_,e2) ->
       (if pol then or_cnf else and_cnf) (xcnf  (not pol) e1) (xcnf  pol e2) in
 
   xcnf  true f
@@ -116,12 +116,12 @@ struct
  open Coqlib
  open Term
   (*    let constant = gen_constant_in_modules "Omicron" coq_modules*)
-  
-  
+
+
  let logic_dir = ["Coq";"Logic";"Decidable"]
  let coq_modules =
-  init_modules @ 
-   [logic_dir] @ arith_modules @ zarith_base_modules @ 
+  init_modules @
+   [logic_dir] @ arith_modules @ zarith_base_modules @
    [ ["Coq";"Lists";"List"];
      ["ZMicromega"];
      ["Tauto"];
@@ -135,7 +135,7 @@ struct
      ["Coq";"Reals" ; "Rdefinitions"];
      ["Coq";"Reals" ; "Rpow_def"];
      ["LRing_normalise"]]
-   
+
  let constant = gen_constant_in_modules "ZMicromega" coq_modules
 
  let coq_and = lazy (constant "and")
@@ -144,7 +144,7 @@ struct
  let coq_iff = lazy (constant "iff")
  let coq_True = lazy (constant "True")
  let coq_False = lazy (constant "False")
-  
+
  let coq_cons = lazy (constant "cons")
  let coq_nil = lazy (constant "nil")
  let coq_list = lazy (constant "list")
@@ -153,9 +153,9 @@ struct
  let coq_S = lazy (constant "S")
  let coq_nat = lazy (constant "nat")
 
- let coq_NO = lazy 
+ let coq_NO = lazy
   (gen_constant_in_modules "N" [ ["Coq";"NArith";"BinNat" ]]  "N0")
- let coq_Npos = lazy 
+ let coq_Npos = lazy
   (gen_constant_in_modules "N" [ ["Coq";"NArith"; "BinNat"]]  "Npos")
   (* let coq_n = lazy (constant "N")*)
 
@@ -166,7 +166,7 @@ struct
  let coq_xH = lazy (constant "xH")
  let coq_xO = lazy (constant "xO")
  let coq_xI = lazy (constant "xI")
-  
+
  let coq_N0 = lazy (constant "N0")
  let coq_N0 = lazy (constant "Npos")
 
@@ -179,11 +179,11 @@ struct
  let coq_POS = lazy (constant  "Zpos")
  let coq_NEG = lazy (constant  "Zneg")
 
- let coq_QWitness = lazy 
-  (gen_constant_in_modules "QMicromega" 
+ let coq_QWitness = lazy
+  (gen_constant_in_modules "QMicromega"
     [["Coq"; "micromega"; "QMicromega"]] "QWitness")
- let coq_ZWitness = lazy 
-  (gen_constant_in_modules "QMicromega" 
+ let coq_ZWitness = lazy
+  (gen_constant_in_modules "QMicromega"
     [["Coq"; "micromega"; "ZMicromega"]] "ZWitness")
 
 
@@ -212,8 +212,8 @@ struct
  let coq_Zopp = lazy (constant "Zopp")
  let coq_Zmult = lazy (constant "Zmult")
  let coq_Zpower = lazy (constant "Zpower")
- let coq_N_of_Z = lazy 
-  (gen_constant_in_modules "ZArithRing" 
+ let coq_N_of_Z = lazy
+  (gen_constant_in_modules "ZArithRing"
     [["Coq";"setoid_ring";"ZArithRing"]] "N_of_Z")
 
  let coq_Qgt = lazy (constant "Qgt")
@@ -271,27 +271,27 @@ struct
  let coq_PsatzC  = lazy (constant "PsatzC")
  let coq_PsatzZ    = lazy (constant "PsatzZ")
  let coq_coneMember    = lazy (constant "coneMember")
-  
 
- let coq_make_impl = lazy 
+
+ let coq_make_impl = lazy
   (gen_constant_in_modules "Zmicromega" [["Refl"]] "make_impl")
- let coq_make_conj = lazy 
+ let coq_make_conj = lazy
   (gen_constant_in_modules "Zmicromega" [["Refl"]] "make_conj")
 
- let coq_Build = lazy 
-  (gen_constant_in_modules "RingMicromega" 
-    [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] 
+ let coq_Build = lazy
+  (gen_constant_in_modules "RingMicromega"
+    [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ]
     "Build_Formula")
- let coq_Cstr = lazy 
-  (gen_constant_in_modules "RingMicromega" 
+ let coq_Cstr = lazy
+  (gen_constant_in_modules "RingMicromega"
     [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] "Formula")
 
 
- type parse_error  = 
-   | Ukn 
-   | BadStr of string 
-   | BadNum of int 
-   | BadTerm of Term.constr 
+ type parse_error  =
+   | Ukn
+   | BadStr of string
+   | BadNum of int
+   | BadTerm of Term.constr
    | Msg   of string
    | Goal of (Term.constr list ) * Term.constr * parse_error
 
@@ -304,73 +304,73 @@ struct
   | Goal _    -> "Goal"
 
 
- exception ParseError 
+ exception ParseError
 
 
 
 
- let get_left_construct term = 
+ let get_left_construct term =
   match Term.kind_of_term term with
    | Term.Construct(_,i) -> (i,[| |])
-   | Term.App(l,rst) -> 
+   | Term.App(l,rst) ->
       (match Term.kind_of_term l with
        | Term.Construct(_,i) -> (i,rst)
        |   _     -> raise ParseError
       )
    | _ ->   raise ParseError
-      
+
  module Mc = Micromega
-      
- let rec parse_nat term = 
+
+ let rec parse_nat term =
   let (i,c) = get_left_construct term in
    match i with
     | 1 -> Mc.O
     | 2 -> Mc.S (parse_nat (c.(0)))
     | i -> raise ParseError
-       
+
 
  let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n)
 
 
- let rec dump_nat x = 
+ let rec dump_nat x =
   match x with
    | Mc.O -> Lazy.force coq_O
    | Mc.S p -> Term.mkApp(Lazy.force coq_S,[| dump_nat p |])
 
 
- let rec parse_positive term = 
+ let rec parse_positive term =
   let (i,c) = get_left_construct term in
    match i with
     | 1 -> Mc.XI (parse_positive c.(0))
     | 2 -> Mc.XO (parse_positive c.(0))
     | 3 -> Mc.XH
     | i -> raise ParseError
-       
 
- let rec dump_positive x = 
+
+ let rec dump_positive x =
   match x with
    | Mc.XH -> Lazy.force coq_xH
    | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_positive p |])
    | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_positive p |])
 
- let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x)	  
+ let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x)
 
 
- let rec dump_n x = 
-  match x with 
+ let rec dump_n x =
+  match x with
    | Mc.N0 -> Lazy.force coq_N0
    | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|])
 
- let rec dump_index x = 
+ let rec dump_index x =
   match x with
    | Mc.XH -> Lazy.force coq_xH
    | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_index p |])
    | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_index p |])
 
 
- let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x)	  
+ let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x)
 
- let rec dump_n x = 
+ let rec dump_n x =
   match x with
    | Mc.N0 -> Lazy.force coq_NO
    | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p |])
@@ -392,30 +392,30 @@ struct
  let dump_z x =
   match x with
    | Mc.Z0 ->Lazy.force coq_ZERO
-   | Mc.Zpos p -> Term.mkApp(Lazy.force coq_POS,[| dump_positive p|]) 
-   | Mc.Zneg p -> Term.mkApp(Lazy.force coq_NEG,[| dump_positive p|])  
+   | Mc.Zpos p -> Term.mkApp(Lazy.force coq_POS,[| dump_positive p|])
+   | Mc.Zneg p -> Term.mkApp(Lazy.force coq_NEG,[| dump_positive p|])
 
  let pp_z o x = Printf.fprintf o "%i" (CoqToCaml.z x)
 
-let dump_num bd1 = 
+let dump_num bd1 =
  Term.mkApp(Lazy.force coq_Qmake,
-	   [|dump_z (CamlToCoq.bigint (numerator bd1)) ; 
+	   [|dump_z (CamlToCoq.bigint (numerator bd1)) ;
 	     dump_positive (CamlToCoq.positive_big_int (denominator bd1)) |])
 
 
-let dump_q q = 
- Term.mkApp(Lazy.force coq_Qmake, 
+let dump_q q =
+ Term.mkApp(Lazy.force coq_Qmake,
 	   [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|])
 
-let parse_q term =  
+let parse_q term =
  match Term.kind_of_term term with
   | Term.App(c, args) -> if c = Lazy.force coq_Qmake then
 	{Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
       else raise ParseError
   |  _ -> raise ParseError
 
-  
- let rec parse_list parse_elt term = 
+
+ let rec parse_list parse_elt term =
   let (i,c) = get_left_construct term in
    match i with
     | 1 -> []
@@ -430,20 +430,20 @@ let parse_q term =
 			       [| typ; dump_elt e;dump_list typ dump_elt l|])
 
 
- let pp_list op cl elt o l = 
-  let rec _pp  o l = 
+ let pp_list op cl elt o l =
+  let rec _pp  o l =
    match l with
     | [] -> ()
     | [e] -> Printf.fprintf o "%a" elt e
     | e::l -> Printf.fprintf o "%a ,%a" elt e  _pp l in
-   Printf.fprintf o "%s%a%s" op _pp l cl 
+   Printf.fprintf o "%s%a%s" op _pp l cl
 
 
  let pp_var  = pp_positive
  let dump_var = dump_positive
 
- let pp_expr pp_z o e = 
- let rec pp_expr  o e = 
+ let pp_expr pp_z o e =
+ let rec pp_expr  o e =
   match e with
    | Mc.PEX n -> Printf.fprintf o "V %a" pp_var n
    | Mc.PEc z -> pp_z o z
@@ -474,62 +474,62 @@ let parse_q term =
    dump_expr e
 
 
- let dump_pol typ dump_c e = 
-   let rec dump_pol e = 
-     match e with 
+ let dump_pol typ dump_c e =
+   let rec dump_pol e =
+     match e with
        | Mc.Pc n -> mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|])
        | Mc.Pinj(p,pol) -> mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|])
        | Mc.PX(pol1,p,pol2) -> mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in
      dump_pol e
 
- let pp_pol pp_c o e = 
-   let rec pp_pol o e = 
-     match e with 
+ let pp_pol pp_c o e =
+   let rec pp_pol o e =
+     match e with
        | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n
        | Mc.Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol
        | Mc.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in
      pp_pol o e
-     
-   
- let pp_cnf pp_c o f = 
+
+
+ let pp_cnf pp_c o f =
    let pp_clause o l = List.iter (fun ((p,_),t) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c)  p Tag.pp t) l in
      List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause l) f
 
-	   
- let dump_psatz typ dump_z e = 
-  let z = Lazy.force typ in 
+
+ let dump_psatz typ dump_z e =
+  let z = Lazy.force typ in
  let rec dump_cone e =
   match e with
    | Mc.PsatzIn n -> mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |])
-   | Mc.PsatzMulC(e,c) -> mkApp(Lazy.force coq_PsatzMultC, 
+   | Mc.PsatzMulC(e,c) -> mkApp(Lazy.force coq_PsatzMultC,
 			     [| z; dump_pol z dump_z e ; dump_cone c |])
-   | Mc.PsatzSquare e -> mkApp(Lazy.force coq_PsatzSquare, 
+   | Mc.PsatzSquare e -> mkApp(Lazy.force coq_PsatzSquare,
 			   [| z;dump_pol z dump_z e|])
    | Mc.PsatzAdd(e1,e2) -> mkApp(Lazy.force coq_PsatzAdd,
 			     [| z; dump_cone e1; dump_cone e2|])
    | Mc.PsatzMulE(e1,e2) -> mkApp(Lazy.force coq_PsatzMulE,
 			      [| z; dump_cone e1; dump_cone e2|])
    | Mc.PsatzC p -> mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|])
-   | Mc.PsatzZ    -> mkApp( Lazy.force coq_PsatzZ,[| z|]) in 
+   | Mc.PsatzZ    -> mkApp( Lazy.force coq_PsatzZ,[| z|]) in
   dump_cone e
 
 
- let  pp_psatz pp_z o e = 
-  let rec pp_cone o e = 
-   match e with 
-    | Mc.PsatzIn n -> 
+ let  pp_psatz pp_z o e =
+  let rec pp_cone o e =
+   match e with
+    | Mc.PsatzIn n ->
        Printf.fprintf o "(In %a)%%nat" pp_nat n
-    | Mc.PsatzMulC(e,c) -> 
+    | Mc.PsatzMulC(e,c) ->
        Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c
-    | Mc.PsatzSquare e -> 
+    | Mc.PsatzSquare e ->
        Printf.fprintf o "(%a^2)" (pp_pol pp_z) e
-    | Mc.PsatzAdd(e1,e2) -> 
+    | Mc.PsatzAdd(e1,e2) ->
        Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2
-    | Mc.PsatzMulE(e1,e2) -> 
+    | Mc.PsatzMulE(e1,e2) ->
        Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2
-    | Mc.PsatzC p -> 
+    | Mc.PsatzC p ->
        Printf.fprintf o "(%a)%%positive" pp_z p
-    | Mc.PsatzZ    -> 
+    | Mc.PsatzZ    ->
        Printf.fprintf o "0" in
    pp_cone o e
 
@@ -544,8 +544,8 @@ let parse_q term =
 
 
 
- let pp_op o e= 
-  match e with 
+ let pp_op o e=
+  match e with
    | Mc.OpEq-> Printf.fprintf o "="
    | Mc.OpNEq-> Printf.fprintf o "<>"
    | Mc.OpLe -> Printf.fprintf o "=<"
@@ -561,29 +561,29 @@ let parse_q term =
 
  let dump_cstr typ dump_constant {Mc.flhs = e1 ; Mc.fop = o ; Mc.frhs = e2} =
    Term.mkApp(Lazy.force coq_Build,
-	     [| typ; dump_expr typ dump_constant e1 ; 
-		dump_op o ; 
+	     [| typ; dump_expr typ dump_constant e1 ;
+		dump_op o ;
 		dump_expr typ dump_constant e2|])
 
- let assoc_const x l = 
-  try 
+ let assoc_const x l =
+  try
   snd (List.find (fun (x',y) -> x = Lazy.force x') l)
   with
     Not_found -> raise ParseError
 
- let zop_table = [ 
-  coq_Zgt, Mc.OpGt ; 
+ let zop_table = [
+  coq_Zgt, Mc.OpGt ;
   coq_Zge, Mc.OpGe ;
   coq_Zlt, Mc.OpLt ;
   coq_Zle, Mc.OpLe ]
 
- let rop_table = [ 
-  coq_Rgt, Mc.OpGt ; 
+ let rop_table = [
+  coq_Rgt, Mc.OpGt ;
   coq_Rge, Mc.OpGe ;
   coq_Rlt, Mc.OpLt ;
   coq_Rle, Mc.OpLe ]
 
- let qop_table = [ 
+ let qop_table = [
   coq_Qlt, Mc.OpLt ;
   coq_Qle, Mc.OpLe ;
   coq_Qeq, Mc.OpEq
@@ -593,7 +593,7 @@ let parse_q term =
  let parse_zop (op,args) =
   match kind_of_term op with
    | Const x -> (assoc_const op zop_table, args.(0) , args.(1))
-   |  Ind(n,0) -> 
+   |  Ind(n,0) ->
        if op = Lazy.force coq_Eq &&   args.(0) = Lazy.force coq_Z
        then (Mc.OpEq, args.(1), args.(2))
        else raise ParseError
@@ -603,7 +603,7 @@ let parse_q term =
  let parse_rop (op,args) =
    match kind_of_term op with
     | Const x -> (assoc_const op rop_table, args.(0) , args.(1))
-    |  Ind(n,0) -> 
+    |  Ind(n,0) ->
        if op = Lazy.force coq_Eq &&   args.(0) = Lazy.force coq_R
        then (Mc.OpEq, args.(1), args.(2))
        else raise ParseError
@@ -614,25 +614,25 @@ let parse_q term =
 
 
  module Env =
- struct 
+ struct
   type t = constr list
-    
+
   let compute_rank_add env v =
    let rec _add env n v =
     match env with
      | [] -> ([v],n)
-     | e::l -> 
-	if eq_constr e v 
+     | e::l ->
+	if eq_constr e v
 	then (env,n)
-	else 
+	else
 	 let (env,n) = _add l ( n+1) v in
 	  (e::env,n) in
    let (env, n) =  _add env 1 v in
     (env, CamlToCoq.idx n)
 
-     
+
   let empty = []
-   
+
   let elements env = env
 
  end
@@ -640,63 +640,63 @@ let parse_q term =
 
  let is_constant t = (* This is an approx *)
   match kind_of_term t with
-   | Construct(i,_) -> true 
+   | Construct(i,_) -> true
    |   _ -> false
 
 
- type 'a op = 
-   | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) 
-   | Opp 
-   | Power 
+ type 'a op =
+   | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr)
+   | Opp
+   | Power
    | Ukn of string
 
 
- let assoc_ops x l = 
-  try 
+ let assoc_ops x l =
+  try
     snd (List.find (fun (x',y) -> x = Lazy.force x') l)
   with
     Not_found -> Ukn "Oups"
 
 
 
- let parse_expr parse_constant parse_exp ops_spec env term = 
- if debug 
- then (Pp.pp (Pp.str "parse_expr: ");   
+ let parse_expr parse_constant parse_exp ops_spec env term =
+ if debug
+ then (Pp.pp (Pp.str "parse_expr: ");
        Pp.pp_flush ();Pp.pp (Printer.prterm  term); Pp.pp_flush ());
 
-  let constant_or_variable env term = 
-   try 
+  let constant_or_variable env term =
+   try
     ( Mc.PEc (parse_constant term) , env)
-   with ParseError -> 
+   with ParseError ->
     let (env,n) = Env.compute_rank_add env term in
      (Mc.PEX  n , env) in
 
-  let rec parse_expr env term = 
+  let rec parse_expr env term =
    let combine env op (t1,t2) =
     let (expr1,env) = parse_expr env t1 in
     let (expr2,env) = parse_expr env t2 in
     (op expr1 expr2,env) in
 
     match kind_of_term term with
-     | App(t,args) -> 
+     | App(t,args) ->
 	(
 	 match kind_of_term t with
-	  | Const c -> 
+	  | Const c ->
 	     ( match assoc_ops t ops_spec  with
 	      | Binop f -> combine env f (args.(0),args.(1))
 	      | Opp     -> let (expr,env) = parse_expr env args.(0) in
 			    (Mc.PEopp expr, env)
-	      | Power   -> 
+	      | Power   ->
 		  begin
-		    try 
+		    try
 		      let (expr,env) = parse_expr env args.(0) in
-		      let exp = (parse_exp args.(1)) in 
-			(Mc.PEpow(expr, exp)  , env) 
+		      let exp = (parse_exp args.(1)) in
+			(Mc.PEpow(expr, exp)  , env)
 		    with _ ->   (* if the exponent is a variable *)
 		      let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
 		  end
-	      | Ukn  s -> 
-		 if debug 
+	      | Ukn  s ->
+		 if debug
 		 then (Printf.printf "unknown op: %s\n" s; flush stdout;);
 		 let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
 	     )
@@ -704,47 +704,47 @@ let parse_q term =
 	)
      | _ -> constant_or_variable env term in
    parse_expr env term
-    
 
- let zop_spec = 
-   [ 
+
+ let zop_spec =
+   [
      coq_Zplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
      coq_Zminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
-     coq_Zmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ; 
-     coq_Zopp   , Opp ; 
+     coq_Zmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ;
+     coq_Zopp   , Opp ;
      coq_Zpower , Power]
 
-let qop_spec = 
+let qop_spec =
   [
      coq_Qplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
      coq_Qminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
-     coq_Qmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ; 
-     coq_Qopp   , Opp ; 
+     coq_Qmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ;
+     coq_Qopp   , Opp ;
      coq_Qpower , Power]
 
-let rop_spec = 
+let rop_spec =
   [
      coq_Rplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
      coq_Rminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
-     coq_Rmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ; 
-     coq_Ropp   , Opp ; 
+     coq_Rmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ;
+     coq_Ropp   , Opp ;
      coq_Rpower , Power]
 
 
 
 
-      
+
 let zconstant = parse_z
 let qconstant = parse_q
 
 
-let rconstant term = 
- if debug 
+let rconstant term =
+ if debug
  then (Pp.pp_flush ();
        Pp.pp (Pp.str "rconstant: ");
        Pp.pp (Printer.prterm  term); Pp.pp_flush ());
  match Term.kind_of_term term with
-  | Const x ->  
+  | Const x ->
       if term = Lazy.force coq_R0
       then Mc.Z0
       else if term = Lazy.force coq_R1
@@ -753,37 +753,37 @@ let rconstant term =
   |  _ -> raise ParseError
 
 
-let parse_zexpr = 
- parse_expr zconstant (fun x -> Mc.n_of_Z (parse_z x))  zop_spec 
-let parse_qexpr  = 
- parse_expr qconstant (fun x -> Mc.n_of_Z (parse_z x)) qop_spec 
-let parse_rexpr = 
+let parse_zexpr =
+ parse_expr zconstant (fun x -> Mc.n_of_Z (parse_z x))  zop_spec
+let parse_qexpr  =
+ parse_expr qconstant (fun x -> Mc.n_of_Z (parse_z x)) qop_spec
+let parse_rexpr =
  parse_expr rconstant  (fun x -> Mc.n_of_nat (parse_nat x)) rop_spec
 
 
- let  parse_arith parse_op parse_expr env cstr = 
-  if debug 
+ let  parse_arith parse_op parse_expr env cstr =
+  if debug
   then (Pp.pp_flush ();
 	Pp.pp (Pp.str "parse_arith: ");
-	Pp.pp (Printer.prterm  cstr); 
+	Pp.pp (Printer.prterm  cstr);
 	Pp.pp_flush ());
   match kind_of_term cstr with
-   | App(op,args) -> 
+   | App(op,args) ->
       let (op,lhs,rhs) = parse_op (op,args) in
       let (e1,env) = parse_expr env lhs in
       let (e2,env) = parse_expr env rhs in
        ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env)
    |  _ -> failwith "error : parse_arith(2)"
 
- let parse_zarith = parse_arith  parse_zop parse_zexpr 
-  
+ let parse_zarith = parse_arith  parse_zop parse_zexpr
+
  let parse_qarith = parse_arith  parse_qop parse_qexpr
-  
+
  let parse_rarith = parse_arith  parse_rop parse_rexpr
-  
-  
+
+
  (* generic parsing of arithmetic expressions *)
-  
+
 
 
 
@@ -797,7 +797,7 @@ let parse_rexpr =
   | N (a) -> Mc.N(f2f a)
   | I(a,_,b)  -> Mc.I(f2f a,f2f b)
 
- let is_prop t = 
+ let is_prop t =
   match t with
    | Names.Anonymous -> true (* Not quite right *)
    | Names.Name x    -> false
@@ -814,7 +814,7 @@ let parse_rexpr =
 
  let parse_formula parse_atom env term =
 
-  let parse_atom env tg t = try let (at,env) = parse_atom env t in 
+  let parse_atom env tg t = try let (at,env) = parse_atom env t in
 				  (A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in
 
   let rec xparse_formula env tg term =
@@ -845,36 +845,36 @@ let parse_rexpr =
     | _  -> X(term),env,tg in
   xparse_formula env term
 
- let coq_TT = lazy 
-  (gen_constant_in_modules "ZMicromega" 
+ let coq_TT = lazy
+  (gen_constant_in_modules "ZMicromega"
     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "TT")
- let coq_FF = lazy 
-  (gen_constant_in_modules "ZMicromega" 
+ let coq_FF = lazy
+  (gen_constant_in_modules "ZMicromega"
     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "FF")
- let coq_And = lazy 
-  (gen_constant_in_modules "ZMicromega"    
+ let coq_And = lazy
+  (gen_constant_in_modules "ZMicromega"
     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "Cj")
- let coq_Or = lazy 
-  (gen_constant_in_modules "ZMicromega"  
+ let coq_Or = lazy
+  (gen_constant_in_modules "ZMicromega"
     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]    "D")
- let coq_Neg = lazy 
-  (gen_constant_in_modules "ZMicromega" 
+ let coq_Neg = lazy
+  (gen_constant_in_modules "ZMicromega"
     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "N")
- let coq_Atom = lazy 
-  (gen_constant_in_modules "ZMicromega" 
+ let coq_Atom = lazy
+  (gen_constant_in_modules "ZMicromega"
     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "A")
- let coq_X = lazy 
-  (gen_constant_in_modules "ZMicromega"  
+ let coq_X = lazy
+  (gen_constant_in_modules "ZMicromega"
     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "X")
- let coq_Impl = lazy 
-  (gen_constant_in_modules "ZMicromega" 
+ let coq_Impl = lazy
+  (gen_constant_in_modules "ZMicromega"
     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "I")
- let coq_Formula = lazy 
-  (gen_constant_in_modules "ZMicromega" 
+ let coq_Formula = lazy
+  (gen_constant_in_modules "ZMicromega"
     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "BFormula")
 
- let dump_formula typ dump_atom f = 
-  let rec xdump f = 
+ let dump_formula typ dump_atom f =
+  let rec xdump f =
    match f with
     | TT  -> mkApp(Lazy.force coq_TT,[| typ|])
     | FF  -> mkApp(Lazy.force coq_FF,[| typ|])
@@ -882,11 +882,11 @@ let parse_rexpr =
     | D(x,y) -> mkApp(Lazy.force coq_Or,[| typ ; xdump x ; xdump y|])
     | I(x,_,y) -> mkApp(Lazy.force coq_Impl,[| typ ; xdump x ; xdump y|])
     | N(x) -> mkApp(Lazy.force coq_Neg,[| typ ; xdump x|])
-    | A(x,_,_) -> mkApp(Lazy.force coq_Atom,[| typ ; dump_atom x|]) 
+    | A(x,_,_) -> mkApp(Lazy.force coq_Atom,[| typ ; dump_atom x|])
     | X(t) -> mkApp(Lazy.force coq_X,[| typ ; t|])  in
 
    xdump f
-    
+
 
 
 
@@ -894,7 +894,7 @@ let parse_rexpr =
  let set l concl =
   let rec _set acc = function
    | [] -> acc
-   | (e::l) ->  
+   | (e::l) ->
       let (name,expr,typ) = e in
        _set (Term.mkNamedLetIn
 	      (Names.id_of_string name)
@@ -902,7 +902,7 @@ let parse_rexpr =
    _set concl l
 
 
-end            
+end
 
 open M
 
@@ -916,33 +916,33 @@ let rec sig_of_cone = function
  | _  -> []
 
 let same_proof sg cl1 cl2 =
- let rec xsame_proof sg = 
+ let rec xsame_proof sg =
   match sg with
    | [] -> true
-   | n::sg -> (try List.nth cl1 n = List.nth cl2 n with _ -> false) 
+   | n::sg -> (try List.nth cl1 n = List.nth cl2 n with _ -> false)
       && (xsame_proof sg ) in
   xsame_proof sg
 
 
 
 
-let tags_of_clause tgs wit clause = 
+let tags_of_clause tgs wit clause =
  let rec xtags tgs = function
-  | Mc.PsatzIn n -> Names.Idset.union tgs  
+  | Mc.PsatzIn n -> Names.Idset.union tgs
      (snd (List.nth clause (CoqToCaml.nat n) ))
   | Mc.PsatzMulC(e,w) -> xtags tgs w
   | Mc.PsatzMulE (w1,w2) | Mc.PsatzAdd(w1,w2) -> xtags (xtags tgs w1) w2
   |   _   -> tgs in
   xtags tgs wit
 
-let tags_of_cnf wits cnf = 
- List.fold_left2 (fun acc w cl -> tags_of_clause acc w cl) 
+let tags_of_cnf wits cnf =
+ List.fold_left2 (fun acc w cl -> tags_of_clause acc w cl)
   Names.Idset.empty wits cnf
 
 
 let find_witness prover polys1 = try_any prover polys1
 
-let rec witness prover   l1 l2 = 
+let rec witness prover   l1 l2 =
  match l2 with
   | [] -> Some []
   | e :: l2 ->
@@ -955,23 +955,23 @@ let rec witness prover   l1 l2 =
 	 )
 
 
-let rec apply_ids t ids = 
+let rec apply_ids t ids =
  match ids with
   | [] -> t
   | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
 
-     
-let coq_Node = lazy 
- (Coqlib.gen_constant_in_modules "VarMap" 
+
+let coq_Node = lazy
+ (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")
-let coq_Leaf = lazy 
- (Coqlib.gen_constant_in_modules "VarMap" 
+let coq_Leaf = lazy
+ (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")
-let coq_Empty = lazy 
- (Coqlib.gen_constant_in_modules "VarMap" 
+let coq_Empty = lazy
+ (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
- 
- 
+
+
 let btree_of_array typ a  =
  let size_of_a = Array.length a in
  let semi_size_of_a = size_of_a lsr 1 in
@@ -979,25 +979,25 @@ let btree_of_array typ a  =
  and leaf = Lazy.force coq_Leaf
  and empty = Term.mkApp (Lazy.force coq_Empty, [| typ |]) in
  let rec aux n =
-  if n > size_of_a 
+  if n > size_of_a
   then empty
-  else if  n > semi_size_of_a 
+  else if  n > semi_size_of_a
   then Term.mkApp (leaf, [| typ; a.(n-1) |])
   else Term.mkApp (node, [| typ; aux (2*n); a.(n-1); aux (2*n+1) |])
- in 
+ in
   aux 1
 
-let btree_of_array typ a = 
- try 
+let btree_of_array typ a =
+ try
   btree_of_array typ a
- with x -> 
+ with x ->
   failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x))
 
 let dump_varmap typ env =
  btree_of_array typ (Array.of_list env)
 
 
-let rec pp_varmap o vm = 
+let rec pp_varmap o vm =
  match vm with
   | Mc.Empty -> output_string o "[]"
   | Mc.Leaf z -> Printf.fprintf o "[%a]" pp_z  z
@@ -1005,37 +1005,37 @@ let rec pp_varmap o vm =
 
 
 
-let rec dump_proof_term = function 
+let rec dump_proof_term = function
   | Micromega.DoneProof -> Lazy.force coq_doneProof
-  | Micromega.RatProof(cone,rst) -> 
+  | Micromega.RatProof(cone,rst) ->
     Term.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|])
  | Micromega.CutProof(cone,prf) ->
-    Term.mkApp(Lazy.force coq_cutProof, 
-	      [| dump_psatz coq_Z dump_z cone ; 
+    Term.mkApp(Lazy.force coq_cutProof,
+	      [| dump_psatz coq_Z dump_z cone ;
 		 dump_proof_term prf|])
- | Micromega.EnumProof(c1,c2,prfs) -> 
+ | Micromega.EnumProof(c1,c2,prfs) ->
     Term.mkApp (Lazy.force coq_enumProof,
-	       [|  dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; 
+	       [|  dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ;
 		  dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |])
 
 let pp_q o q = Printf.fprintf o "%a/%a" pp_z q.Micromega.qnum pp_positive q.Micromega.qden
- 
- 
+
+
 let rec pp_proof_term o = function
   | Micromega.DoneProof -> Printf.fprintf o "D"
   | Micromega.RatProof(cone,rst) -> Printf.fprintf o "R[%a,%a]" (pp_psatz  pp_z) cone pp_proof_term rst
   | Micromega.CutProof(cone,rst) -> Printf.fprintf o "C[%a,%a]" (pp_psatz  pp_z) cone pp_proof_term rst
-  | Micromega.EnumProof(c1,c2,rst) -> 
-      Printf.fprintf o "EP[%a,%a,%a]" 
-	(pp_psatz pp_z) c1 (pp_psatz pp_z) c2 
+  | Micromega.EnumProof(c1,c2,rst) ->
+      Printf.fprintf o "EP[%a,%a,%a]"
+	(pp_psatz pp_z) c1 (pp_psatz pp_z) c2
      (pp_list "[" "]" pp_proof_term) rst
 
 let rec parse_hyps parse_arith env tg hyps =
  match hyps with
   | [] -> ([],env,tg)
-  | (i,t)::l -> 
+  | (i,t)::l ->
      let (lhyps,env,tg) = parse_hyps parse_arith env tg l in
-      try 
+      try
        let (c,env,tg) = parse_formula parse_arith env  tg t in
 	((i,c)::lhyps, env,tg)
       with _ -> 		(lhyps,env,tg)
@@ -1044,7 +1044,7 @@ let rec parse_hyps parse_arith env tg hyps =
 
 exception ParseError
 
-let parse_goal parse_arith env hyps term = 
+let parse_goal parse_arith env hyps term =
  (*  try*)
  let (f,env,tg) = parse_formula parse_arith env (Tag.from 0) term in
  let (lhyps,env,tg) = parse_hyps parse_arith env tg hyps in
@@ -1052,11 +1052,11 @@ let parse_goal parse_arith env hyps term =
    (*  with Failure x -> raise ParseError*)
 
 
-type ('d, 'prf) domain_spec = { 
+type ('d, 'prf) domain_spec = {
  typ : Term.constr; (* Z, Q , R *)
  coeff : Term.constr ; (* Z, Q *)
- dump_coeff : 'd -> Term.constr ; 
- proof_typ : Term.constr ; 
+ dump_coeff : 'd -> Term.constr ;
+ proof_typ : Term.constr ;
  dump_proof : 'prf -> Term.constr
 }
 
@@ -1085,25 +1085,25 @@ let rz_domain_spec = lazy {
 }
 
 
-let abstract_formula hyps f = 
-  
-  let rec xabs f = 
+let abstract_formula hyps f =
+
+  let rec xabs f =
     match f with
       | X c -> X c
       | A(a,t,term) -> if TagSet.mem t hyps then A(a,t,term) else X(term)
-      | C(f1,f2) -> 
+      | C(f1,f2) ->
 	  (match xabs f1 , xabs f2 with
 	    |   X a1    ,  X a2   -> X (Term.mkApp(Lazy.force coq_and, [|a1;a2|]))
 	    |    f1     , f2      -> C(f1,f2) )
-      | D(f1,f2) -> 
+      | D(f1,f2) ->
 	  (match xabs f1 , xabs f2 with
 	    |   X a1    ,  X a2   -> X (Term.mkApp(Lazy.force coq_or, [|a1;a2|]))
 	    |    f1     , f2      -> D(f1,f2) )
-      | N(f) -> 
+      | N(f) ->
 	  (match xabs f with
 	    |   X a    -> X (Term.mkApp(Lazy.force coq_not, [|a|]))
 	    |     f     -> N f)
-      | I(f1,hyp,f2) -> 
+      | I(f1,hyp,f2) ->
 	  (match xabs f1 , hyp, xabs f2 with
 	    | X a1      , Some _ , af2    ->  af2
 	    | X a1      , None   , X a2   -> X (Term.mkArrow a1 a2)
@@ -1117,25 +1117,25 @@ let abstract_formula hyps f =
 
 
 
-let micromega_order_change spec cert cert_typ env  ff gl = 
+let micromega_order_change spec cert cert_typ env  ff gl =
  let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[|  spec.coeff|])) in
 
  let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
  let vm  = dump_varmap  ( spec.typ)  env in
   Tactics.change_in_concl None
-   (set 
-     [ 
+   (set
+     [
       ("__ff", ff, Term.mkApp(Lazy.force coq_Formula ,[| formula_typ |]));
-      ("__varmap", vm , Term.mkApp 
-       (Coqlib.gen_constant_in_modules "VarMap" 
+      ("__varmap", vm , Term.mkApp
+       (Coqlib.gen_constant_in_modules "VarMap"
 	 [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "t", [|  spec.typ|]));
       ("__wit", cert,cert_typ)
-     ]  	
+     ]
      (Tacmach.pf_concl gl )
 
        )
-   gl 
-   
+   gl
+
 
 type ('a,'prf) prover = {
   name : string ; (* name of the prover *)
@@ -1147,18 +1147,18 @@ type ('a,'prf) prover = {
 }
 
 let find_witness provers    polys1 =
-  
-  let provers = List.map (fun p -> 
-    (fun l -> 
+
+  let provers = List.map (fun p ->
+    (fun l ->
       match p.prover l with
         | None -> None
         | Some prf -> Some(prf,p)) , p.name) provers in
-                           
+
     try_any provers (List.map fst polys1)
 
 
-let witness_list prover l = 
- let rec xwitness_list l = 
+let witness_list prover l =
+ let rec xwitness_list l =
   match l with
    | [] -> Some []
    | e :: l ->
@@ -1173,79 +1173,79 @@ let witness_list prover l =
 
 
 let witness_list_tags  = witness_list
- 
+
 let is_singleton = function [] -> true | [e] -> true | _ -> false
 
-let pp_ml_list pp_elt o l = 
+let pp_ml_list pp_elt o l =
   output_string o "[" ;
-  List.iter (fun x -> Printf.fprintf o "%a ;" pp_elt x) l ; 
-  output_string o "]" 
+  List.iter (fun x -> Printf.fprintf o "%a ;" pp_elt x) l ;
+  output_string o "]"
 
-let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = 
+let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
 
-  let compact_proof (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) = 
+  let compact_proof (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
     let new_cl = Mutils.mapi (fun (f,_) i -> (f,i)) new_cl in
-    let remap i = 
+    let remap i =
       let formula = try fst (List.nth old_cl i) with Failure _ -> failwith "bad old index" in
 	List.assoc formula new_cl in
 
-      if debug then 
+      if debug then
 	begin
-	  Printf.printf "\ncompact_proof : %a %a %a" 
-	    (pp_ml_list prover.pp_f) (List.map fst old_cl) 
-	    prover.pp_prf prf 
+	  Printf.printf "\ncompact_proof : %a %a %a"
+	    (pp_ml_list prover.pp_f) (List.map fst old_cl)
+	    prover.pp_prf prf
 	    (pp_ml_list prover.pp_f) (List.map fst new_cl)   ;
 	    flush stdout
 	end ;
       let res = try prover.compact prf remap with x ->
-	if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; 
+	if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
 	(* This should not happen -- this is the recovery plan... *)
-	match prover.prover (List.map fst new_cl) with 
+	match prover.prover (List.map fst new_cl) with
 	  | None -> failwith "proof compaction error"
-	  | Some p ->  p 
+	  | Some p ->  p
       in
-      if debug then 
+      if debug then
 	begin
-	  Printf.printf " -> %a\n" 
+	  Printf.printf " -> %a\n"
 	    prover.pp_prf res ;
 	  flush stdout
 	end
-	  ; 
+	  ;
       res in
 
 
 
-  let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) = 
+  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
 
   let cnf_res = List.combine cnf_ff res in (* we get pairs clause * proof *)
-    
-    List.map (fun x -> 
-      let (o,p) = List.find (fun (l,p) -> is_proof_compatible l p x) cnf_res 
-      in compact_proof o p x) cnf_ff' 
-    
-
-
-
-let micromega_tauto negate normalise spec prover env polys1 polys2  gl = 
- let spec = Lazy.force spec in 
- let (ff,ids) = 
-  List.fold_right 
-   (fun (id,f)  (cc,ids) -> 
-    match f with 
-      X _ -> (cc,ids) 
-     | _ -> (I(f,Some id,cc), id::ids)) 
+
+    List.map (fun x ->
+      let (o,p) = List.find (fun (l,p) -> is_proof_compatible l p x) cnf_res
+      in compact_proof o p x) cnf_ff'
+
+
+
+
+let micromega_tauto negate normalise spec prover env polys1 polys2  gl =
+ let spec = Lazy.force spec in
+ let (ff,ids) =
+  List.fold_right
+   (fun (id,f)  (cc,ids) ->
+    match f with
+      X _ -> (cc,ids)
+     | _ -> (I(f,Some id,cc), id::ids))
    polys1 (polys2,[]) in
 
  let cnf_ff = cnf negate normalise ff in
 
-  if debug then 
+  if debug then
     begin
       Pp.pp (Pp.str "Formula....\n") ;
       let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
-      let ff = dump_formula formula_typ 
+      let ff = dump_formula formula_typ
         (dump_cstr spec.typ spec.dump_coeff) ff in
         Pp.pp (Printer.prterm  ff) ;  Pp.pp_flush ();
 	  Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
@@ -1255,30 +1255,30 @@ let micromega_tauto negate normalise spec prover env polys1 polys2  gl =
     | None -> Tacticals.tclFAIL 0 (Pp.str "Cannot find witness") gl
     | Some res -> (*Printf.printf "\nList %i" (List.length `res); *)
 
-        let hyps = List.fold_left (fun s (cl,(prf,p)) -> 
+        let hyps = List.fold_left (fun s (cl,(prf,p)) ->
 	  let tags = ISet.fold (fun i s -> let t = snd (List.nth cl i) in
 					     if debug then (Printf.fprintf stdout "T : %i -> %a" i Tag.pp t) ;
 	    (*try*) TagSet.add t s (* with Invalid_argument _ -> s*)) (p.hyps prf) TagSet.empty in
 	  TagSet.union s tags) TagSet.empty (List.combine cnf_ff res) in
 
 	  if debug then (Printf.printf "TForm : %a\n" pp_formula ff ; flush stdout;
-			 Printf.printf "Hyps : %a\n" (fun o s -> TagSet.fold (fun i _ -> Printf.fprintf o "%a " Tag.pp i) s ()) hyps) ;  
-	  
+			 Printf.printf "Hyps : %a\n" (fun o s -> TagSet.fold (fun i _ -> Printf.fprintf o "%a " Tag.pp i) s ()) hyps) ;
+
         let ff'   = abstract_formula hyps ff in
-	  
+
         let cnf_ff' = cnf negate normalise ff' in
 
 	  if debug then
 	    begin
-	      Pp.pp (Pp.str "\nAFormula\n") ; 
+	      Pp.pp (Pp.str "\nAFormula\n") ;
 	      let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
-	      let ff' = dump_formula formula_typ 
+	      let ff' = dump_formula formula_typ
 		(dump_cstr spec.typ spec.dump_coeff) ff' in
 		Pp.pp (Printer.prterm  ff') ;  Pp.pp_flush ();
 		Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
 	    end;
 
-   (* Even if it does not work, this does not mean it is not provable 
+   (* Even if it does not work, this does not mean it is not provable
       -- the prover is REALLY incomplete *)
 (*	if debug then
 	  begin
@@ -1295,15 +1295,15 @@ let micromega_tauto negate normalise spec prover env polys1 polys2  gl =
         (Tacticals.tclTHENSEQ
           [
            Tactics.generalize ids;
-           micromega_order_change spec res' 
+           micromega_order_change spec res'
             (Term.mkApp(Lazy.force coq_list,[|  spec.proof_typ|]))  env  ff' ;
            ]) gl
 
 
-let micromega_gen 
-    parse_arith 
-    (negate:'cst atom -> 'cst mc_cnf) 
-    (normalise:'cst atom -> 'cst mc_cnf) 
+let micromega_gen
+    parse_arith
+    (negate:'cst atom -> 'cst mc_cnf)
+    (normalise:'cst atom -> 'cst mc_cnf)
     spec  prover   gl =
   let concl = Tacmach.pf_concl gl in
   let hyps  = Tacmach.pf_hyps_types gl in
@@ -1311,8 +1311,8 @@ let micromega_gen
    let (hyps,concl,env) = parse_goal parse_arith Env.empty hyps concl in
    let env = Env.elements env in
     micromega_tauto negate normalise spec prover env hyps concl gl
-  with 
-   | Failure x -> flush stdout ; Pp.pp_flush () ; 
+  with
+   | Failure x -> flush stdout ; Pp.pp_flush () ;
       Tacticals.tclFAIL 0 (Pp.str x) gl
    | ParseError  -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
 
@@ -1328,16 +1328,16 @@ type provername = string * int option
 
 open Persistent_cache
 
-module Cache = PHashtable(struct 
-  type t = (provername * micromega_polys) 
+module Cache = PHashtable(struct
+  type t = (provername * micromega_polys)
   let equal = (=)
   let hash  = Hashtbl.hash
 end)
 
-let csdp_cache = "csdp.cache" 
+let csdp_cache = "csdp.cache"
 
 let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivstellensatz option  =
-  fun provername poly -> 
+  fun provername poly ->
 
   let cmdname =
     List.fold_left Filename.concat (Envars.coqlib ())
@@ -1355,36 +1355,36 @@ let xcall_csdpcert =
 
 let call_csdpcert prover pb = xcall_csdpcert (prover,pb)
 
-let rec z_to_q_pol e = 
+let rec z_to_q_pol e =
  match e with
   | Mc.Pc z   -> Mc.Pc {Mc.qnum = z ; Mc.qden = Mc.XH}
   | Mc.Pinj(p,pol)   -> Mc.Pinj(p,z_to_q_pol pol)
   | Mc.PX(pol1,p,pol2) -> Mc.PX(z_to_q_pol pol1, p, z_to_q_pol pol2)
 
 
-let call_csdpcert_q provername poly = 
+let call_csdpcert_q provername poly =
  match call_csdpcert provername poly with
   | None -> None
-  | Some cert -> 
+  | Some cert ->
      let cert = Certificate.q_cert_of_pos cert in
      if Mc.qWeakChecker poly cert
      then Some cert
      else ((print_string "buggy certificate" ; flush stdout) ;None)
 
 
-let call_csdpcert_z provername poly = 
+let call_csdpcert_z provername poly =
  let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in
   match call_csdpcert provername l with
    | None -> None
-   | Some cert -> 
+   | Some cert ->
       let cert = Certificate.z_cert_of_pos cert in
       if Mc.zWeakChecker poly cert
       then Some cert
       else ((print_string "buggy certificate" ; flush stdout) ;None)
 
 
-let  xhyps_of_cone base acc prf = 
-  let rec xtract e acc = 
+let  xhyps_of_cone base acc prf =
+  let rec xtract e acc =
     match e with
     | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> acc
     | Mc.PsatzIn n -> let n = (CoqToCaml.nat n) in
@@ -1401,7 +1401,7 @@ let hyps_of_cone prf = xhyps_of_cone 0 ISet.empty prf
 let compact_cone prf f  =
   let np n = CamlToCoq.nat (f (CoqToCaml.nat n)) in
 
-  let rec xinterp prf = 
+  let rec xinterp prf =
     match prf with
     | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> prf
     | Mc.PsatzIn n -> Mc.PsatzIn (np n)
@@ -1411,31 +1411,31 @@ let compact_cone prf f  =
 
     xinterp prf
 
-let hyps_of_pt pt = 
-  let rec xhyps base pt acc = 
+let hyps_of_pt pt =
+  let rec xhyps base pt acc =
     match pt with
       | Mc.DoneProof -> acc
       | Mc.RatProof(c,pt) ->  xhyps (base+1) pt (xhyps_of_cone base acc c)
       | Mc.CutProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c)
-      | Mc.EnumProof(c1,c2,l) -> 
+      | Mc.EnumProof(c1,c2,l) ->
 	  let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in
 	    List.fold_left (fun s x -> xhyps (base + 1) x s) s l in
-    
+
     xhyps 0 pt ISet.empty
 
-let hyps_of_pt pt = 
+let hyps_of_pt pt =
   let res = hyps_of_pt pt in
-    if debug 
+    if debug
     then (Printf.fprintf stdout "\nhyps_of_pt : %a -> " pp_proof_term pt ; ISet.iter (fun i -> Printf.printf "%i " i) res);
     res
-	  
-  
-let compact_pt pt f = 
+
+
+let compact_pt pt f =
   let translate ofset x =
     if x < ofset then x
     else (f (x-ofset)  + ofset) in
 
-  let rec compact_pt ofset pt = 
+  let rec compact_pt ofset pt =
     match pt with
       | Mc.DoneProof -> Mc.DoneProof
       | Mc.RatProof(c,pt) -> Mc.RatProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt )
@@ -1451,8 +1451,8 @@ let compact_pt pt f =
 let lift_pexpr_prover p l =  p (List.map (fun (e,o) -> Mc.denorm e , o) l)
 
 let linear_prover_Z = {
-  name    = "linear prover" ; 
-  prover  = lift_ratproof (lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec)) ; 
+  name    = "linear prover" ;
+  prover  = lift_ratproof (lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec)) ;
   hyps    = hyps_of_pt ;
   compact = compact_pt ;
   pp_prf  = pp_proof_term;
@@ -1461,8 +1461,8 @@ let linear_prover_Z = {
 
 let linear_prover_Q = {
   name    = "linear prover";
-  prover  = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ; 
-  hyps    = hyps_of_cone ; 
+  prover  = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ;
+  hyps    = hyps_of_cone ;
   compact = compact_cone ;
   pp_prf  = pp_psatz pp_q ;
   pp_f   = fun o x -> pp_pol pp_q o  (fst x)
@@ -1470,8 +1470,8 @@ let linear_prover_Q = {
 
 let linear_prover_R = {
   name    = "linear prover";
-  prover  = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec) ; 
-  hyps    = hyps_of_cone ; 
+  prover  = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec) ;
+  hyps    = hyps_of_cone ;
   compact = compact_cone ;
   pp_prf  = pp_psatz pp_z ;
   pp_f    =  fun o x -> pp_pol pp_z o (fst x)
@@ -1504,7 +1504,7 @@ let non_linear_prover_Z str o  = {
   pp_f    =  fun o x -> pp_pol pp_z o (fst x)
 }
 
-module CacheZ = PHashtable(struct 
+module CacheZ = PHashtable(struct
   type t = (Mc.z Mc.pol * Mc.op1) list
   let equal = (=)
   let hash  = Hashtbl.hash
@@ -1515,7 +1515,7 @@ let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate
 
 let linear_Z =   {
   name = "lia";
-  prover = memo_zlinear_prover ; 
+  prover = memo_zlinear_prover ;
   hyps   = hyps_of_pt;
   compact = compact_pt;
   pp_prf      = pp_proof_term;
@@ -1526,52 +1526,52 @@ let linear_Z =   {
 
 (** Instantiation of the tactics *)
 
-let psatzl_Z gl = 
+let psatzl_Z gl =
  micromega_gen parse_zarith  Mc.negate Mc.normalise zz_domain_spec
   [linear_prover_Z ] gl
 
 
-let psatzl_Q gl = 
- micromega_gen  parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec 
+let psatzl_Q gl =
+ micromega_gen  parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec
   [ linear_prover_Q ]   gl
 
 
-let psatz_Q i gl = 
+let psatz_Q i gl =
  micromega_gen parse_qarith Mc.qnegate Mc.qnormalise qq_domain_spec
   [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ]  gl
 
 
-let psatzl_R gl = 
- micromega_gen  parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec 
+let psatzl_R gl =
+ micromega_gen  parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec
   [ linear_prover_R ]   gl
 
-let psatz_R i gl = 
+let psatz_R i gl =
  micromega_gen parse_rarith Mc.rnegate Mc.rnormalise rz_domain_spec
   [ non_linear_prover_R "real_nonlinear_prover" (Some i)]  gl
 
 
-let psatz_Z i gl = 
- micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec 
+let psatz_Z i gl =
+ micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec
  [non_linear_prover_Z "real_nonlinear_prover" (Some i) ] gl
 
 
-let sos_Z gl = 
- micromega_gen parse_zarith Mc.negate Mc.normalise  zz_domain_spec 
+let sos_Z gl =
+ micromega_gen parse_zarith Mc.negate Mc.normalise  zz_domain_spec
   [non_linear_prover_Z "pure_sos" None]  gl
 
-let sos_Q gl = 
- micromega_gen parse_qarith Mc.qnegate Mc.qnormalise  qq_domain_spec 
+let sos_Q gl =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise  qq_domain_spec
   [non_linear_prover_Q "pure_sos" None]  gl
 
 
-let sos_R gl = 
- micromega_gen parse_rarith Mc.rnegate Mc.rnormalise  rz_domain_spec 
+let sos_R gl =
+ micromega_gen parse_rarith Mc.rnegate Mc.rnormalise  rz_domain_spec
   [non_linear_prover_R "pure_sos" None]  gl
 
 
 
-let xlia gl = 
- micromega_gen parse_zarith Mc.negate Mc.normalise   zz_domain_spec 
+let xlia gl =
+ micromega_gen parse_zarith Mc.negate Mc.normalise   zz_domain_spec
   [linear_Z] gl
 
 (* Local Variables: *)
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index 78087c0704..d4e6d920bd 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -29,7 +29,7 @@ type provername = string * int option
 
 
 let debug = true
-let flags = [Open_append;Open_binary;Open_creat] 
+let flags = [Open_append;Open_binary;Open_creat]
 
 let chan = open_out_gen flags 0o666 "trace"
 
@@ -41,7 +41,7 @@ struct
  let rec expr_to_term = function
   |  PEc z ->  Const  (C2Ml.q_to_num z)
   |  PEX v ->  Var ("x"^(string_of_int (C2Ml.index v)))
-  |  PEmul(p1,p2) -> 
+  |  PEmul(p1,p2) ->
       let p1 = expr_to_term p1 in
       let p2 = expr_to_term p2 in
       let res = Mul(p1,p2) in 	   res
@@ -51,12 +51,12 @@ struct
   | PEpow(p,n)   -> Pow(expr_to_term p , C2Ml.n n)
   |  PEopp p ->  Opp (expr_to_term p)
 
-      
-end 
-open M      
+
+end
+open M
 
 open List
-open Mutils 
+open Mutils
 
 
 
@@ -65,29 +65,29 @@ let rec canonical_sum_to_string = function s -> failwith "not implemented"
 
 let print_canonical_sum m = Format.print_string (canonical_sum_to_string m)
 
-let print_list_term o l = 
+let print_list_term o l =
   output_string o "print_list_term\n";
  List.iter (fun (e,k) -> Printf.fprintf o "q: %s %s ;"
-  (string_of_poly (poly_of_term (expr_to_term e))) 
-  (match k with 
-    Mc.Equal -> "= " 
-   | Mc.Strict -> "> " 
-   | Mc.NonStrict -> ">= " 
+  (string_of_poly (poly_of_term (expr_to_term e)))
+  (match k with
+    Mc.Equal -> "= "
+   | Mc.Strict -> "> "
+   | Mc.NonStrict -> ">= "
    | _ -> failwith "not_implemented")) (List.map (fun (e, o) -> Mc.denorm e , o) l) ;
  output_string o "\n"
 
 
-let partition_expr l = 
+let partition_expr l =
  let rec f i = function
   | [] -> ([],[],[])
   | (e,k)::l ->
      let (eq,ge,neq) = f (i+1) l in
-      match k with 
+      match k with
        | Mc.Equal -> ((e,i)::eq,ge,neq)
        | Mc.NonStrict -> (eq,(e,Axiom_le i)::ge,neq)
-       | Mc.Strict    -> (* e > 0 == e >= 0 /\ e <> 0 *) 
+       | Mc.Strict    -> (* e > 0 == e >= 0 /\ e <> 0 *)
 	  (eq, (e,Axiom_lt i)::ge,(e,Axiom_lt i)::neq)
-       | Mc.NonEqual -> (eq,ge,(e,Axiom_eq i)::neq) 
+       | Mc.NonEqual -> (eq,ge,(e,Axiom_eq i)::neq)
 	  (* Not quite sure -- Coq interface has changed *)
  in f 0 l
 
@@ -96,28 +96,28 @@ let rec sets_of_list l =
  match l with
   | [] -> [[]]
   | e::l -> let s = sets_of_list l in
-	     s@(List.map (fun s0 -> e::s0) s) 
+	     s@(List.map (fun s0 -> e::s0) s)
 
 (* The exploration is probably not complete - for simple cases, it works... *)
 let real_nonlinear_prover d l =
   let l = List.map (fun (e,op) -> (Mc.denorm e,op)) l in
- try 
+ try
   let (eq,ge,neq) = partition_expr l in
 
   let rec elim_const  = function
     [] ->  []
    | (x,y)::l -> let p = poly_of_term (expr_to_term x) in
-		  if poly_isconst p 
-		  then elim_const l 
+		  if poly_isconst p
+		  then elim_const l
 		  else (p,y)::(elim_const l) in
 
   let eq = elim_const eq in
   let peq = List.map  fst eq in
-   
-  let pge = List.map 
+
+  let pge = List.map
    (fun (e,psatz) -> poly_of_term (expr_to_term e),psatz) ge in
-   
-  let monoids = List.map (fun m ->  (List.fold_right (fun (p,kd) y -> 
+
+  let monoids = List.map (fun m ->  (List.fold_right (fun (p,kd) y ->
    let p = poly_of_term (expr_to_term p) in
     match kd with
      | Axiom_lt i -> poly_mul p y
@@ -125,30 +125,30 @@ let real_nonlinear_prover d l =
      |   _        -> failwith "monoids") m (poly_const (Int 1)) , map  snd m))
    (sets_of_list neq) in
 
-  let (cert_ideal, cert_cone,monoid) = deepen_until d (fun d -> 
-   list_try_find (fun m -> let (ci,cc) = 
+  let (cert_ideal, cert_cone,monoid) = deepen_until d (fun d ->
+   list_try_find (fun m -> let (ci,cc) =
     real_positivnullstellensatz_general false d peq pge (poly_neg (fst m) ) in
 		      (ci,cc,snd m)) monoids) 0 in
-   
-  let proofs_ideal = map2 (fun q i -> Eqmul(term_of_poly q,Axiom_eq i))  
+
+  let proofs_ideal = map2 (fun q i -> Eqmul(term_of_poly q,Axiom_eq i))
    cert_ideal (List.map snd eq) in
 
   let proofs_cone = map term_of_sos cert_cone in
-   
-  let proof_ne =  
-   let (neq , lt) = List.partition 
+
+  let proof_ne =
+   let (neq , lt) = List.partition
     (function  Axiom_eq _ -> true | _ -> false ) monoid in
-   let sq = match 
-     (List.map (function Axiom_eq i -> i | _ -> failwith "error") neq) 
+   let sq = match
+     (List.map (function Axiom_eq i -> i | _ -> failwith "error") neq)
     with
     | []  -> Rational_lt (Int 1)
     | l   -> Monoid l in
     List.fold_right (fun x y -> Product(x,y)) lt sq in
 
-  let proof = list_fold_right_elements 
+  let proof = list_fold_right_elements
    (fun s t -> Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) in
    S (Some proof)
- with 
+ with
   | Sos_lib.TooDeep -> S None
   |    x        ->   F (Printexc.to_string x)
 
@@ -156,17 +156,17 @@ let real_nonlinear_prover d l =
 let pure_sos  l =
   let l = List.map (fun (e,o) -> Mc.denorm e, o) l in
 
- (* If there is no strict inequality, 
+ (* If there is no strict inequality,
     I should nonetheless be able to try something - over Z  > is equivalent to -1  >= *)
- try 
+ try
   let l = List.combine l (interval 0 (length l -1)) in
   let (lt,i) =  try (List.find (fun (x,_) -> 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) *)
-  let pos = Product (Rational_lt n, 
+  let pos = Product (Rational_lt n,
 		    List.fold_right (fun (c,p) rst -> Sum (Product (Rational_lt c, Square
-		     (term_of_poly p)), rst)) 
+		     (term_of_poly p)), rst))
 		     polys (Rational_lt (Int 0))) in
   let proof = Sum(Axiom_lt i, pos) in
 (*  let s,proof' = scale_certificate proof in
@@ -174,11 +174,11 @@ let pure_sos  l =
     S (Some proof)
  with
 (*   | Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *)
-   |  x        -> (* May be that could be refined *) S None 
+   |  x        -> (* May be that could be refined *) S None
 
 
 
-let run_prover prover pb = 
+let run_prover prover pb =
     match prover with
     | "real_nonlinear_prover", Some d -> real_nonlinear_prover d pb
     | "pure_sos", None -> pure_sos pb
@@ -192,17 +192,17 @@ let output_csdp_certificate o = function
 
 
 let main () =
-  try 
+  try
     let (prover,poly) = (input_value stdin : provername * micromega_polys) in
     let cert = run_prover prover poly in
 (*      Printf.fprintf chan "%a -> %a" print_list_term poly output_csdp_certificate cert ;
       close_out chan ;   *)
-        
+
       output_value stdout (cert:csdp_certificate);
-      flush stdout ; 
+      flush stdout ;
       Marshal.to_channel  chan (cert:csdp_certificate) [] ;
-      flush chan ; 
-      exit 0 
+      flush chan ;
+      exit 0
   with  x -> (Printf.fprintf chan "error %s" (Printexc.to_string x)  ; exit 1)
 
 ;;
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index c547b3d4ae..6250e324a5 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -8,100 +8,100 @@ let debug = false
 type ('a,'b) lr = Inl of 'a | Inr of 'b
 
 
-module Vect = 
-  struct 
+module Vect =
+  struct
     (** [t] is the type of vectors.
 	A vector [(x1,v1) ; ... ; (xn,vn)] is such that:
 	- variables indexes are ordered (x1 < ... < xn
 	- values are all non-zero
     *)
     type var = int
-    type t = (var * num) list 
+    type t = (var * num) list
 
-(** [equal v1 v2 = true] if the vectors are syntactically equal. 
+(** [equal v1 v2 = true] if the vectors are syntactically equal.
     ([num] is not handled by  [Pervasives.equal] *)
 
-    let rec equal v1 v2 = 
+    let rec equal v1 v2 =
       match v1 , v2 with
 	| [] , []   -> true
 	| [] , _    -> false
 	| _::_ , [] -> false
-	| (i1,n1)::v1 , (i2,n2)::v2 -> 
+	| (i1,n1)::v1 , (i2,n2)::v2 ->
 	    (i1 = i2) && n1 =/ n2 && equal v1 v2
 
-    let hash v = 
-      let rec hash i = function 
+    let hash v =
+      let rec hash i = function
 	| [] -> i
 	| (vr,vl)::l ->  hash (i + (Hashtbl.hash (vr, float_of_num vl))) l in
 	Hashtbl.hash (hash 0 v )
 
-	
+
     let null = []
 
-    let pp_vect o vect = 
+    let pp_vect o vect =
       List.iter (fun (v,n) -> Printf.printf "%sx%i + " (string_of_num n) v) vect
-	
-    let from_list (l: num list) = 
-      let rec xfrom_list i l = 
+
+    let from_list (l: num list) =
+      let rec xfrom_list i l =
 	match l with
 	  | [] -> []
-	  | e::l ->  
-	      if e <>/ Int 0 
+	  | e::l ->
+	      if e <>/ Int 0
 	      then (i,e)::(xfrom_list (i+1) l)
 	      else xfrom_list (i+1) l in
-	
+
 	xfrom_list 0 l
 
     let zero_num = Int 0
     let unit_num = Int 1
-      
-      
-    let to_list m = 
+
+
+    let to_list m =
       let rec xto_list i l =
 	match l with
 	  | [] -> []
-	  |	(x,v)::l' -> 
+	  |	(x,v)::l' ->
 		  if i = x then v::(xto_list (i+1) l') else zero_num ::(xto_list (i+1) l) in
 	xto_list 0 m
-	  
+
 
     let cons i v rst = if v =/ Int 0 then rst else (i,v)::rst
-	
-    let rec update i f t = 
+
+    let rec update i f t =
       match t with
 	| [] -> cons i (f zero_num) []
-	| (k,v)::l -> 
+	| (k,v)::l ->
 	    match Pervasives.compare i k with
 	  | 0 -> cons k (f v) l
 	  | -1 -> cons i (f zero_num) t
 	  |  1 -> (k,v) ::(update i f l)
 	  |  _  -> failwith "compare_num"
-	       
+
     let rec set i n t =
       match t with
 	| [] -> cons i n []
-	| (k,v)::l -> 
+	| (k,v)::l ->
 	    match Pervasives.compare i k with
 	      | 0 -> cons k n l
 	      | -1 -> cons i n t
 	      |  1 -> (k,v) :: (set i n l)
 	      |  _  -> failwith "compare_num"
-		   
-    let gcd m = 
+
+    let gcd m =
       let res = List.fold_left (fun x (i,e) -> Big_int.gcd_big_int  x (Utils.numerator e))  Big_int.zero_big_int m in
-	if Big_int.compare_big_int res Big_int.zero_big_int = 0 
+	if Big_int.compare_big_int res Big_int.zero_big_int = 0
 	then Big_int.unit_big_int else res
-	  
-    let rec mul z t = 
+
+    let rec mul z t =
       match z with
 	| Int 0 -> []
 	| Int 1 -> t
 	|  _    -> List.map (fun (i,n) -> (i, mult_num z n)) t
 
-    let compare : t -> t -> int = Utils.Cmp.compare_list (fun x y -> Utils.Cmp.compare_lexical 
+    let compare : t -> t -> int = Utils.Cmp.compare_list (fun x y -> Utils.Cmp.compare_lexical
       [
 	(fun () -> Pervasives.compare (fst x) (fst y));
-	(fun () -> compare_num (snd x) (snd y))]) 
+	(fun () -> compare_num (snd x) (snd y))])
 
     (** [tail v vect] returns
 	- [None] if [v] is not a variable of the vector [vect]
@@ -109,16 +109,16 @@ module Vect =
         and [rst] is the remaining of the vector
 	We exploit that vectors are ordered lists
     *)
-    let rec tail (v:var) (vect:t) = 
+    let rec tail (v:var) (vect:t) =
       match vect with
 	| [] -> None
-	| (v',vl)::vect' -> 
+	| (v',vl)::vect' ->
 	    match Pervasives.compare v' v with
 	      | 0 -> Some (vl,vect) (* Ok, found *)
 	      | -1 -> tail v vect' (* Might be in the tail *)
 	      | _  -> None (* Hopeless *)
-		  
-    let get v vect = 
+
+    let get v vect =
       match tail v vect with
 	| None -> None
 	| Some(vl,_) -> Some vl
@@ -134,13 +134,13 @@ module Vect =
 open Vect
 
 (** Implementation of intervals *)
-module Itv = 
-struct 
-  
+module Itv =
+struct
+
   (** The type of intervals is *)
   type interval = num option * num option
       (** None models the absence of bound i.e. infinity *)
-      (** As a result, 
+      (** As a result,
 	  - None , None   -> ]-oo,+oo[
 	  - None , Some v -> ]-oo,v]
 	  - Some v, None  -> [v,+oo[
@@ -148,36 +148,36 @@ struct
       Intervals needs to be explicitely normalised.
       *)
 
-  type who = Left | Right 
+  type who = Left | Right
 
 
-  (** if then interval [itv] is empty, [norm_itv itv] returns [None] 
+  (** if then interval [itv] is empty, [norm_itv itv] returns [None]
       otherwise, it returns [Some itv] *)
-      
-  let norm_itv itv = 
+
+  let norm_itv itv =
     match itv with
       | Some a , Some b -> if a <=/ b then Some itv else None
       |   _             -> Some itv
-	    
+
   (** [opp_itv itv] computes the opposite interval *)
-  let opp_itv itv = 
+  let opp_itv itv =
   let (l,r) = itv in
     (map_option minus_num r, map_option minus_num l)
-      
+
 
 
 
 (** [inter i1 i2 = None] if the intersection of intervals is empty
     [inter i1 i2 = Some i] if [i] is the intersection of the intervals [i1] and [i2] *)
-  let inter i1 i2 = 
+  let inter i1 i2 =
     let (l1,r1) = i1
     and (l2,r2) = i2 in
-      
-    let inter f o1 o2 = 
+
+    let inter f o1 o2 =
       match o1 , o2 with
 	| None , None -> None
 	| Some _ , None -> o1
-	| None  , Some _ -> o2 
+	| None  , Some _ -> o2
 	| Some n1 , Some n2 -> Some (f n1 n2) in
 
     norm_itv (inter max_num l1 l2 , inter min_num r1 r2)
@@ -185,9 +185,9 @@ struct
   let range = function
     | None,_ | _,None -> None
     | Some i,Some j -> Some (floor_num j -/ceiling_num i +/ (Int 1))
-	
 
-  let smaller_itv i1 i2 = 
+
+  let smaller_itv i1 i2 =
     match  range i1 ,  range i2  with
       | None , _ -> false
       |  _   , None -> true
@@ -204,7 +204,7 @@ let in_bound bnd v =
     | Some a , Some b -> a <=/ v && v <=/ b
 
 end
-open Itv 
+open Itv
 type vector = Vect.t
 
 type cstr = { coeffs : vector ; bound : interval }
@@ -220,22 +220,22 @@ module PSet = ISet
 
 module System = Hashtbl.Make(Vect)
 
-  type proof = 
-      | Hyp of int 
+  type proof =
+      | Hyp of int
       | Elim of  var * proof * proof
       | And of proof * proof
 
 
 
-type system = { 
-  sys : cstr_info ref System.t ; 
+type system = {
+  sys : cstr_info ref System.t ;
   vars : ISet.t
-} 
-and cstr_info = { 
+}
+and cstr_info = {
   bound : interval ;
   prf : proof ;
   pos : int ;
-  neg : int ; 
+  neg : int ;
 }
 
 
@@ -247,85 +247,85 @@ and cstr_info = {
        When a new constraint c is computed by a function f(c1,...,cn), its proof_idx is ISet.fold union (List.map (fun x -> x.proof_idx) [c1;...;cn]
     - [pos] is the number of positive values of the vector
     - [neg] is the number of negative values of the vector
-    ( [neg] + [pos] is therefore the length of the vector) 
+    ( [neg] + [pos] is therefore the length of the vector)
     [v] is an upper-bound of the set of variables which appear in [s].
 *)
 
 (** To be thrown when a system has no solution *)
 exception SystemContradiction of proof
-let hyps prf = 
-  let rec hyps prf acc = 
+let hyps prf =
+  let rec hyps prf acc =
     match prf with
       | Hyp i -> ISet.add i acc
-      | Elim(_,prf1,prf2) 
+      | Elim(_,prf1,prf2)
       | And(prf1,prf2) -> hyps prf1 (hyps prf2 acc) in
     hyps prf ISet.empty
 
 
 (** Pretty printing *)
-  let rec pp_proof o prf = 
+  let rec pp_proof o prf =
     match prf with
       | Hyp i -> Printf.fprintf o "H%i" i
       | Elim(v, prf1,prf2) -> Printf.fprintf o "E(%i,%a,%a)" v pp_proof prf1 pp_proof prf2
       | And(prf1,prf2)   -> Printf.fprintf o "A(%a,%a)"  pp_proof prf1 pp_proof prf2
-	  
+
 let pp_bound o  = function
   | None -> output_string o "oo"
   | Some a -> output_string o (string_of_num a)
 
 let pp_itv o (l,r) = Printf.fprintf o "(%a,%a)" pp_bound l pp_bound r
 
-let rec pp_list f o l = 
+let rec pp_list f o l =
   match l with
     | [] -> ()
     | e::l -> f o e ; output_string o ";" ; pp_list f o l
 
-let pp_iset o s = 
+let pp_iset o s =
   output_string o "{" ;
   ISet.fold (fun i _ -> Printf.fprintf o "%i " i) s ();
-  output_string o "}" 
+  output_string o "}"
 
-let pp_pset o s = 
+let pp_pset o s =
   output_string o "{" ;
   PSet.fold (fun i _ -> Printf.fprintf o "%i " i) s ();
-  output_string o "}" 
+  output_string o "}"
 
 
 let pp_info o i = pp_itv o i.bound
 
-let pp_cstr o (vect,bnd) = 
+let pp_cstr o (vect,bnd) =
     let (l,r) = bnd in
       (match l with
 	| None -> ()
 	| Some n -> Printf.fprintf o "%s <= " (string_of_num n))
       ;
-      pp_vect o vect ; 
+      pp_vect o vect ;
       (match r with
 	      | None -> output_string o"\n"
 	      | Some n -> Printf.fprintf o "<=%s\n" (string_of_num n))
 
 
-let pp_system o sys= 
-  System.iter (fun vect ibnd -> 
+let pp_system o sys=
+  System.iter (fun vect ibnd ->
     pp_cstr o (vect,(!ibnd).bound)) sys
 
 
 
-let pp_split_cstr o (vl,v,c,_) = 
+let pp_split_cstr o (vl,v,c,_) =
   Printf.fprintf o "(val x = %s ,%a,%s)" (string_of_num vl) pp_vect  v  (string_of_num c)
 
 (** [merge_cstr_info] takes:
-    - the intersection of bounds and 
+    - the intersection of bounds and
     - the union of proofs
     - [pos] and [neg] fields should be identical *)
 
-let merge_cstr_info i1 i2 = 
+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 (p1 = p2 && n1 = n2) ;
     match inter i1 i2 with
       | None -> None (* Could directly raise a system contradiction exception *)
-      | Some bnd -> 
+      | Some bnd ->
 	  Some { pos = p1 ; neg = n1 ; bound = bnd ; prf = And(prf1,prf2) }
 
 (** [xadd_cstr vect cstr_info] loads an constraint into the system.
@@ -333,18 +333,18 @@ let merge_cstr_info i1 i2 =
     @raise SystemContradiction if [cstr_info] returns [None]
 *)
 
-let xadd_cstr vect cstr_info sys =   
-  if debug && System.length sys mod 1000 = 0 then (print_string "*" ; flush stdout) ; 
-  try 
+let xadd_cstr vect cstr_info sys =
+  if debug && 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
 	  | None       -> raise (SystemContradiction  (And(cstr_info.prf, (!info).prf)))
 	  | Some info' -> info := info'
-      with 
+      with
 	| Not_found -> System.replace  sys vect (ref cstr_info)
 
 
-type cstr_ext = 
+type cstr_ext =
     | Contradiction (** The constraint is contradictory.
 			Typically, a [SystemContradiction] exception will be raised. *)
     | Redundant  (** The constrain is redundant.
@@ -353,16 +353,16 @@ type cstr_ext =
 				     Typically, it will be added to the constraint system. *)
 
 (** [normalise_cstr] : vector -> cstr_info -> cstr_ext *)
-let normalise_cstr vect cinfo = 
+let normalise_cstr vect cinfo =
   match norm_itv cinfo.bound with
     | None -> Contradiction
-    | Some (l,r) -> 
+    | Some (l,r) ->
 	match vect with
 	  | [] -> if Itv.in_bound (l,r) (Int 0) then Redundant else Contradiction
 	  | (_,n)::_ ->  Cstr(
-	      (if n <>/ Int 1 then List.map (fun (x,nx) -> (x,nx // n)) vect else vect), 
+	      (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 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)})
 
@@ -378,21 +378,21 @@ let eval_op = function
   | Eq -> (=/)
   | Ge ->  (>=/)
 
-let count v = 
+let count v =
   let rec count n p v =
     match v with
       | [] -> (n,p)
-      | (_,vl)::v -> let sg = sign_num vl in 
-		       assert (sg <> 0) ; 
+      | (_,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
     count 0 0 v
 
 
 let norm_cstr {coeffs = v ; op = o ; cst = c} idx =
-  let (n,p) = count v in 
+  let (n,p) = count v in
 
-  normalise_cstr v {pos = p ; neg = n ; bound = 
-  (match o with 
+  normalise_cstr v {pos = p ; neg = n ; bound =
+  (match o with
 	| Eq -> Some c , Some c
 	| Ge -> Some c , None) ;
 	    prf = Hyp idx }
@@ -402,60 +402,60 @@ let norm_cstr {coeffs = v ; op = o ; cst = c} idx =
     @return a system of constraints
     @raise SystemContradiction if a contradiction is found
 *)
-let load_system l = 
-    
+let load_system l =
+
   let sys = System.create 1000 in
-    
+
   let li = Mutils.mapi (fun e i -> (e,i)) l in
 
-  let vars = List.fold_left (fun vrs (cstr,i) -> 
+  let vars = List.fold_left (fun vrs (cstr,i) ->
     match norm_cstr cstr i with
       | Contradiction -> raise (SystemContradiction (Hyp i))
       | Redundant      -> vrs
-      | Cstr(vect,info) -> 
+      | Cstr(vect,info) ->
 	  xadd_cstr  vect info sys ;
 	  List.fold_left (fun s (v,_) -> ISet.add v s) vrs cstr.coeffs) ISet.empty li   in
 
     {sys = sys ;vars = vars}
 
-let system_list sys = 
-  let { sys = s ; vars  = v } = sys in  
-    System.fold (fun k bi l -> (k, !bi)::l) s [] 
+let system_list sys =
+  let { sys = s ; vars  = v } = sys in
+    System.fold (fun k bi l -> (k, !bi)::l) s []
 
 
-(** [add (v1,c1)  (v2,c2)  ] 
+(** [add (v1,c1)  (v2,c2)  ]
     precondition:  (c1 <>/ Int 0 && c2 <>/ Int 0)
-    @return a pair [(v,ln)] such that 
+    @return a pair [(v,ln)] such that
     [v] is the sum of vector [v1] divided by [c1] and vector [v2] divided by [c2]
     Note that the resulting vector is not normalised.
 *)
 
-let add (v1,c1)  (v2,c2)  = 
+let add (v1,c1)  (v2,c2)  =
     assert (c1 <>/ Int 0 && c2 <>/ Int 0) ;
 
-  let rec xadd v1 v2  = 
+  let rec xadd v1 v2  =
     match v1 , v2 with
-      | (x1,n1)::v1' , (x2,n2)::v2' -> 
-	  if x1 = x2 
-	  then 
+      | (x1,n1)::v1' , (x2,n2)::v2' ->
+	  if x1 = x2
+	  then
 	    let n' = (n1 // c1) +/ (n2 // c2) in
-	      if n' =/ Int 0 then xadd v1' v2' 
-	      else 
+	      if n' =/ Int 0 then xadd v1' v2'
+	      else
 		let res = xadd v1' v2'  in
 		  (x1,n') ::res
 	  else if x1 < x2
 	  then let res = xadd v1' v2   in
-		 (x1, n1 // c1)::res 
+		 (x1, n1 // c1)::res
 	  else let res = xadd v1 v2'  in
 		 (x2, n2 // c2)::res
       |  [] , [] -> []
       |  [] ,  _ -> List.map (fun (x,vl) -> (x,vl // c2)) v2
       |  _  , [] -> List.map (fun (x,vl) -> (x,vl // c1)) v1 in
-    
+
   let res = xadd v1 v2 in
     (res, count res)
 
-let add (v1,c1)   (v2,c2)  = 
+let add (v1,c1)   (v2,c2)  =
   let res = add (v1,c1)   (v2,c2)  in
     (*    Printf.printf "add(%a,%s,%a,%s) -> %a\n" pp_vect v1 (string_of_num c1) pp_vect v2 (string_of_num c2) pp_vect (fst res) ;*)
     res
@@ -464,27 +464,27 @@ type tlr = (num * vector * cstr_info) list
 type tm = (vector * cstr_info ) list
 
 (** To perform Fourier elimination, constraints are categorised depending on the sign of the variable to eliminate. *)
-    
+
 (** [split x vect info (l,m,r)]
     @param v is the variable to eliminate
-    @param l contains constraints such that (e + a*x) // a >= c / a 
+    @param l contains constraints such that (e + a*x) // a >= c / a
     @param r contains constraints such that (e + a*x) // - a >= c / -a
     @param m contains constraints which do not mention [x]
 *)
 
 let split x (vect: vector) info (l,m,r) =
-    match get x vect with 
+    match get x vect with
       | None -> (* The constraint does not mention [x], store it in m *)
-	  (l,(vect,info)::m,r) 
+	  (l,(vect,info)::m,r)
       | Some vl -> (* otherwise *)
 
-          let cons_bound lst bd = 
+          let cons_bound lst bd =
             match  bd with
               | None -> lst
               | Some bnd -> (vl,vect,{info with bound = Some bnd,None})::lst in
-        
+
           let lb,rb = info.bound in
-            if sign_num vl = 1 
+            if 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)
@@ -493,36 +493,36 @@ let split x (vect: vector) info (l,m,r) =
 (** [project vr sys] projects system [sys] over the set of variables [ISet.remove vr sys.vars ].
     This is a one step Fourier elimination.
 *)
-let project vr sys = 
-  
+let project vr sys =
+
   let (l,m,r)  = System.fold (fun vect rf l_m_r -> split vr vect !rf l_m_r) sys.sys  ([],[],[])  in
 
   let new_sys = System.create (System.length sys.sys) in
-    
+
     (* Constraints in [m] belong to the projection - for those [vr] is already projected out *)
     List.iter (fun  (vect,info) -> System.replace new_sys vect (ref info) )  m ;
 
-    let elim (v1,vect1,info1) (v2,vect2,info2) = 
+    let elim (v1,vect1,info1) (v2,vect2,info2) =
       let {neg = n1 ; pos = p1 ; bound = bound1 ; prf = prf1} = info1
       and {neg = n2 ; pos = p2 ; bound = bound2 ; prf = prf2} = info2 in
 
-      let bnd1 = from_option (fst bound1) 
+      let bnd1 = from_option (fst bound1)
       and bnd2 = from_option (fst bound2) in
       let bound = (bnd1 // v1) +/ (bnd2 // minus_num v2) in
       let vres,(n,p) = add (vect1,v1) (vect2,minus_num v2)  in
         (vres,{neg = n ; pos = p ; bound = (Some bound, None); prf = Elim(vr,info1.prf,info2.prf)}) in
 
-      List.iter(fun  l_elem -> List.iter (fun r_elem -> 
+      List.iter(fun  l_elem -> List.iter (fun r_elem ->
         let (vect,info) = elim l_elem r_elem in
 	  match normalise_cstr vect info with
 	    | Redundant -> ()
 	    | Contradiction -> raise (SystemContradiction  info.prf)
 	    | Cstr(vect,info)   -> xadd_cstr vect info new_sys) r ) l;
       {sys = new_sys ; vars = ISet.remove  vr sys.vars}
-      
+
 
 (** [project_using_eq] performs elimination by pivoting using an equation.
-    This is the counter_part of the [elim] sub-function of [!project]. 
+    This is the counter_part of the [elim] sub-function of [!project].
     @param vr is the variable to be used as pivot
     @param c is the coefficient of variable [vr] in vector [vect]
     @param len is the length of the equation
@@ -530,42 +530,42 @@ let project vr sys =
     @param prf is the proof of the equation
 *)
 
-let project_using_eq vr c vect bound  prf (vect',info') = 
+let project_using_eq vr c vect bound  prf (vect',info') =
     match get vr vect' with
-    | Some c2 -> 
+    | Some c2 ->
 	let c1 = if c2 >=/ Int 0 then minus_num c else c in
-	  
+
 	let c2 = abs_num c2 in
-	  
+
 	let (vres,(n,p)) = add (vect,c1) (vect', c2)  in
-	  
+
 	let cst = bound // c1 in
-	  
-	let bndres = 
+
+	let bndres =
 	  let f x = cst +/ x // c2 in
 	  let (l,r) = info'.bound in
 	    (map_option f l , map_option f r) in
-	  
+
 	  (vres,{neg = n ; pos = p ; bound = bndres ; prf = Elim(vr,prf,info'.prf)})
     | None -> (vect',info')
 
 let elim_var_using_eq vr vect cst  prf sys =
   let c = from_option (get vr vect) in
-  
+
   let elim_var = project_using_eq vr c vect cst prf  in
 
   let  new_sys  =  System.create (System.length sys.sys) in
 
-    System.iter(fun vect iref -> 
+    System.iter(fun vect iref ->
       let (vect',info') = elim_var (vect,!iref) in
 	match normalise_cstr vect' info' with
 	    | Redundant -> ()
 	    | Contradiction -> raise (SystemContradiction info'.prf)
-	    | Cstr(vect,info')   -> xadd_cstr vect info' new_sys) sys.sys ; 
-    
+	    | Cstr(vect,info')   -> xadd_cstr vect info' new_sys) sys.sys ;
+
     {sys = new_sys ; vars = ISet.remove  vr sys.vars}
 
-	
+
 (** [size sys] computes the number of entries in the system of constraints *)
 let size sys = System.fold (fun v iref s -> s + (!iref).neg + (!iref).pos) sys 0
 
@@ -577,23 +577,23 @@ let pp_map o map = IMap.fold (fun k elt () -> Printf.fprintf o "%i -> %s\n" k (s
     If [map] binds all the variables of [vect], we get
     [eval_vect map [(x1,v1);...;(xn,vn)] = (IMap.find x1 map * v1) + ... + (IMap.find xn map) * vn , []]
     The function returns as second argument, a sub-vector consisting in the variables that are not in [map]. *)
-    
-let  eval_vect map vect = 
-  let rec xeval_vect vect sum rst = 
+
+let  eval_vect map vect =
+  let rec xeval_vect vect sum rst =
     match vect with
       | [] -> (sum,rst)
-      | (v,vl)::vect -> 
-	  try 
+      | (v,vl)::vect ->
+	  try
 	    let val_v = IMap.find v map in
 	      xeval_vect vect (sum +/ (val_v */ vl)) rst
 	  with
 	      Not_found -> xeval_vect vect sum ((v,vl)::rst) in
     xeval_vect vect (Int 0) []
-  
+
 
 (** [restrict_bound n sum itv] returns the interval of [x]
     given that (fst itv) <=  x * n + sum <= (snd itv) *)
-let restrict_bound n sum (itv:interval) = 
+let restrict_bound n sum (itv:interval) =
   let f x  = (x -/ sum) // n in
   let l,r = itv in
     match sign_num n with
@@ -606,8 +606,8 @@ let restrict_bound n sum (itv:interval) =
 
 (** [bound_of_variable map v sys] computes the interval of [v] in
     [sys] given a mapping [map] binding all the other variables *)
-let bound_of_variable map v sys = 
-  System.fold (fun vect iref bnd  -> 
+let bound_of_variable map v sys =
+  System.fold (fun vect iref bnd  ->
     let sum,rst = eval_vect  map vect in
     let vl = match get v rst with
       | None -> Int 0
@@ -618,53 +618,53 @@ let bound_of_variable map v sys =
 
 
 (** [pick_small_value bnd] picks a value being closed to zero within the interval *)
-let pick_small_value bnd = 
+let pick_small_value bnd =
   match bnd with
     | None , None   ->  Int 0
     | None , Some i ->  if  (Int 0) <=/ (floor_num  i) then Int 0 else floor_num i
     | Some i,None   ->  if i <=/ (Int 0) then Int 0 else ceiling_num i
-    | Some i,Some j -> 
-	if i <=/ Int 0 && Int 0 <=/ j 
+    | Some i,Some j ->
+	if i <=/ Int 0 && Int 0 <=/ j
 	then Int 0
-	else if ceiling_num i <=/ floor_num j 
+	else if ceiling_num i <=/ floor_num j
 	then ceiling_num i (* why not *) else i
 
 
-(** [solution s1 sys_l  = Some(sn,[(vn-1,sn-1);...; (v1,s1)]@sys_l)] 
+(** [solution s1 sys_l  = Some(sn,[(vn-1,sn-1);...; (v1,s1)]@sys_l)]
     then [sn] is a  system which contains only [black_v] -- if it existed in [s1]
-    and [sn+1] is obtained by projecting [vn] out of [sn] 
-    @raise SystemContradiction if  system [s] has no solution 
+    and [sn+1] is obtained by projecting [vn] out of [sn]
+    @raise SystemContradiction if  system [s] has no solution
 *)
 
-let solve_sys black_v choose_eq choose_variable sys sys_l = 
+let solve_sys black_v choose_eq choose_variable sys sys_l =
 
-  let rec solve_sys sys sys_l = 
+  let rec solve_sys sys sys_l =
     if debug then Printf.printf "S #%i size %i\n" (System.length sys.sys) (size sys.sys);
-    
+
     let eqs = choose_eq sys in
-      try 
+      try
 	let (v,vect,cst,ln) =  fst (List.find (fun ((v,_,_,_),_) -> v <> black_v) eqs) in
-	  if debug then 
+	  if debug then
 	    (Printf.printf "\nE %a = %s variable %i\n" pp_vect vect (string_of_num cst) v ;
 	     flush stdout);
 	  let sys' = elim_var_using_eq v vect cst ln sys in
-	    solve_sys sys' ((v,sys)::sys_l)  
-    with Not_found -> 
+	    solve_sys sys' ((v,sys)::sys_l)
+    with Not_found ->
       let vars = choose_variable  sys in
-	try 
+	try
 	  let (v,est) =  (List.find (fun (v,_) -> v <> black_v) vars) in
-	    if debug then (Printf.printf "\nV : %i esimate %f\n" v est ; flush stdout) ; 
+	    if debug then (Printf.printf "\nV : %i esimate %f\n" v est ; flush stdout) ;
 	    let sys' =  project v sys in
-	      solve_sys sys' ((v,sys)::sys_l) 
+	      solve_sys sys' ((v,sys)::sys_l)
 	with Not_found ->  (* we are done *) Inl (sys,sys_l)  in
     solve_sys sys sys_l
 
 
 
 
-let  solve black_v choose_eq choose_variable cstrs = 
+let  solve black_v choose_eq choose_variable cstrs =
 
-  try 
+  try
     let sys = load_system cstrs in
 (*      Printf.printf "solve :\n %a" pp_system sys.sys ; *)
       solve_sys black_v choose_eq choose_variable sys []
@@ -675,22 +675,22 @@ let  solve black_v choose_eq choose_variable cstrs =
     The output is an ordered list of (variable,cost).
 *)
 
-module EstimateElimVar = 
+module EstimateElimVar =
 struct
   type sys_list = (vector * cstr_info) list
 
   let abstract_partition (v:int) (l: sys_list) =
 
-    let rec xpart (l:sys_list) (ltl:sys_list) (n:int list) (z:int) (p:int list) = 
+    let rec xpart (l:sys_list) (ltl:sys_list) (n:int list) (z:int) (p:int list) =
       match l with
         | [] -> (ltl, n,z,p)
-        | (l1,info) ::rl -> 
+        | (l1,info) ::rl ->
             match  l1 with
             | [] -> xpart rl (([],info)::ltl) n (info.neg+info.pos+z) p
-            | (vr,vl)::rl1 -> 
+            | (vr,vl)::rl1 ->
 		if v = vr
 		then
-		  let cons_bound lst bd = 
+		  let cons_bound lst bd =
 		    match  bd with
 		      | None -> lst
 		      | Some bnd -> info.neg+info.pos::lst in
@@ -701,7 +701,7 @@ struct
 		    else  xpart rl ((rl1,info)::ltl) (cons_bound n rb) z (cons_bound p lb)
 		else
 		  (* the variable is greater *)
-		  xpart rl ((l1,info)::ltl) n (info.neg+info.pos+z) p 
+		  xpart rl ((l1,info)::ltl) n (info.neg+info.pos+z) p
 
     in
     let (sys',n,z,p) =  xpart l [] [] 0 []  in
@@ -711,72 +711,72 @@ struct
     let lp = float_of_int (List.length p) in
     let sp = float_of_int (List.fold_left (+) 0 p) in
       (sys',  float_of_int z +.  lp *.  sn +.  ln *.  sp -. lp*.ln)
-        
-        
+
+
   let choose_variable   sys =
     let {sys = s ; vars = v} = sys in
-      
+
     let sl = system_list sys in
 
     let evals  = fst
       (ISet.fold (fun v (eval,s) -> let ts,vl = abstract_partition v s  in
                                       ((v,vl)::eval, ts)) v ([],sl)) in
-      
+
       List.sort (fun x y -> Pervasives.compare (snd x) (snd y) ) evals
 
 
-end 
+end
 open EstimateElimVar
 
 (** The  module [EstimateElimEq] is similar to [EstimateElimVar] but it orders equations.
 *)
 module EstimateElimEq =
-struct 
-  
-  let itv_point bnd = 
+struct
+
+  let itv_point bnd =
     match bnd with
       |(Some a, Some b) -> a =/ b
       | _   -> false
 
-  let eq_bound bnd c = 
+  let eq_bound bnd c =
     match bnd with
       |(Some a, Some b) -> a =/ b && c =/ b
       | _   -> false
-    
 
-  let rec unroll_until v l = 
+
+  let rec unroll_until v l =
     match l with
       | [] -> (false,[])
-      | (i,_)::rl -> if i = v 
-	then (true,rl) 
+      | (i,_)::rl -> if i = v
+	then (true,rl)
 	else if i < v then unroll_until v rl else (false,l)
 
 
-  let choose_primal_equation eqs sys_l = 
+  let choose_primal_equation eqs sys_l =
 
-    let is_primal_equation_var v = 
-      List.fold_left (fun (nb_eq,nb_cst) (vect,info) -> 
-	if fst (unroll_until v vect) 
+    let is_primal_equation_var v =
+      List.fold_left (fun (nb_eq,nb_cst) (vect,info) ->
+	if fst (unroll_until v vect)
 	then if itv_point  info.bound then (nb_eq +  1,nb_cst) else (nb_eq,nb_cst)
 	else (nb_eq,nb_cst)) (0,0) sys_l in
 
-    let rec find_var vect = 
+    let rec find_var vect =
       match vect with
 	| [] -> None
-	| (i,_)::vect -> 
+	| (i,_)::vect ->
 	    let (nb_eq,nb_cst) = is_primal_equation_var i in
 	      if nb_eq = 2 && nb_cst = 0
 	      then Some i else find_var vect in
 
-    let rec find_eq_var eqs = 
+    let rec find_eq_var eqs =
       match eqs with
 	| [] -> None
-	| (vect,a,prf,ln)::l -> 
-	    match find_var vect with 
+	| (vect,a,prf,ln)::l ->
+	    match find_var vect with
 		| None -> find_eq_var l
-		| Some r -> Some (r,vect,a,prf,ln) 
+		| Some r -> Some (r,vect,a,prf,ln)
     in
-      
+
 
       find_eq_var eqs
 
@@ -787,33 +787,33 @@ struct
 
     let sys_l = system_list sys in
 
-    let equalities = List.fold_left 
-      (fun  l (vect,info) -> 
+    let equalities = List.fold_left
+      (fun  l (vect,info) ->
 	match  info.bound with
-	  | Some a , Some b -> 
+	  | Some a , Some b ->
 	      if a =/ b then (* This an equation *)
 		(vect,a,info.prf,info.neg+info.pos)::l else l
 	  |   _ -> l
       ) [] sys_l  in
 
-    let rec estimate_cost v ct sysl acc tlsys = 
+    let rec estimate_cost v ct sysl acc tlsys =
       match sysl with
 	| [] -> (acc,tlsys)
 	| (l,info)::rsys ->
 	    let ln = info.pos + info.neg in
 	    let (b,l) = unroll_until v l in
 	    match b with
-	      | true -> 
-		  if itv_point info.bound 
+	      | true ->
+		  if itv_point info.bound
 		  then estimate_cost  v ct rsys (acc+ln) ((l,info)::tlsys) (* this is free *)
 		  else estimate_cost v ct rsys (acc+ln+ct) ((l,info)::tlsys)  (* should be more ? *)
 	      | false -> estimate_cost v ct rsys (acc+ln) ((l,info)::tlsys) in
 
       match choose_primal_equation equalities sys_l with
-	| None -> 
-	    let cost_eq eq const prf ln acc_costs = 
-	      
-	      let rec cost_eq eqr sysl costs = 
+	| None ->
+	    let cost_eq eq const prf ln acc_costs =
+
+	      let rec cost_eq eqr sysl costs =
 		match eqr with
 		  | [] -> costs
 		  | (v,_) ::eqr -> let (cst,tlsys) = estimate_cost v (ln-1) sysl 0 [] in
@@ -823,7 +823,7 @@ struct
 	    let all_costs = List.fold_left (fun all_costs (vect,const,prf,ln) -> cost_eq vect const prf ln all_costs) [] equalities in
 
 	      (*      pp_list (fun o ((v,eq,_,_),cst) -> Printf.fprintf o "((%i,%a),%i)\n" v pp_vect eq cst) stdout all_costs ; *)
-	      
+
 	      List.sort (fun x y -> Pervasives.compare (snd x) (snd y) ) all_costs
 	| Some (v,vect, const,prf,_) -> [(v,vect,const,prf),0]
 
@@ -834,33 +834,33 @@ open EstimateElimEq
 module Fourier =
 struct
 
-  let optimise vect l = 
+  let optimise vect l =
     (* We add a dummy (fresh) variable for vector *)
-    let fresh = 
+    let fresh =
       List.fold_left (fun fr c -> Pervasives.max fr (Vect.fresh c.coeffs)) 0 l in
     let cstr = {
-      coeffs = Vect.set fresh (Int (-1)) vect ; 
-      op = Eq ; 
+      coeffs = Vect.set fresh (Int (-1)) vect ;
+      op = Eq ;
       cst = (Int 0)} in
       match solve fresh choose_equality_var choose_variable (cstr::l) with
 	| Inr prf -> None (* This is an unsatisfiability proof *)
-	| Inl (s,_) -> 
-	    try 
+	| Inl (s,_) ->
+	    try
 	      Some (bound_of_variable IMap.empty fresh s.sys)
 	    with
 		x -> Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None
 
 
-  let find_point cstrs = 
-  
+  let find_point cstrs =
+
     match solve max_int choose_equality_var choose_variable cstrs with
       | Inr prf -> Inr prf
-      | Inl (_,l) -> 
-      
-	let rec rebuild_solution l map = 
+      | Inl (_,l) ->
+
+	let rec rebuild_solution l map =
 	  match l with
 	    | [] -> map
-	    | (v,e)::l -> 
+	    | (v,e)::l ->
 		let itv = bound_of_variable map v e.sys in
 		let map = IMap.add v (pick_small_value itv) map in
 		  rebuild_solution l map
@@ -877,9 +877,9 @@ end
 
 
 module Proof =
-struct 
-  
-	
+struct
+
+
 
 
 (** A proof term in the sense of a ZMicromega.RatProof is a positive combination of the hypotheses which leads to a contradiction.
@@ -893,49 +893,49 @@ struct
 
   let forall_pairs f l1 l2 =
     List.fold_left (fun acc e1 ->
-      List.fold_left (fun acc e2 -> 
+      List.fold_left (fun acc e2 ->
 	match f e1 e2 with
 	  | None -> acc
 	  | Some v -> v::acc) acc l2) [] l1
 
 
-  let add_op x y = 
+  let add_op x y =
     match x , y with
       | Eq , Eq -> Eq
       |     _   -> Ge
 
 
-  let pivot v (p1,c1) (p2,c2) = 
+  let pivot v (p1,c1) (p2,c2) =
     let {coeffs = v1 ; op = op1 ; cst = n1} = c1
     and {coeffs = v2 ; op = op2 ; cst = n2} = c2 in
-      
+
       match Vect.get v v1 , Vect.get v v2 with
         | None , _ | _ , None -> None
-        | Some a   , Some b   -> 
+        | Some a   , Some b   ->
             if (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) ; 
+            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
-            then Some (add (p1,minus_num (a // b)) (p2,Int 1), 
-                      {coeffs = add (v1,minus_num (a// b)) (v2 ,Int 1) ; 
+            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
 	    then
-	      Some (add (p2,minus_num (b // a)) (p1,Int 1), 
-                   {coeffs = add (v2,minus_num (b// a)) (v1 ,Int 1) ; 
+	      Some (add (p2,minus_num (b // a)) (p1,Int 1),
+                   {coeffs = add (v2,minus_num (b// a)) (v1 ,Int 1) ;
                     op     = add_op op1 op2;
                     cst    = n2 // (minus_num (b// a)) +/ n1 // (Int 1)})
-	    else  None (* op2 could be Eq ... this might happen *) 
-    
+	    else  None (* op2 could be Eq ... this might happen *)
+
 
-  let normalise_proofs l = 
-    List.fold_left (fun acc (prf,cstr) -> 
+  let normalise_proofs l =
+    List.fold_left (fun acc (prf,cstr) ->
       match acc with
         | Inr _ -> acc (* I already found a contradiction *)
-        | Inl acc -> 
+        | Inl acc ->
             match norm_cstr cstr 0 with
               | Redundant -> Inl acc
               | Contradiction -> Inr (prf,cstr)
@@ -944,11 +944,11 @@ struct
 
   type oproof = (vector * cstr_compat * num) option
 
-  let merge_proof (oleft:oproof) (prf,cstr,v,info) (oright:oproof) = 
+  let merge_proof (oleft:oproof) (prf,cstr,v,info) (oright:oproof) =
     let (l,r) = info.bound in
 
-    let keep p ob bd = 
-      match ob , bd with 
+    let keep p ob bd =
+      match ob , bd with
         | None , None -> None
         | None , Some b -> Some(prf,cstr,b)
         | Some _ , None -> ob
@@ -959,24 +959,24 @@ struct
       (* Now, there might be a contradiction *)
       match oleft , oright with
         | None , _ | _ , None -> Inl (oleft,oright)
-        | Some(prfl,cstrl,l) , Some(prfr,cstrr,r) -> 
-            if l <=/ r 
+        | Some(prfl,cstrl,l) , Some(prfr,cstrr,r) ->
+            if l <=/ r
             then Inl (oleft,oright)
             else (* There is a contradiction - it should show up by scaling up the vectors - any pivot should do*)
               match cstrr.coeffs with
                 | [] -> Inr (add (prfl,Int 1) (prfr,Int 1), cstrr) (* this is wrong *)
-                | (v,_)::_ -> 
+                | (v,_)::_ ->
                     match pivot v (prfl,cstrl) (prfr,cstrr) with
                       | None -> failwith "merge_proof : pivot is not possible"
                       | Some x -> Inr x
 
-let  mk_proof hyps prf = 
+let  mk_proof hyps prf =
   (* I am keeping list - I might have a proof for the left bound and a proof for the right bound.
      If I perform aggressive elimination of redundancies, I expect the list to be of length at most 2.
      For each proof list, all the vectors should be of the form a.v for different constants a.
   *)
 
-  let rec mk_proof prf = 
+  let rec mk_proof prf =
     match prf with
       | Hyp i -> [ ([i, Int 1] , List.nth hyps i) ]
 
@@ -985,15 +985,15 @@ let  mk_proof hyps prf =
           and prfsr = mk_proof prf2 in
             (* I take only the pairs for which the elimination is meaningfull *)
             forall_pairs (pivot v) prfsl prfsr
-      | And(prf1,prf2) -> 
-          let prfsl1 = mk_proof prf1 
+      | And(prf1,prf2) ->
+          let prfsl1 = mk_proof prf1
           and prfsl2 = mk_proof prf2 in
           (* detect trivial redundancies and contradictions *)
             match normalise_proofs (prfsl1@prfsl2) with
               | Inr x -> [x] (* This is a contradiction - this should be the end of the proof *)
               | Inl l -> (* All the vectors are the same *)
-                  let prfs = 
-                    List.fold_left (fun acc e -> 
+                  let prfs =
+                    List.fold_left (fun acc e ->
                       match acc with
                         | Inr _ -> acc (* I have a contradiction *)
                         | Inl (oleft,oright) -> merge_proof oleft e oright) (Inl(None,None)) l in
@@ -1008,5 +1008,5 @@ let  mk_proof hyps prf =
     mk_proof prf
 
 
-end 
+end
 
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index d884f26598..5c45c8f5fa 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -803,7 +803,7 @@ let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with
                      (match q0 with
                         | Pc c -> q0
                         | Pinj (j', q1) -> Pinj ((pplus XH j'), q1)
-                        | PX (p3, p4, p5) -> Pinj (XH, q0)) p')) i' 
+                        | PX (p3, p4, p5) -> Pinj (XH, q0)) p')) i'
                  (p0 cO))
                (mkPX cO ceqb
                  (pmulI cO cI cmul ceqb (fun x x0 ->
@@ -1599,16 +1599,16 @@ let rec zChecker l = function
                                          (match op4 with
                                             | NonStrict ->
                                                 if is_pol_Z0 (padd1 e1 e2)
-                                                then 
+                                                then
                                                   let rec label pfs lb ub =
-                                                    
+
                                                   match pfs with
-                                                    | 
+                                                    |
                                                   [] ->
                                                   if z_gt_dec lb ub
                                                   then true
                                                   else false
-                                                    | 
+                                                    |
                                                   pf1 :: rsr ->
                                                   (&&)
                                                   (zChecker
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index a0158b1567..ec06fa58bb 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -14,25 +14,25 @@
 
 let debug = false
 
-let finally f rst = 
-  try 
+let finally f rst =
+  try
     let res = f () in
       rst () ; res
-  with x -> 
-    (try rst () 
+  with x ->
+    (try rst ()
     with _  -> raise x
     ); raise x
 
-let map_option f x = 
+let map_option f x =
   match x with
     | None -> None
     | Some v -> Some (f v)
 
 let from_option = function
   | None -> failwith "from_option"
-  | Some v -> v  
+  | Some v -> v
 
-let rec try_any l x = 
+let rec try_any l x =
  match l with
   | [] -> None
   | (f,s)::l -> match f x with
@@ -40,20 +40,20 @@ let rec try_any l x =
      | x -> x
 
 let iteri f l =
- let rec xiter i l = 
+ let rec xiter i l =
   match l with
    | [] -> ()
    | e::l -> f i e ; xiter (i+1) l in
   xiter 0 l
 
 let mapi f l =
- let rec xmap i l = 
+ let rec xmap i l =
   match l with
    | [] -> []
    | e::l -> (f i e)::xmap (i+1) l in
   xmap 0 l
 
-let rec map3 f l1 l2 l3 = 
+let rec map3 f l1 l2 l3 =
   match l1 , l2 ,l3 with
     | [] , [] , [] -> []
     | e1::l1 , e2::l2 , e3::l3 -> (f e1 e2 e3)::(map3 f l1 l2 l3)
@@ -61,14 +61,14 @@ let rec map3 f l1 l2 l3 =
 
 
 
-let rec is_sublist l1 l2 = 
+let rec is_sublist l1 l2 =
   match l1 ,l2 with
     | [] ,_ -> true
     | e::l1', [] -> false
-    | e::l1' , e'::l2' -> 
+    | e::l1' , e'::l2' ->
 	if e = e' then is_sublist l1' l2'
 	else is_sublist l1 l2'
-		
+
 
 
 let list_try_find f =
@@ -85,16 +85,16 @@ let rec list_fold_right_elements f l =
     | x::l -> f x (aux l) in
   aux l
 
-let interval n m = 
+let interval n m =
   let rec interval_n (l,m) =
     if n > m then l else interval_n (m::l,pred m)
-  in 
+  in
   interval_n ([],m)
 
 open Num
 open Big_int
 
-let ppcm x y = 
+let ppcm x y =
  let g = gcd_big_int x y in
  let x' = div_big_int x g in
  let y' = div_big_int y g in
@@ -115,26 +115,26 @@ let rec ppcm_list c l =
   | [] -> c
   | e::l -> ppcm_list (ppcm c (denominator e)) l
 
-let rec rec_gcd_list c l  = 
+let rec rec_gcd_list c l  =
  match l with
   | [] -> c
   | e::l -> rec_gcd_list (gcd_big_int  c (numerator e)) l
 
-let rec gcd_list l = 
+let rec gcd_list l =
  let res = rec_gcd_list zero_big_int l in
-  if compare_big_int res zero_big_int = 0 
+  if compare_big_int res zero_big_int = 0
   then unit_big_int else res
-   
-   
-   
-let rats_to_ints l = 
+
+
+
+let rats_to_ints l =
  let c = ppcm_list unit_big_int l in
-  List.map (fun x ->  (div_big_int (mult_big_int (numerator x) c) 
+  List.map (fun x ->  (div_big_int (mult_big_int (numerator x) c)
 			(denominator x))) l
-   
+
 (* Nasty reordering of lists - useful to trim certificate down *)
 let mapi f l =
- let rec xmapi i l = 
+ let rec xmapi i l =
   match l with
    | []   -> []
    | e::l ->  (f e i)::(xmapi (i+1) l) in
@@ -146,11 +146,11 @@ let concatMapi f l = List.rev (mapi (fun e i -> (i,f e)) l)
 (* assoc_pos j [a0...an] = [j,a0....an,j+n],j+n+1 *)
 let assoc_pos j l = (mapi (fun e i -> e,i+j) l, j + (List.length l))
 
-let assoc_pos_assoc l = 
+let assoc_pos_assoc l =
  let rec xpos i l =
   match l with
    | [] -> []
-   | (x,l) ::rst -> let (l',j) = assoc_pos i l in 
+   | (x,l) ::rst -> let (l',j) = assoc_pos i l in
 		     (x,l')::(xpos j rst) in
   xpos 0 l
 
@@ -159,7 +159,7 @@ let filter_pos f l =
  let rec xfilter l =
   match l with
    | []  -> []
-   | (x,e)::l -> 
+   | (x,e)::l ->
       if List.exists (fun ee -> List.mem ee f) (List.map snd e)
       then (x,e)::(xfilter l)
       else xfilter l in
@@ -169,11 +169,11 @@ let  select_pos lpos l =
  let rec xselect i lpos l =
   match lpos with
    | [] -> []
-   | j::rpos -> 
+   | j::rpos ->
       match l with
        | []   -> failwith "select_pos"
-       | e::l -> 
-	  if i = j 
+       | e::l ->
+	  if i = j
 	  then e:: (xselect (i+1) rpos l)
 	  else xselect (i+1) lpos l in
   xselect 0 lpos l
@@ -188,7 +188,7 @@ struct
   | S n -> (nat n) + 1
 
 
- let rec positive p = 
+ let rec positive p =
   match p with
    | XH -> 1
    | XI p -> 1+ 2*(positive p)
@@ -208,7 +208,7 @@ struct
    | XO i -> 2*(index i)
 
 
- let z x = 
+ let z x =
   match x with
    | Z0 -> 0
    | Zpos p -> (positive p)
@@ -223,7 +223,7 @@ struct
    | XO p -> (mult_int_big_int 2 (positive_big_int p))
 
 
- let z_big_int x = 
+ let z_big_int x =
   match x with
    | Z0 -> zero_big_int
    | Zpos p -> (positive_big_int p)
@@ -232,9 +232,9 @@ struct
 
  let num x = Num.Big_int (z_big_int x)
 
- let q_to_num {qnum = x ; qden = y} = 
+ let q_to_num {qnum = x ; qden = y} =
   Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y)))
-  
+
 end
 
 
@@ -252,8 +252,8 @@ struct
   else if n land 1 = 1 then XI (positive (n lsr 1))
   else  XO (positive (n lsr 1))
 
- let  n nt = 
-  if nt < 0 
+ let  n nt =
+  if nt < 0
   then assert false
   else if nt = 0 then N0
   else Npos (positive nt)
@@ -264,47 +264,47 @@ struct
   else  XO (index (n lsr 1))
 
 
- let idx n = 
+ let idx n =
   (*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 [] 
+   if n=1 then []
    else (n mod 2 = 1)::(digits_of_int (n lsr 1))
   in
-   List.fold_right 
+   List.fold_right
     (fun b c -> (if b then XI c else XO c))
     (List.rev (digits_of_int n))
     (XH)
 
- let z x = 
+ let z x =
   match compare x 0 with
    | 0 -> Z0
    | 1 -> Zpos (positive x)
    | _ -> (* this should be -1 *)
-      Zneg (positive (-x)) 
+      Zneg (positive (-x))
 
  open Big_int
 
- let positive_big_int n = 
-  let two = big_int_of_int 2 in 
-  let rec _pos n = 
+ let positive_big_int n =
+  let two = big_int_of_int 2 in
+  let rec _pos n =
    if eq_big_int n unit_big_int then XH
    else
     let (q,m) = quomod_big_int n two  in
-     if eq_big_int unit_big_int m 
+     if eq_big_int unit_big_int m
      then XI (_pos q)
      else XO (_pos q) in
    _pos n
 
- let bigint x = 
+ let bigint x =
   match sign_big_int x with
    | 0 -> Z0
    | 1 -> Zpos (positive_big_int x)
    | _ -> Zneg (positive_big_int (minus_big_int x))
 
- let q n = 
-  {Micromega.qnum = bigint (numerator n) ; 
+ let q n =
+  {Micromega.qnum = bigint (numerator n) ;
    Micromega.qden = positive_big_int (denominator n)}
 
 end
@@ -312,23 +312,23 @@ end
 module Cmp =
 struct
 
- let rec compare_lexical l = 
+ let rec compare_lexical l =
   match l with
    | [] -> 0 (* Equal *)
-   | f::l -> 
+   | f::l ->
       let cmp = f () in
        if cmp = 0 	then  compare_lexical l else cmp
 
- let rec compare_list cmp l1 l2 = 
+ let rec compare_list cmp l1 l2 =
   match l1 , l2 with
    | []  , [] -> 0
    | []  , _  -> -1
    | _   , [] -> 1
-   | e1::l1 , e2::l2 -> 
+   | e1::l1 , e2::l2 ->
       let c = cmp e1 e2 in
        if c = 0 then compare_list cmp l1 l2 else c
-	
- let hash_list hash l = 
+
+ let hash_list hash l =
   let rec _hash_list l h =
    match l with
     | []  -> h lxor (Hashtbl.hash [])
@@ -373,21 +373,21 @@ let command exe_path args vl =
   let outch = Unix.out_channel_of_descr stdin_write in
     output_value outch vl ;
     flush outch ;
-    
+
   (* Wait for its completion *)
     let _pid,status = Unix.waitpid [] pid in
 
-      finally 
-	(fun () -> 
+      finally
+	(fun () ->
 	  (* Recover the result *)
 	  match status with
-	    | Unix.WEXITED 0 -> 
-		let inch  = Unix.in_channel_of_descr  stdout_read in 
+	    | Unix.WEXITED 0 ->
+		let inch  = Unix.in_channel_of_descr  stdout_read in
 		  begin try Marshal.from_channel inch with x -> failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) end
 	    | Unix.WEXITED i -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
 	    | Unix.WSIGNALED i -> failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i)
 	    | Unix.WSTOPPED  i -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i))
-	(fun () -> 
+	(fun () ->
 	  (* Cleanup  *)
 	  List.iter (fun x -> try Unix.close x with _ -> ()) [stdin_read; stdin_write; stdout_read ; stdout_write ; stderr_read; stderr_write]
 	)
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 87c9d1bbeb..f17e1c35bd 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -13,13 +13,13 @@
 (************************************************************************)
 
 
-module type PHashtable = 
+module type PHashtable =
   sig
     type 'a t
-    type key 
+    type key
 
     val create : int -> string -> 'a t
-    (** [create i f] creates an empty persistent table 
+    (** [create i f] creates an empty persistent table
 	with initial size i
 	associated with file [f] *)
 
@@ -31,7 +31,7 @@ module type PHashtable =
 
     val find : 'a t -> key -> 'a
     (** find has the specification of Hashtable.find *)
-      
+
     val add  : 'a t -> key -> 'a -> unit
     (** [add tbl key elem] adds the binding [key] [elem] to the table [tbl].
 	(and writes the binding to the file associated with [tbl].)
@@ -50,7 +50,7 @@ module type PHashtable =
 
 open Hashtbl
 
-module PHashtable(Key:HashedType) : PHashtable with type key = Key.t  = 
+module PHashtable(Key:HashedType) : PHashtable with type key = Key.t  =
 struct
 
   type key = Key.t
@@ -66,27 +66,27 @@ struct
   type mode = Closed | Open
 
 
-  type 'a t = 
-      { 
+  type 'a t =
+      {
 	outch : out_channel ;
-	mutable status : mode ; 
+	mutable status : mode ;
 	htbl : 'a Table.t
       }
 
 
-let create i f = 
-  { 
-    outch = open_out_bin f ; 
-    status = Open ; 
+let create i f =
+  {
+    outch = open_out_bin f ;
+    status = Open ;
     htbl = Table.create i
   }
 
-let finally f rst = 
-  try 
+let finally f rst =
+  try
     let res = f () in
       rst () ; res
-  with x -> 
-    (try rst () 
+  with x ->
+    (try rst ()
     with _  -> raise x
     ); raise x
 
@@ -94,80 +94,80 @@ let finally f rst =
 let read_key_elem inch =
   try
     Some (Marshal.from_channel inch)
-  with 
+  with
     | End_of_file -> None
     |    _        -> raise InvalidTableFormat
-      
-let open_in f = 
+
+let open_in f =
   let flags = [Open_rdonly;Open_binary;Open_creat] in
   let inch = open_in_gen flags 0o666 f in
   let htbl = Table.create 10 in
 
-  let rec xload () = 
+  let rec xload () =
     match read_key_elem inch with
       | None -> ()
-      | Some (key,elem) -> 
-	  Table.add htbl key elem ; 
+      | Some (key,elem) ->
+	  Table.add htbl key elem ;
 	  xload () in
 
-    try 
+    try
       finally (fun () -> xload () ) (fun () -> close_in inch) ;
       {
 	outch = begin
 	  let flags = [Open_append;Open_binary;Open_creat] in
-	    open_out_gen flags 0o666 f 
+	    open_out_gen flags 0o666 f
 	end ;
 	status = Open ;
 	htbl = htbl
       }
-    with InvalidTableFormat -> 
+    with InvalidTableFormat ->
       (* Try to keep as many entries as possible *)
       begin
 	let flags = [Open_wronly; Open_trunc;Open_binary;Open_creat] in
 	let outch = open_out_gen flags 0o666 f in
-	  Table.iter (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl; 
+	  Table.iter (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
 	  { outch = outch ;
-	    status = Open ; 
+	    status = Open ;
 	    htbl   = htbl
 	  }
       end
 
 
-let close t = 
+let close t =
   let {outch = outch ; status = status ; htbl = tbl} = t in
     match t.status with
     | Closed -> () (* don't do it twice *)
-    | Open  -> 
-	close_out outch ; 
+    | Open  ->
+	close_out outch ;
 	Table.clear tbl ;
 	t.status <- Closed
 
-let add t k e = 
+let add t k e =
   let {outch = outch ; status = status ; htbl = tbl} = t in
     if status = Closed
     then raise UnboundTable
     else
       begin
-	Table.add tbl k e ; 
+	Table.add tbl k e ;
 	Marshal.to_channel outch (k,e) [Marshal.No_sharing]
       end
 
-let find t k = 
+let find t k =
   let {outch = outch ; status = status ; htbl = tbl} = t in
     if status = Closed
     then raise UnboundTable
     else
       let res = Table.find tbl k in
-	res 
+	res
 
-let memo cache f = 
+let memo cache f =
   let tbl = lazy (open_in cache) in
-    fun x -> 
+    fun x ->
       let tbl = Lazy.force tbl in
-	try 
+	try
 	  find tbl x
 	with
-	    Not_found -> 
+	    Not_found ->
 	      let res = f x in
 		add tbl x res ;
 		res
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 87e55c9e17..2512dee92d 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -318,16 +318,16 @@ let string_of_vname (v:vname): string = (v: string);;
 let rec string_of_term t =
   match t with
   Opp t1 -> "(- " ^ string_of_term t1 ^ ")"
-| Add (t1, t2) -> 
+| Add (t1, t2) ->
    "(" ^ (string_of_term t1) ^ " + " ^ (string_of_term t2) ^ ")"
-| Sub (t1, t2) -> 
+| Sub (t1, t2) ->
    "(" ^ (string_of_term t1) ^ " - " ^ (string_of_term t2) ^ ")"
-| Mul (t1, t2) -> 
+| Mul (t1, t2) ->
    "(" ^ (string_of_term t1) ^ " * " ^ (string_of_term t2) ^ ")"
 | Inv t1 -> "(/ " ^ string_of_term t1 ^ ")"
-| Div (t1, t2) -> 
+| Div (t1, t2) ->
    "(" ^ (string_of_term t1) ^ " / " ^ (string_of_term t2) ^ ")"
-| Pow (t1, n1) -> 
+| Pow (t1, n1) ->
    "(" ^ (string_of_term t1) ^ " ^ " ^ (string_of_int n1) ^ ")"
 | Zero -> "0"
 | Var v -> "x" ^ (string_of_vname v)
@@ -384,11 +384,11 @@ let print_poly m = Format.print_string(string_of_poly m);;
 (* ------------------------------------------------------------------------- *)
 
 let rec poly_of_term t = match t with
-  Zero -> poly_0 
+  Zero -> poly_0
 | Const n -> poly_const n
 | Var x -> poly_var x
 | Opp t1 -> poly_neg (poly_of_term t1)
-| Inv t1 -> 
+| Inv t1 ->
       let p = poly_of_term t1 in
       if poly_isconst p then poly_const(Int 1 // eval undefined p)
       else failwith "poly_of_term: inverse of non-constant polyomial"
diff --git a/plugins/micromega/sos.mli b/plugins/micromega/sos.mli
index 42e22ffec2..e38caba06c 100644
--- a/plugins/micromega/sos.mli
+++ b/plugins/micromega/sos.mli
@@ -24,7 +24,7 @@ val poly_of_term : term -> poly
 
 val term_of_poly : poly -> term
 
-val term_of_sos : positivstellensatz * (Num.num * poly) list -> 
+val term_of_sos : positivstellensatz * (Num.num * poly) list ->
      positivstellensatz
 
 val string_of_poly : poly -> string
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index a9228365ec..baf90d4daa 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -606,16 +606,16 @@ let rec deepen f n =
 
 exception TooDeep
 
-let deepen_until limit f n = 
+let deepen_until limit f n =
   match compare limit 0 with
     | 0 -> raise TooDeep
     | -1 -> deepen f n
-    | _  -> 
+    | _  ->
 	let rec d_until  f n =
-	  try(* if !debugging 
-	  then (print_string "Searching with depth limit "; 
+	  try(* if !debugging
+	  then (print_string "Searching with depth limit ";
 		print_int n; print_newline()) ;*) f n
-	  with Failure x -> 
+	  with Failure x ->
 	    (*if !debugging then (Printf.printf "solver error : %s\n" x) ; *)
 	    if n = limit then raise TooDeep else  d_until f (n + 1) in
 	  d_until f n