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

5 files changed, 496 insertions, 496 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 12176d661..a97f43d08 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -12,19 +12,19 @@ Delimit Scope Int_scope with I.
 
 (* Abstract Integers. *)
 
-Module Type Int. 
+Module Type Int.
 
-  Parameter int : Set. 
+  Parameter int : Set.
 
-  Parameter zero : int. 
-  Parameter one : int. 
-  Parameter plus : int -> int -> int. 
+  Parameter zero : int.
+  Parameter one : int.
+  Parameter plus : int -> int -> int.
   Parameter opp : int -> int.
-  Parameter minus : int -> int -> int. 
+  Parameter minus : int -> int -> int.
   Parameter mult : int -> int -> int.
 
   Notation "0" := zero : Int_scope.
-  Notation "1" := one : Int_scope. 
+  Notation "1" := one : Int_scope.
   Infix "+" := plus : Int_scope.
   Infix "-" := minus : Int_scope.
   Infix "*" := mult : Int_scope.
@@ -57,17 +57,17 @@ Module Type Int.
   Axiom lt_0_1 : 0<1.
   Axiom plus_le_compat : forall i j k l, i<=j -> k<=l -> i+k<=j+l.
   Axiom opp_le_compat : forall i j, i<=j -> (-j)<=(-i).
-  Axiom mult_lt_compat_l : 
+  Axiom mult_lt_compat_l :
    forall i j k, 0 < k -> i < j -> k*i<k*j.
 
-  (* We should have a way to decide the equality and the order*)  
+  (* We should have a way to decide the equality and the order*)
   Parameter compare : int -> int -> comparison.
   Infix "?=" := compare (at level 70, no associativity) : Int_scope.
   Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j.
   Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j.
   Axiom compare_Gt : forall i j, compare i j = Gt <-> i>j.
 
-  (* Up to here, these requirements could be fulfilled 
+  (* Up to here, these requirements could be fulfilled
      by any totally ordered ring. Let's now be int-specific: *)
   Axiom le_lt_int : forall x y, x<y <-> x<=y+-(1).
 
@@ -83,9 +83,9 @@ Module Z_as_Int <: Int.
 
   Open Scope Z_scope.
 
-  Definition int := Z. 
-  Definition zero := 0. 
-  Definition one := 1. 
+  Definition int := Z.
+  Definition zero := 0.
+  Definition one := 1.
   Definition plus := Zplus.
   Definition opp := Zopp.
   Definition minus := Zminus.
@@ -154,32 +154,32 @@ Module Z_as_Int <: Int.
    apply Zlt_succ.
   Qed.
 
-End Z_as_Int.  
+End Z_as_Int.
 
 
 
 
-Module IntProperties (I:Int). 
+Module IntProperties (I:Int).
  Import I.
- 
+
  (* Primo, some consequences of being a ring theory... *)
- 
+
  Definition two := 1+1.
- Notation "2" := two : Int_scope. 
+ Notation "2" := two : Int_scope.
 
  (* Aliases for properties packed in the ring record. *)
 
  Definition plus_assoc := ring.(Radd_assoc).
  Definition plus_comm := ring.(Radd_comm).
  Definition plus_0_l := ring.(Radd_0_l).
- Definition mult_assoc := ring.(Rmul_assoc). 
+ Definition mult_assoc := ring.(Rmul_assoc).
  Definition mult_comm := ring.(Rmul_comm).
  Definition mult_1_l := ring.(Rmul_1_l).
  Definition mult_plus_distr_r := ring.(Rdistr_l).
  Definition opp_def := ring.(Ropp_def).
  Definition minus_def := ring.(Rsub_def).
 
- Opaque plus_assoc plus_comm plus_0_l mult_assoc mult_comm mult_1_l 
+ Opaque plus_assoc plus_comm plus_0_l mult_assoc mult_comm mult_1_l
   mult_plus_distr_r opp_def minus_def.
 
  (* More facts about plus *)
@@ -188,7 +188,7 @@ Module IntProperties (I:Int).
  Proof. intros; rewrite plus_comm; apply plus_0_l. Qed.
 
  Lemma plus_0_r_reverse : forall x, x = x+0.
- Proof. intros; symmetry; apply plus_0_r. Qed. 
+ Proof. intros; symmetry; apply plus_0_r. Qed.
 
  Lemma plus_assoc_reverse : forall x y z, x+y+z = x+(y+z).
  Proof. intros; symmetry; apply plus_assoc. Qed.
@@ -197,14 +197,14 @@ Module IntProperties (I:Int).
  Proof. intros; do 2 rewrite plus_assoc; f_equal; apply plus_comm. Qed.
 
  Lemma plus_reg_l : forall x y z, x+y = x+z -> y = z.
- Proof. 
+ Proof.
   intros.
   rewrite (plus_0_r_reverse y), (plus_0_r_reverse z), <-(opp_def x).
-  now rewrite plus_permute, plus_assoc, H, <- plus_assoc, plus_permute. 
+  now rewrite plus_permute, plus_assoc, H, <- plus_assoc, plus_permute.
  Qed.
 
- (* More facts about mult *) 
-   
+ (* More facts about mult *)
+
  Lemma mult_assoc_reverse : forall x y z, x*y*z = x*(y*z).
  Proof. intros; symmetry; apply mult_assoc. Qed.
 
@@ -216,7 +216,7 @@ Module IntProperties (I:Int).
  Qed.
 
  Lemma mult_0_l : forall x, 0*x = 0.
- Proof. 
+ Proof.
   intros.
   generalize (mult_plus_distr_r 0 1 x).
   rewrite plus_0_l, mult_1_l, plus_comm; intros.
@@ -224,7 +224,7 @@ Module IntProperties (I:Int).
   rewrite <- H.
   apply plus_0_r_reverse.
  Qed.
- 
+
 
  (* More facts about opp *)
 
@@ -269,7 +269,7 @@ Module IntProperties (I:Int).
   rewrite <- mult_opp_comm.
   apply plus_reg_l with (x*y).
   now rewrite opp_def, <-mult_plus_distr_r, opp_def, mult_0_l.
- Qed.  
+ Qed.
 
  Lemma egal_left : forall n m, n=m -> n+-m = 0.
  Proof. intros; subst; apply opp_def. Qed.
@@ -287,7 +287,7 @@ Module IntProperties (I:Int).
  Proof. symmetry; rewrite mult_comm; apply mult_1_l. Qed.
 
  Lemma red_factor1 : forall n, n+n = n*2.
- Proof. 
+ Proof.
   intros; unfold two.
   now rewrite mult_comm, mult_plus_distr_r, mult_1_l.
  Qed.
@@ -302,10 +302,10 @@ Module IntProperties (I:Int).
  Proof. intros; now rewrite plus_comm, red_factor2. Qed.
 
  Lemma red_factor4 : forall n m p, n*m + n*p = n*(m+p).
- Proof. 
+ Proof.
   intros; now rewrite mult_plus_distr_l.
  Qed.
- 
+
  Lemma red_factor5 : forall n m , n * 0 + m = m.
  Proof. intros; now rewrite mult_comm, mult_0_l, plus_0_l. Qed.
 
@@ -368,7 +368,7 @@ Module IntProperties (I:Int).
  Qed.
 
 
- (* Secondo, some results about order (and equality) *)  
+ (* Secondo, some results about order (and equality) *)
 
  Lemma lt_irrefl : forall n, ~ n<n.
  Proof.
@@ -440,7 +440,7 @@ Module IntProperties (I:Int).
  intros; unfold beq; generalize (compare_Eq i j).
  destruct compare; intuition discriminate.
  Qed.
-                               
+
  Lemma beq_true : forall i j, beq i j = true -> i=j.
  Proof.
  intros.
@@ -471,7 +471,7 @@ Module IntProperties (I:Int).
  Proof. intros; now rewrite <- bgt_iff. Qed.
 
  Lemma bgt_false : forall i j, bgt i j = false -> i<=j.
- Proof. 
+ Proof.
   intros.
   rewrite le_lt_iff, <-gt_lt_iff, <-bgt_iff; intro H'; now rewrite H' in H.
  Qed.
@@ -498,7 +498,7 @@ Module IntProperties (I:Int).
   destruct (lt_eq_lt_dec p m) as [[H|H]|H]; subst; auto.
   generalize (lt_trans _ _ _ H C); intuition.
  Qed.
- 
+
  (* order and operations *)
 
  Lemma le_0_neg : forall n, 0 <= n <-> -n <= 0.
@@ -582,7 +582,7 @@ Module IntProperties (I:Int).
  Lemma mult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0.
  Proof.
  intros.
- destruct (lt_eq_lt_dec n 0) as [[Hn|Hn]|Hn]; auto; 
+ destruct (lt_eq_lt_dec n 0) as [[Hn|Hn]|Hn]; auto;
   destruct (lt_eq_lt_dec m 0) as [[Hm|Hm]|Hm]; auto; elimtype False.
 
  rewrite lt_0_neg' in Hn.
@@ -611,7 +611,7 @@ Module IntProperties (I:Int).
  exact (lt_irrefl 0).
  Qed.
 
- Lemma mult_le_compat : 
+ Lemma mult_le_compat :
    forall i j k l, i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l.
  Proof.
  intros.
@@ -624,9 +624,9 @@ Module IntProperties (I:Int).
 
  generalize (le_trans _ _ _ H2 H0); clear H0 H1 H2; intros.
  rewrite (mult_comm i), (mult_comm j).
- destruct (le_is_lt_or_eq _ _ H0); 
+ destruct (le_is_lt_or_eq _ _ H0);
   [ | subst; do 2 rewrite mult_0_l; apply le_refl].
- destruct (le_is_lt_or_eq _ _ H); 
+ destruct (le_is_lt_or_eq _ _ H);
   [ | subst; apply le_refl].
  apply lt_le_weak.
  apply mult_lt_compat_l; auto.
@@ -634,9 +634,9 @@ Module IntProperties (I:Int).
  subst i.
  rewrite mult_0_l.
  generalize (le_trans _ _ _ H2 H0); clear H0 H1 H2; intros.
- destruct (le_is_lt_or_eq _ _ H); 
+ destruct (le_is_lt_or_eq _ _ H);
   [ | subst; rewrite mult_0_l; apply le_refl].
- destruct (le_is_lt_or_eq _ _ H0); 
+ destruct (le_is_lt_or_eq _ _ H0);
   [ | subst; rewrite mult_comm, mult_0_l; apply le_refl].
  apply lt_le_weak.
  apply mult_lt_0_compat; auto.
@@ -766,7 +766,7 @@ Module IntProperties (I:Int).
  apply plus_lt_compat; auto.
  apply mult_lt_0_compat; auto.
  apply lt_trans with x; auto.
- Qed. 
+ Qed.
 
  Lemma OMEGA19 : forall x, x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1).
  Proof.
@@ -781,7 +781,7 @@ Module IntProperties (I:Int).
  apply opp_lt_compat; auto.
  Qed.
 
- Lemma mult_le_approx : 
+ Lemma mult_le_approx :
   forall n m p, n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.
  Proof.
  intros n m p.
@@ -850,7 +850,7 @@ Module IntOmega (I:Int).
 Import I.
 Module IP:=IntProperties(I).
 Import IP.
-   
+
 (* \subsubsection{Definition of reified integer expressions}
    Terms are either:
    \begin{itemize}
@@ -903,7 +903,7 @@ Inductive proposition : Set :=
   | Tprop : nat -> proposition.
 
 (* Definition of goals as a list of hypothesis *)
-Notation hyps := (list proposition).      
+Notation hyps := (list proposition).
 
 (* Definition of lists of subgoals  (set of open goals) *)
 Notation lhyps := (list hyps).
@@ -930,7 +930,7 @@ Inductive t_fusion : Set :=
   | F_right : t_fusion.
 
 (* \subsubsection{Rewriting steps to normalize terms} *)
-Inductive step : Set := 
+Inductive step : Set :=
   (* apply the rewriting steps to both subterms of an operation *)
   | C_DO_BOTH : step -> step -> step
   (* apply the rewriting step to the first branch *)
@@ -938,9 +938,9 @@ Inductive step : Set :=
   (* apply the rewriting step to the second branch *)
   | C_RIGHT : step -> step
   (* apply two steps consecutively to a term *)
-  | C_SEQ : step -> step -> step 
+  | C_SEQ : step -> step -> step
   (* empty step *)
-  | C_NOP : step 
+  | C_NOP : step
   (* the following operations correspond to actual rewriting *)
   | C_OPP_PLUS : step
   | C_OPP_OPP : step
@@ -990,8 +990,8 @@ Inductive t_omega : Set :=
   | O_STATE : int -> step -> nat -> nat -> t_omega -> t_omega.
 
 (* \subsubsection{Rules for normalizing the hypothesis} *)
-(* These rules indicate how to normalize useful propositions 
-   of each useful hypothesis before the decomposition of hypothesis. 
+(* These rules indicate how to normalize useful propositions
+   of each useful hypothesis before the decomposition of hypothesis.
    The rules include the inversion phase for negation removal. *)
 
 Inductive p_step : Set :=
@@ -1001,19 +1001,19 @@ Inductive p_step : Set :=
   | P_STEP : step -> p_step
   | P_NOP : p_step.
 
-(* List of normalizations to perform : with a constructor of type 
-   [p_step] allowing to visit both left and right branches, we would be  
-   able to restrict to only one normalization by hypothesis. 
-   And since all hypothesis are useful (otherwise they wouldn't be included), 
+(* List of normalizations to perform : with a constructor of type
+   [p_step] allowing to visit both left and right branches, we would be
+   able to restrict to only one normalization by hypothesis.
+   And since all hypothesis are useful (otherwise they wouldn't be included),
    we would be able to replace [h_step] by a simple list. *)
 
 Inductive h_step : Set :=
     pair_step : nat -> p_step -> h_step.
 
 (* \subsubsection{Rules for decomposing the hypothesis} *)
-(* This type allows to navigate in the logical constructors that 
-   form the predicats of the hypothesis in order to decompose them. 
-   This allows in particular to extract one hypothesis from a 
+(* This type allows to navigate in the logical constructors that
+   form the predicats of the hypothesis in order to decompose them.
+   This allows in particular to extract one hypothesis from a
    conjonction with possibly the right level of negations. *)
 
 Inductive direction : Set :=
@@ -1022,8 +1022,8 @@ Inductive direction : Set :=
   | D_mono : direction.
 
 (* This type allows to extract useful components from hypothesis, either
-   hypothesis generated by splitting a disjonction, or equations. 
-   The last constructor indicates how to solve the obtained system 
+   hypothesis generated by splitting a disjonction, or equations.
+   The last constructor indicates how to solve the obtained system
    via the use of the trace type of Omega [t_omega] *)
 
 Inductive e_step : Set :=
@@ -1032,10 +1032,10 @@ Inductive e_step : Set :=
   | E_SOLVE : t_omega -> e_step.
 
 (* \subsection{Efficient decidable equality} *)
-(* For each reified data-type, we define an efficient equality test. 
+(* For each reified data-type, we define an efficient equality test.
    It is not the one produced by [Decide Equality].
-   
-   Then we prove two theorem allowing to eliminate such equalities : 
+
+   Then we prove two theorem allowing to eliminate such equalities :
    \begin{verbatim}
    (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2.
    (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2.
@@ -1056,21 +1056,21 @@ Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
   | _, _ => false
   end.
 
-Close Scope romega_scope.  
+Close Scope romega_scope.
 
 Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2.
 Proof.
  simple induction t1; intros until t2; case t2; simpl in *;
- try (intros; discriminate; fail); 
+ try (intros; discriminate; fail);
  [ intros; elim beq_true with (1 := H); trivial
  | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
-    elim H with (1 := H4); elim H0 with (1 := H5); 
+    elim H with (1 := H4); elim H0 with (1 := H5);
     trivial
  | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
-    elim H with (1 := H4); elim H0 with (1 := H5); 
+    elim H with (1 := H4); elim H0 with (1 := H5);
     trivial
  | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
-    elim H with (1 := H4); elim H0 with (1 := H5); 
+    elim H with (1 := H4); elim H0 with (1 := H5);
     trivial
  | intros t21 H3; elim H with (1 := H3); trivial
  | intros; elim beq_nat_true with (1 := H); trivial ].
@@ -1083,7 +1083,7 @@ Theorem eq_term_false :
 Proof.
  simple induction t1;
  [ intros z t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *;
-    intros; elim beq_false with (1 := H); simplify_eq H0; 
+    intros; elim beq_false with (1 := H); simplify_eq H0;
     auto
  | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *;
     intros t21 t22 H3; unfold not in |- *; intro H4;
@@ -1101,21 +1101,21 @@ Proof.
     [ elim H1 with (1 := H5); simplify_eq H4; auto
     | elim H2 with (1 := H5); simplify_eq H4; auto ]
  | intros t11 H1 t2; case t2; try trivial_case; simpl in |- *; intros t21 H3;
-    unfold not in |- *; intro H4; elim H1 with (1 := H3); 
+    unfold not in |- *; intro H4; elim H1 with (1 := H3);
     simplify_eq H4; auto
  | intros n t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *;
-    intros; elim beq_nat_false with (1 := H); simplify_eq H0; 
+    intros; elim beq_nat_false with (1 := H); simplify_eq H0;
     auto ].
 Qed.
 
-(* \subsubsection{Tactiques pour éliminer ces tests} 
+(* \subsubsection{Tactiques pour éliminer ces tests}
 
-   Si on se contente de faire un [Case (eq_typ t1 t2)] on perd 
+   Si on se contente de faire un [Case (eq_typ t1 t2)] on perd
    totalement dans chaque branche le fait que [t1=t2] ou [~t1=t2].
 
    Initialement, les développements avaient été réalisés avec les
    tests rendus par [Decide Equality], c'est à dire un test rendant
-   des termes du type [{t1=t2}+{~t1=t2}]. Faire une élimination sur un 
+   des termes du type [{t1=t2}+{~t1=t2}]. Faire une élimination sur un
    tel test préserve bien l'information voulue mais calculatoirement de
    telles fonctions sont trop lentes. *)
 
@@ -1132,8 +1132,8 @@ Ltac elim_beq t1 t2 :=
    [ generalize (beq_true t1 t2 Aux); clear Aux
    | generalize (beq_false t1 t2 Aux); clear Aux ].
 
-Ltac elim_bgt t1 t2 := 
-  pattern (bgt t1 t2) in |- *; apply bool_eq_ind; intro Aux; 
+Ltac elim_bgt t1 t2 :=
+  pattern (bgt t1 t2) in |- *; apply bool_eq_ind; intro Aux;
   [ generalize (bgt_true t1 t2 Aux); clear Aux
   | generalize (bgt_false t1 t2 Aux); clear Aux ].
 
@@ -1151,7 +1151,7 @@ Fixpoint interp_term (env : list int) (t : term) {struct t} : int :=
   | [n]%term => nth n env 0
   end.
 
-(* \subsubsection{Interprétation des prédicats} *) 
+(* \subsubsection{Interprétation des prédicats} *)
 
 Fixpoint interp_proposition (envp : list Prop) (env : list int)
  (p : proposition) {struct p} : Prop :=
@@ -1179,7 +1179,7 @@ Fixpoint interp_proposition (envp : list Prop) (env : list int)
    Interprétation sous forme d'une conjonction d'hypothèses plus faciles
    à manipuler individuellement *)
 
-Fixpoint interp_hyps (envp : list Prop) (env : list int) 
+Fixpoint interp_hyps (envp : list Prop) (env : list int)
  (l : hyps) {struct l} : Prop :=
   match l with
   | nil => True
@@ -1191,7 +1191,7 @@ Fixpoint interp_hyps (envp : list Prop) (env : list int)
    [Generalize] et qu'une conjonction est forcément lourde (répétition des
    types dans les conjonctions intermédiaires) *)
 
-Fixpoint interp_goal_concl (c : proposition) (envp : list Prop) 
+Fixpoint interp_goal_concl (c : proposition) (envp : list Prop)
  (env : list int) (l : hyps) {struct l} : Prop :=
   match l with
   | nil => interp_proposition envp env c
@@ -1219,7 +1219,7 @@ Theorem hyps_to_goal :
 Proof.
  simple induction l; simpl in |- *; [ auto | intros; apply H; elim H1; auto ].
 Qed.
-      
+
 (* \subsection{Manipulations sur les hypothèses} *)
 
 (* \subsubsection{Définitions de base de stabilité pour la réflexion} *)
@@ -1228,7 +1228,7 @@ Definition term_stable (f : term -> term) :=
   forall (e : list int) (t : term), interp_term e t = interp_term e (f t).
 
 (* Une opération est valide sur une hypothèse, si l'hypothèse implique le
-   résultat de l'opération. \emph{Attention : cela ne concerne que des 
+   résultat de l'opération. \emph{Attention : cela ne concerne que des
    opérations sur les hypothèses et non sur les buts (contravariance)}.
    On définit la validité pour une opération prenant une ou deux propositions
    en argument (cela suffit pour omega). *)
@@ -1242,15 +1242,15 @@ Definition valid2 (f : proposition -> proposition -> proposition) :=
   interp_proposition ep e p1 ->
   interp_proposition ep e p2 -> interp_proposition ep e (f p1 p2).
 
-(* Dans cette notion de validité, la fonction prend directement une 
-   liste de propositions et rend une nouvelle liste de proposition. 
+(* Dans cette notion de validité, la fonction prend directement une
+   liste de propositions et rend une nouvelle liste de proposition.
    On reste contravariant *)
 
 Definition valid_hyps (f : hyps -> hyps) :=
   forall (ep : list Prop) (e : list int) (lp : hyps),
   interp_hyps ep e lp -> interp_hyps ep e (f lp).
 
-(* Enfin ce théorème élimine la contravariance et nous ramène à une 
+(* Enfin ce théorème élimine la contravariance et nous ramène à une
    opération sur les buts *)
 
 Theorem valid_goal :
@@ -1264,14 +1264,14 @@ Qed.
 (* \subsubsection{Généralisation a des listes de buts (disjonctions)} *)
 
 
-Fixpoint interp_list_hyps (envp : list Prop) (env : list int) 
+Fixpoint interp_list_hyps (envp : list Prop) (env : list int)
  (l : lhyps) {struct l} : Prop :=
   match l with
   | nil => False
   | h :: l' => interp_hyps envp env h \/ interp_list_hyps envp env l'
   end.
 
-Fixpoint interp_list_goal (envp : list Prop) (env : list int) 
+Fixpoint interp_list_goal (envp : list Prop) (env : list int)
  (l : lhyps) {struct l} : Prop :=
   match l with
   | nil => True
@@ -1311,10 +1311,10 @@ Theorem goal_valid :
  forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f.
 Proof.
  unfold valid_list_goal in |- *; intros f H ep e lp H1; apply goal_to_hyps;
- intro H2; apply list_hyps_to_goal with (1 := H1); 
+ intro H2; apply list_hyps_to_goal with (1 := H1);
  apply (H ep e lp); assumption.
 Qed.
- 
+
 Theorem append_valid :
  forall (ep : list Prop) (e : list int) (l1 l2 : lhyps),
  interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 ->
@@ -1345,7 +1345,7 @@ Proof.
     | intros; simpl in |- *; apply H; elim H1; auto ] ].
 Qed.
 
-(* Appliquer une opération (valide) sur deux hypothèses extraites de 
+(* Appliquer une opération (valide) sur deux hypothèses extraites de
    la liste et ajouter le résultat à la liste. *)
 Definition apply_oper_2 (i j : nat)
   (f : proposition -> proposition -> proposition) (l : hyps) :=
@@ -1361,7 +1361,7 @@ Qed.
 
 (* Modifier une hypothèse par application d'une opération valide *)
 
-Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition) 
+Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition)
  (l : hyps) {struct i} : hyps :=
   match l with
   | nil => nil (A:=proposition)
@@ -1390,7 +1390,7 @@ Qed.
 (* \subsubsection{Manipulations de termes} *)
 (* Les fonctions suivantes permettent d'appliquer une fonction de
    réécriture sur un sous terme du terme principal. Avec la composition,
-   cela permet de construire des réécritures complexes proches des 
+   cela permet de construire des réécritures complexes proches des
    tactiques de conversion *)
 
 Definition apply_left (f : term -> term) (t : term) :=
@@ -1415,7 +1415,7 @@ Definition apply_both (f g : term -> term) (t : term) :=
   | x => x
   end.
 
-(* Les théorèmes suivants montrent la stabilité (conditionnée) des 
+(* Les théorèmes suivants montrent la stabilité (conditionnée) des
    fonctions. *)
 
 Theorem apply_left_stable :
@@ -1448,21 +1448,21 @@ Proof.
 Qed.
 
 (* \subsection{Les règles de réécriture} *)
-(* Chacune des règles de réécriture est accompagnée par sa preuve de 
-   stabilité. Toutes ces preuves ont la même forme : il faut analyser 
+(* Chacune des règles de réécriture est accompagnée par sa preuve de
+   stabilité. Toutes ces preuves ont la même forme : il faut analyser
    suivant la forme du terme (élimination de chaque Case). On a besoin d'une
-   élimination uniquement dans les cas d'utilisation d'égalité décidable. 
+   élimination uniquement dans les cas d'utilisation d'égalité décidable.
 
    Cette tactique itère la décomposition des Case. Elle est
    constituée de deux fonctions s'appelant mutuellement :
-   \begin{itemize} 
+   \begin{itemize}
     \item une fonction d'enrobage qui lance la recherche sur le but,
     \item une fonction récursive qui décompose ce but. Quand elle a trouvé un
-          Case, elle l'élimine. 
-   \end{itemize}  
+          Case, elle l'élimine.
+   \end{itemize}
    Les motifs sur les cas sont très imparfaits et dans certains cas, il
    semble que cela ne marche pas. On aimerait plutot un motif de la
-   forme [ Case (?1 :: T) of _ end ] permettant de s'assurer que l'on 
+   forme [ Case (?1 :: T) of _ end ] permettant de s'assurer que l'on
    utilise le bon type.
 
    Chaque élimination introduit correctement exactement le nombre d'hypothèses
@@ -1520,15 +1520,15 @@ Ltac loop t :=
     | [x]%term => _
     end => destruct X1; auto; Simplify
   | (if beq ?X1 ?X2 then _ else _) =>
-      let H := fresh "H" in 
+      let H := fresh "H" in
       elim_beq X1 X2; intro H; try (rewrite H in *; clear H);
        simpl in |- *; auto; Simplify
   | (if bgt ?X1 ?X2 then _ else _) =>
-      let H := fresh "H" in 
+      let H := fresh "H" in
       elim_bgt X1 X2; intro H; simpl in |- *; auto; Simplify
   | (if eq_term ?X1 ?X2 then _ else _) =>
-      let H := fresh "H" in 
-      elim_eq_term X1 X2; intro H; try (rewrite H in *; clear H); 
+      let H := fresh "H" in
+      elim_eq_term X1 X2; intro H; try (rewrite H in *; clear H);
        simpl in |- *; auto; Simplify
   | (if _ && _ then _ else _) => rewrite andb_if; Simplify
   | (if negb _ then _ else _) => rewrite negb_if; Simplify
@@ -1617,7 +1617,7 @@ Qed.
 Definition T_OMEGA10 (t : term) :=
   match t with
   | ((v * Tint c1 + l1) * Tint k1 + (v' * Tint c2 + l2) * Tint k2)%term =>
-      if eq_term v v' 
+      if eq_term v v'
       then (v * Tint (c1 * k1 + c2 * k2)%I + (l1 * Tint k1 + l2 * Tint k2))%term
       else t
   | _ => t
@@ -1650,12 +1650,12 @@ Definition T_OMEGA12 (t : term) :=
 Theorem T_OMEGA12_stable : term_stable T_OMEGA12.
 Proof.
  prove_stable T_OMEGA12 OMEGA12.
-Qed. 
+Qed.
 
 Definition T_OMEGA13 (t : term) :=
   match t with
   | (v * Tint x + l1 + (v' * Tint x' + l2))%term =>
-      if eq_term v v' && beq x (-x') 
+      if eq_term v v' && beq x (-x')
       then (l1+l2)%term
       else t
   | _ => t
@@ -1670,7 +1670,7 @@ Qed.
 Definition T_OMEGA15 (t : term) :=
   match t with
   | (v * Tint c1 + l1 + (v' * Tint c2 + l2) * Tint k2)%term =>
-      if eq_term v v' 
+      if eq_term v v'
       then (v * Tint (c1 + c2 * k2)%I + (l1 + l2 * Tint k2))%term
       else t
   | _ => t
@@ -1792,9 +1792,9 @@ Qed.
 Definition Tred_factor1 (t : term) :=
   match t with
   | (x + y)%term =>
-      if eq_term x y 
+      if eq_term x y
       then (x * Tint 2)%term
-      else t 
+      else t
   | _ => t
   end.
 
@@ -1806,7 +1806,7 @@ Qed.
 Definition Tred_factor2 (t : term) :=
   match t with
   | (x + y * Tint k)%term =>
-      if eq_term x y 
+      if eq_term x y
       then (x * Tint (1 + k))%term
       else t
   | _ => t
@@ -1820,7 +1820,7 @@ Qed.
 Definition Tred_factor3 (t : term) :=
   match t with
   | (x * Tint k + y)%term =>
-      if eq_term x y 
+      if eq_term x y
       then (x * Tint (1 + k))%term
       else t
   | _ => t
@@ -1835,7 +1835,7 @@ Qed.
 Definition Tred_factor4 (t : term) :=
   match t with
   | (x * Tint k1 + y * Tint k2)%term =>
-      if eq_term x y 
+      if eq_term x y
       then (x * Tint (k1 + k2))%term
       else t
   | _ => t
@@ -1919,13 +1919,13 @@ Proof.
       | intros; auto
       | intros; auto
       | intros; auto
-      | intros; auto ])); intros t0 H0; simpl in |- *; 
+      | intros; auto ])); intros t0 H0; simpl in |- *;
  rewrite H0; case (reduce t0); intros; auto.
 Qed.
 
 (* \subsubsection{Fusions}
     \paragraph{Fusion de deux équations} *)
-(* On donne une somme de deux équations qui sont supposées normalisées. 
+(* On donne une somme de deux équations qui sont supposées normalisées.
    Cette fonction prend une trace de fusion en argument et transforme
    le terme en une équation normalisée. C'est une version très simplifiée
    du moteur de réécriture [rewrite]. *)
@@ -1941,7 +1941,7 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term :=
       | F_right => apply_right (fusion trace') (T_OMEGA12 t)
       end
   end.
-    
+
 Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t).
 Proof.
  simple induction t; simpl in |- *;
@@ -1985,7 +1985,7 @@ Proof.
  unfold term_stable, fusion_cancel in |- *; intros trace e; elim trace;
  [ exact (reduce_stable e)
  | intros n H t; elim H; exact (T_OMEGA13_stable e t) ].
-Qed. 
+Qed.
 
 (* \subsubsection{Opérations affines sur une équation} *)
 (* \paragraph{Multiplication scalaire et somme d'une constante} *)
@@ -2004,7 +2004,7 @@ Proof.
  | intros n H e t; elim apply_right_stable;
     [ exact (T_OMEGA11_stable e t) | exact H ] ].
 Qed.
-   
+
 (* \paragraph{Multiplication scalaire} *)
 Fixpoint scalar_norm (trace : nat) (t : term) {struct trace} : term :=
   match trace with
@@ -2101,8 +2101,8 @@ Proof.
  | exact Tmult_comm_stable ].
 Qed.
 
-(* \subsection{tactiques de résolution d'un but omega normalisé} 
-   Trace de la procédure 
+(* \subsection{tactiques de résolution d'un but omega normalisé}
+   Trace de la procédure
 \subsubsection{Tactiques générant une contradiction}
 \paragraph{[O_CONSTANT_NOT_NUL]} *)
 
@@ -2117,17 +2117,17 @@ Theorem constant_not_nul_valid :
  forall i : nat, valid_hyps (constant_not_nul i).
 Proof.
  unfold valid_hyps, constant_not_nul in |- *; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl in |- *. 
- 
- elim_beq i1 i0; auto; simpl in |- *; intros H1 H2; 
+ generalize (nth_valid ep e i lp); Simplify; simpl in |- *.
+
+ elim_beq i1 i0; auto; simpl in |- *; intros H1 H2;
  elim H1; symmetry  in |- *; auto.
-Qed.   
+Qed.
 
 (* \paragraph{[O_CONSTANT_NEG]} *)
 
 Definition constant_neg (i : nat) (h : hyps) :=
   match nth_hyps i h with
-  | LeqTerm (Tint Nul) (Tint Neg) => 
+  | LeqTerm (Tint Nul) (Tint Neg) =>
      if bgt Nul Neg then absurd else h
   | _ => h
   end.
@@ -2140,14 +2140,14 @@ Proof.
 Qed.
 
 (* \paragraph{[NOT_EXACT_DIVIDE]} *)
-Definition not_exact_divide (k1 k2 : int) (body : term) 
+Definition not_exact_divide (k1 k2 : int) (body : term)
   (t i : nat) (l : hyps) :=
   match nth_hyps i l with
   | EqTerm (Tint Nul) b =>
-      if beq Nul 0 && 
-         eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b && 
-         bgt k2 0 && 
-         bgt k1 k2 
+      if beq Nul 0 &&
+         eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b &&
+         bgt k2 0 &&
+         bgt k1 k2
       then absurd
       else l
   | _ => l
@@ -2161,7 +2161,7 @@ Proof.
  generalize (nth_valid ep e i lp); Simplify.
  rewrite (scalar_norm_add_stable t e), <-H1.
  do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros.
- absurd (interp_term e body * k1 + k2 = 0); 
+ absurd (interp_term e body * k1 + k2 = 0);
  [ now apply OMEGA4 | symmetry; auto ].
 Qed.
 
@@ -2173,8 +2173,8 @@ Definition contradiction (t i j : nat) (l : hyps) :=
       match nth_hyps j l with
       | LeqTerm (Tint Nul') b2 =>
           match fusion_cancel t (b1 + b2)%term with
-          | Tint k => if beq Nul 0 && beq Nul' 0 && bgt 0 k 
-                      then absurd 
+          | Tint k => if beq Nul 0 && beq Nul' 0 && bgt 0 k
+                      then absurd
                       else l
           | _ => l
           end
@@ -2188,16 +2188,16 @@ Theorem contradiction_valid :
 Proof.
  unfold valid_hyps, contradiction in |- *; intros t i j ep e l H;
  generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
- case (nth_hyps i l); auto; intros t1 t2; case t1; 
- auto; case (nth_hyps j l); 
- auto; intros t3 t4; case t3; auto; 
+ case (nth_hyps i l); auto; intros t1 t2; case t1;
+ auto; case (nth_hyps j l);
+ auto; intros t3 t4; case t3; auto;
  simpl in |- *; intros z z' H1 H2;
  generalize (refl_equal (interp_term e (fusion_cancel t (t2 + t4)%term)));
  pattern (fusion_cancel t (t2 + t4)%term) at 2 3 in |- *;
- case (fusion_cancel t (t2 + t4)%term); simpl in |- *; 
+ case (fusion_cancel t (t2 + t4)%term); simpl in |- *;
  auto; intro k; elim (fusion_cancel_stable t); simpl in |- *.
  Simplify; intro H3.
- generalize (OMEGA2 _ _ H2 H1); rewrite H3. 
+ generalize (OMEGA2 _ _ H2 H1); rewrite H3.
  rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition.
 Qed.
 
@@ -2208,17 +2208,17 @@ Definition negate_contradict (i1 i2 : nat) (h : hyps) :=
   | EqTerm (Tint Nul) b1 =>
       match nth_hyps i2 h with
       | NeqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2 
-          then absurd 
+          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2
+          then absurd
           else h
       | _ => h
       end
   | NeqTerm (Tint Nul) b1 =>
       match nth_hyps i2 h with
       | EqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2 
-          then absurd 
-          else h 
+          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2
+          then absurd
+          else h
       | _ => h
       end
   | _ => h
@@ -2229,7 +2229,7 @@ Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) :=
   | EqTerm (Tint Nul) b1 =>
       match nth_hyps i2 h with
       | NeqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 && 
+          if beq Nul 0 && beq Nul' 0 &&
              eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
           then absurd
           else h
@@ -2238,7 +2238,7 @@ Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) :=
   | NeqTerm (Tint Nul) b1 =>
       match nth_hyps i2 h with
       | EqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 && 
+          if beq Nul 0 && beq Nul' 0 &&
              eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
           then absurd
           else h
@@ -2252,9 +2252,9 @@ Theorem negate_contradict_valid :
 Proof.
  unfold valid_hyps, negate_contradict in |- *; intros i j ep e l H;
  generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
- case (nth_hyps i l); auto; intros t1 t2; case t1; 
- auto; intros z; auto; case (nth_hyps j l); 
- auto; intros t3 t4; case t3; auto; intros z'; 
+ case (nth_hyps i l); auto; intros t1 t2; case t1;
+ auto; intros z; auto; case (nth_hyps j l);
+ auto; intros t3 t4; case t3; auto; intros z';
  auto; simpl in |- *; intros H1 H2; Simplify.
 Qed.
 
@@ -2263,15 +2263,15 @@ Theorem negate_contradict_inv_valid :
 Proof.
  unfold valid_hyps, negate_contradict_inv in |- *; intros t i j ep e l H;
  generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
- case (nth_hyps i l); auto; intros t1 t2; case t1; 
- auto; intros z; auto; case (nth_hyps j l); 
- auto; intros t3 t4; case t3; auto; intros z'; 
- auto; simpl in |- *; intros H1 H2; Simplify; 
+ case (nth_hyps i l); auto; intros t1 t2; case t1;
+ auto; intros z; auto; case (nth_hyps j l);
+ auto; intros t3 t4; case t3; auto; intros z';
+ auto; simpl in |- *; intros H1 H2; Simplify;
  [
  rewrite <- scalar_norm_stable in H2; simpl in *;
  elim (mult_integral (interp_term e t4) (-(1))); intuition;
  elim minus_one_neq_zero; auto
- | 
+ |
  elim H2; clear H2;
  rewrite <- scalar_norm_stable; simpl in *;
  now rewrite <- H1, mult_0_l
@@ -2282,7 +2282,7 @@ Qed.
 (* \paragraph{[O_SUM]}
  C'est une oper2 valide mais elle traite plusieurs cas à la fois (suivant
  les opérateurs de comparaison des deux arguments) d'où une
- preuve un peu compliquée. On utilise quelques lemmes qui sont des 
+ preuve un peu compliquée. On utilise quelques lemmes qui sont des
  généralisations des théorèmes utilisés par OMEGA. *)
 
 Definition sum (k1 k2 : int) (trace : list t_fusion)
@@ -2291,11 +2291,11 @@ Definition sum (k1 k2 : int) (trace : list t_fusion)
   | EqTerm (Tint Null) b1 =>
       match prop2 with
       | EqTerm (Tint Null') b2 =>
-          if beq Null 0 && beq Null' 0 
+          if beq Null 0 && beq Null' 0
           then EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
           else TrueTerm
       | LeqTerm (Tint Null') b2 =>
-          if beq Null 0 && beq Null' 0 && bgt k2 0 
+          if beq Null 0 && beq Null' 0 && bgt k2 0
           then LeqTerm (Tint 0)
                 (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
           else TrueTerm
@@ -2305,18 +2305,18 @@ Definition sum (k1 k2 : int) (trace : list t_fusion)
       if beq Null 0 && bgt k1 0
       then match prop2 with
           | EqTerm (Tint Null') b2 =>
-              if beq Null' 0 then 
+              if beq Null' 0 then
               LeqTerm (Tint 0)
                 (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
-              else TrueTerm  
+              else TrueTerm
           | LeqTerm (Tint Null') b2 =>
-              if beq Null' 0 && bgt k2 0 
+              if beq Null' 0 && bgt k2 0
               then LeqTerm (Tint 0)
                     (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
               else TrueTerm
           | _ => TrueTerm
           end
-      else TrueTerm 
+      else TrueTerm
   | NeqTerm (Tint Null) b1 =>
       match prop2 with
       | EqTerm (Tint Null') b2 =>
@@ -2334,7 +2334,7 @@ Theorem sum_valid :
  forall (k1 k2 : int) (t : list t_fusion), valid2 (sum k1 k2 t).
 Proof.
  unfold valid2 in |- *; intros k1 k2 t ep e p1 p2; unfold sum in |- *;
- Simplify; simpl in |- *; auto; try elim (fusion_stable t); 
+ Simplify; simpl in |- *; auto; try elim (fusion_stable t);
  simpl in |- *; intros;
  [ apply sum1; assumption
  | apply sum2; try assumption; apply sum4; assumption
@@ -2350,13 +2350,13 @@ Definition exact_divide (k : int) (body : term) (t : nat)
   (prop : proposition) :=
   match prop with
   | EqTerm (Tint Null) b =>
-      if beq Null 0 && 
-         eq_term (scalar_norm t (body * Tint k)%term) b && 
-         negb (beq k 0) 
+      if beq Null 0 &&
+         eq_term (scalar_norm t (body * Tint k)%term) b &&
+         negb (beq k 0)
       then EqTerm (Tint 0) body
       else TrueTerm
   | NeqTerm (Tint Null) b =>
-      if beq Null 0 && 
+      if beq Null 0 &&
          eq_term (scalar_norm t (body * Tint k)%term) b &&
          negb (beq k 0)
       then NeqTerm (Tint 0) body
@@ -2367,8 +2367,8 @@ Definition exact_divide (k : int) (body : term) (t : nat)
 Theorem exact_divide_valid :
  forall (k : int) (t : term) (n : nat), valid1 (exact_divide k t n).
 Proof.
- unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; 
- Simplify; simpl; auto; subst; 
+ unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1;
+ Simplify; simpl; auto; subst;
  rewrite <- scalar_norm_stable; simpl; intros;
  [ destruct (mult_integral _ _ (sym_eq H0)); intuition
  | contradict H0; rewrite <- H0, mult_0_l; auto
@@ -2380,15 +2380,15 @@ Qed.
   La preuve reprend le schéma de la précédente mais on
   est sur une opération de type valid1 et non sur une opération terminale. *)
 
-Definition divide_and_approx (k1 k2 : int) (body : term) 
+Definition divide_and_approx (k1 k2 : int) (body : term)
   (t : nat) (prop : proposition) :=
   match prop with
   | LeqTerm (Tint Null) b =>
-      if beq Null 0 && 
+      if beq Null 0 &&
          eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b &&
-         bgt k1 0 && 
-         bgt k1 k2 
-      then LeqTerm (Tint 0) body 
+         bgt k1 0 &&
+         bgt k1 k2
+      then LeqTerm (Tint 0) body
       else prop
   | _ => prop
   end.
@@ -2411,7 +2411,7 @@ Definition merge_eq (t : nat) (prop1 prop2 : proposition) :=
       match prop2 with
       | LeqTerm (Tint Null') b2 =>
           if beq Null 0 && beq Null' 0 &&
-             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term) 
+             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
           then EqTerm (Tint 0) b1
           else TrueTerm
       | _ => TrueTerm
@@ -2422,7 +2422,7 @@ Definition merge_eq (t : nat) (prop1 prop2 : proposition) :=
 Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n).
 Proof.
  unfold valid2, merge_eq in |- *; intros n ep e p1 p2; Simplify; simpl in |- *;
- auto; elim (scalar_norm_stable n e); simpl in |- *; 
+ auto; elim (scalar_norm_stable n e); simpl in |- *;
  intros; symmetry  in |- *; apply OMEGA8 with (2 := H0);
  [ assumption | elim opp_eq_mult_neg_1; trivial ].
 Qed.
@@ -2433,8 +2433,8 @@ Qed.
 
 Definition constant_nul (i : nat) (h : hyps) :=
   match nth_hyps i h with
-  | NeqTerm (Tint Null) (Tint Null') => 
-      if beq Null Null' then absurd else h 
+  | NeqTerm (Tint Null) (Tint Null') =>
+      if beq Null Null' then absurd else h
   | _ => h
   end.
 
@@ -2452,7 +2452,7 @@ Definition state (m : int) (s : step) (prop1 prop2 : proposition) :=
   | EqTerm (Tint Null) b1 =>
       match prop2 with
       | EqTerm b2 b3 =>
-          if beq Null 0 
+          if beq Null 0
           then EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term)
           else TrueTerm
       | _ => TrueTerm
@@ -2463,20 +2463,20 @@ Definition state (m : int) (s : step) (prop1 prop2 : proposition) :=
 Theorem state_valid : forall (m : int) (s : step), valid2 (state m s).
 Proof.
  unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify;
- simpl in |- *; auto; elim (rewrite_stable s e); simpl in |- *; 
+ simpl in |- *; auto; elim (rewrite_stable s e); simpl in |- *;
  intros H1 H2; elim H1.
  now rewrite H2, plus_opp_l, plus_0_l, mult_0_l.
 Qed.
 
 (* \subsubsection{Tactiques générant plusieurs but}
-   \paragraph{[O_SPLIT_INEQ]} 
+   \paragraph{[O_SPLIT_INEQ]}
    La seule pour le moment (tant que la normalisation n'est pas réfléchie). *)
 
-Definition split_ineq (i t : nat) (f1 f2 : hyps -> lhyps) 
+Definition split_ineq (i t : nat) (f1 f2 : hyps -> lhyps)
   (l : hyps) :=
   match nth_hyps i l with
   | NeqTerm (Tint Null) b1 =>
-      if beq Null 0 then 
+      if beq Null 0 then
       f1 (LeqTerm (Tint 0) (add_norm t (b1 + Tint (-(1)))%term) :: l) ++
       f2
         (LeqTerm (Tint 0)
@@ -2491,8 +2491,8 @@ Theorem split_ineq_valid :
  valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2).
 Proof.
  unfold valid_list_hyps, split_ineq in |- *; intros i t f1 f2 H1 H2 ep e lp H;
- generalize (nth_valid _ _ i _ H); case (nth_hyps i lp); 
- simpl in |- *; auto; intros t1 t2; case t1; simpl in |- *; 
+ generalize (nth_valid _ _ i _ H); case (nth_hyps i lp);
+ simpl in |- *; auto; intros t1 t2; case t1; simpl in |- *;
  auto; intros z; simpl in |- *; auto; intro H3.
  Simplify.
  apply append_valid; elim (OMEGA19 (interp_term e t2));
@@ -2580,7 +2580,7 @@ Proof.
 Qed.
 
 
-(* \subsection{Les opérations globales sur le but} 
+(* \subsection{Les opérations globales sur le but}
    \subsubsection{Normalisation} *)
 
 Definition move_right (s : step) (p : proposition) :=
@@ -2615,7 +2615,7 @@ Proof.
  apply move_right_valid.
 Qed.
 
-Fixpoint do_normalize_list (l : list step) (i : nat) 
+Fixpoint do_normalize_list (l : list step) (i : nat)
  (h : hyps) {struct l} : hyps :=
   match l with
   | s :: l' => do_normalize_list l' (S i) (do_normalize i s h)
@@ -2659,7 +2659,7 @@ Proof.
 Qed.
 
 (* A simple decidability checker : if the proposition belongs to the
-   simple grammar describe below then it is decidable. Proof is by 
+   simple grammar describe below then it is decidable. Proof is by
    induction and uses well known theorem about arithmetic and propositional
    calculus *)
 
@@ -2703,7 +2703,7 @@ Qed.
 (* An interpretation function for a complete goal with an explicit
    conclusion. We use an intermediate fixpoint. *)
 
-Fixpoint interp_full_goal (envp : list Prop) (env : list int) 
+Fixpoint interp_full_goal (envp : list Prop) (env : list int)
  (c : proposition) (l : hyps) {struct l} : Prop :=
   match l with
   | nil => interp_proposition envp env c
@@ -2711,7 +2711,7 @@ Fixpoint interp_full_goal (envp : list Prop) (env : list int)
       interp_proposition envp env p' -> interp_full_goal envp env c l'
   end.
 
-Definition interp_full (ep : list Prop) (e : list int) 
+Definition interp_full (ep : list Prop) (e : list int)
   (lc : hyps * proposition) : Prop :=
   match lc with
   | (l, c) => interp_full_goal ep e c l
@@ -2729,7 +2729,7 @@ Proof.
 Qed.
 
 (* Push the conclusion in the list of hypothesis using a double negation
-   If the decidability cannot be "proven", then just forget about the 
+   If the decidability cannot be "proven", then just forget about the
    conclusion (equivalent of replacing it with false) *)
 
 Definition to_contradict (lc : hyps * proposition) :=
@@ -2765,16 +2765,16 @@ Fixpoint map_cons (A : Set) (x : A) (l : list (list A)) {struct l} :
   | l :: ll => (x :: l) :: map_cons A x ll
   end.
 
-(* This function breaks up a list of hypothesis in a list of simpler 
+(* This function breaks up a list of hypothesis in a list of simpler
    list of hypothesis that together implie the original one. The goal
-   of all this is to transform the goal in a list of solvable problems. 
+   of all this is to transform the goal in a list of solvable problems.
    Note that :
 	- we need a way to drive the analysis as some hypotheis may not
-          require a split. 
+          require a split.
         - this procedure must be perfectly mimicked by the ML part otherwise
           hypothesis will get desynchronised and this will be a mess.
  *)
- 
+
 Fixpoint destructure_hyps (nn : nat) (ll : hyps) {struct nn} : lhyps :=
   match nn with
   | O => ll :: nil
@@ -2834,7 +2834,7 @@ Proof.
            (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0;
              auto);
           [ simpl in |- *; intros p1 (H1, H2);
-             pattern (decidability p1) in |- *; apply bool_eq_ind; 
+             pattern (decidability p1) in |- *; apply bool_eq_ind;
              intro H3;
              [ apply H; simpl in |- *; split;
                 [ apply not_not; auto | assumption ]
@@ -2842,7 +2842,7 @@ Proof.
           | simpl in |- *; intros p1 p2 (H1, H2); apply H; simpl in |- *;
              elim not_or with (1 := H1); auto
           | simpl in |- *; intros p1 p2 (H1, H2);
-             pattern (decidability p1) in |- *; apply bool_eq_ind; 
+             pattern (decidability p1) in |- *; apply bool_eq_ind;
              intro H3;
              [ apply append_valid; elim not_and with (2 := H1);
                 [ intro; left; apply H; simpl in |- *; auto
@@ -2850,11 +2850,11 @@ Proof.
                 | auto ]
              | auto ] ]
        | simpl in |- *; intros p1 p2 (H1, H2); apply append_valid;
-          (elim H1; intro H3; simpl in |- *; [ left | right ]); 
+          (elim H1; intro H3; simpl in |- *; [ left | right ]);
           apply H; simpl in |- *; auto
        | simpl in |- *; intros; apply H; simpl in |- *; tauto
        | simpl in |- *; intros p1 p2 (H1, H2);
-          pattern (decidability p1) in |- *; apply bool_eq_ind; 
+          pattern (decidability p1) in |- *; apply bool_eq_ind;
           intro H3;
           [ apply append_valid; elim imp_simp with (2 := H1);
              [ intro H4; left; simpl in |- *; apply H; simpl in |- *; auto
@@ -2867,7 +2867,7 @@ Definition prop_stable (f : proposition -> proposition) :=
   forall (ep : list Prop) (e : list int) (p : proposition),
   interp_proposition ep e p <-> interp_proposition ep e (f p).
 
-Definition p_apply_left (f : proposition -> proposition) 
+Definition p_apply_left (f : proposition -> proposition)
   (p : proposition) :=
   match p with
   | Timp x y => Timp (f x) y
@@ -2907,7 +2907,7 @@ Proof.
    | intros p1 p2; elim (H ep e p2); tauto ]).
 Qed.
 
-Definition p_invert (f : proposition -> proposition) 
+Definition p_invert (f : proposition -> proposition)
   (p : proposition) :=
   match p with
   | EqTerm x y => Tnot (f (NeqTerm x y))
@@ -2960,7 +2960,7 @@ Proof.
  | case p; simpl in |- *; intros; auto; generalize H; elim (rewrite_stable s);
     simpl in |- *; intro H1;
     [ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1;
-       rewrite plus_permute; rewrite plus_opp_r; 
+       rewrite plus_permute; rewrite plus_opp_r;
        rewrite plus_0_r; trivial
     | apply (fun a b => plus_le_reg_r a b (- interp_term e t));
        rewrite plus_opp_r; assumption
@@ -3037,7 +3037,7 @@ Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} :
                    end
   | _ => p
   end
- 
+
  with extract_hyp_neg (s : list direction) (p : proposition) {struct s} :
  proposition :=
   match s with
@@ -3087,7 +3087,7 @@ Proof.
       (apply H2; tauto) ||
         (pattern (decidability p0) in |- *; apply bool_eq_ind;
           [ intro H3; generalize (decidable_correct ep e p0 H3);
-             unfold decidable in |- *; intro H4; apply H1; 
+             unfold decidable in |- *; intro H4; apply H1;
              tauto
           | intro; tauto ]) ].
 Qed.
@@ -3103,8 +3103,8 @@ Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
            decompose_solve s1 (Tnot x :: h) ++
            decompose_solve s2 (Tnot y :: h)
           else h :: nil
-      | Timp x y => 
-          if decidability x then 
+      | Timp x y =>
+          if decidability x then
             decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (y :: h)
           else h::nil
       | _ => h :: nil
@@ -3130,11 +3130,11 @@ Proof.
           | simpl in |- *; auto ]
        | intros p1 p2 H2; apply append_valid; simpl in |- *; elim H2;
           [ intros H3; left; apply H; simpl in |- *; auto
-          | intros H3; right; apply H0; simpl in |- *; auto ] 
+          | intros H3; right; apply H0; simpl in |- *; auto ]
        | intros p1 p2 H2;
          pattern (decidability p1) in |- *; apply bool_eq_ind;
           [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4;
-             apply append_valid; elim H4; intro H5; 
+             apply append_valid; elim H4; intro H5;
              [ right; apply H0; simpl in |- *; tauto
              | left; apply H; simpl in |- *; tauto ]
           | simpl in |- *; auto ] ]
@@ -3172,7 +3172,7 @@ Theorem do_reduce_lhyps :
  interp_list_goal envp env (reduce_lhyps l) -> interp_list_goal envp env l.
 Proof.
  intros envp env l H; apply list_goal_to_hyps; intro H1;
- apply list_hyps_to_goal with (1 := H); apply reduce_lhyps_valid; 
+ apply list_hyps_to_goal with (1 := H); apply reduce_lhyps_valid;
  assumption.
 Qed.
 
@@ -3193,12 +3193,12 @@ Proof.
  | simpl in |- *; tauto ].
 Qed.
 
-Definition omega_tactic (t1 : e_step) (t2 : list h_step) 
+Definition omega_tactic (t1 : e_step) (t2 : list h_step)
   (c : proposition) (l : hyps) :=
   reduce_lhyps (decompose_solve t1 (normalize_hyps t2 (concl_to_hyp c :: l))).
 
 Theorem do_omega :
- forall (t1 : e_step) (t2 : list h_step) (envp : list Prop) 
+ forall (t1 : e_step) (t2 : list h_step) (envp : list Prop)
    (env : list int) (c : proposition) (l : hyps),
  interp_list_goal envp env (omega_tactic t1 t2 c l) ->
  interp_goal_concl c envp env l.
@@ -3210,7 +3210,7 @@ Qed.
 
 End IntOmega.
 
-(* For now, the above modular construction is instanciated on Z, 
+(* For now, the above modular construction is instanciated on Z,
    in order to retrieve the initial ROmega. *)
 
 Module ZOmega := IntOmega(Z_as_Int).
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 1caa5db1c..2978d699e 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -9,7 +9,7 @@
 let module_refl_name = "ReflOmegaCore"
 let module_refl_path = ["Coq"; "romega"; module_refl_name]
 
-type result = 
+type result =
    Kvar of string
  | Kapp of string * Term.constr list
  | Kimp of Term.constr * Term.constr
@@ -38,10 +38,10 @@ let destructurate t =
 
 exception Destruct
 
-let dest_const_apply t = 
-  let f,args = Term.decompose_app t in 
-  let ref = 
-  match Term.kind_of_term f with 
+let dest_const_apply t =
+  let f,args = Term.decompose_app t in
+  let ref =
+  match Term.kind_of_term f with
     | Term.Const sp      -> Libnames.ConstRef sp
     | Term.Construct csp -> Libnames.ConstructRef csp
     | Term.Ind isp       -> Libnames.IndRef isp
@@ -165,15 +165,15 @@ let coq_do_omega = lazy (constant  "do_omega")
 
 (* \subsection{Construction d'expressions} *)
 
-let do_left t = 
+let do_left t =
   if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop
   else Term.mkApp (Lazy.force coq_c_do_left, [|t |] )
 
-let do_right t = 
+let do_right t =
   if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop
   else Term.mkApp (Lazy.force coq_c_do_right, [|t |])
 
-let do_both t1 t2 = 
+let do_both t1 t2 =
   if t1 = Lazy.force coq_c_nop then do_right t2
   else if t2 = Lazy.force coq_c_nop then do_left t1
   else Term.mkApp (Lazy.force coq_c_do_both , [|t1; t2 |])
@@ -182,7 +182,7 @@ let do_seq t1 t2 =
   if t1 = Lazy.force coq_c_nop then t2
   else if t2 = Lazy.force coq_c_nop then t1
   else Term.mkApp (Lazy.force coq_c_do_seq, [|t1; t2 |])
-  
+
 let rec do_list = function
   | [] -> Lazy.force coq_c_nop
   | [x] -> x
@@ -206,7 +206,7 @@ let mk_list typ l =
   let rec loop = function
     | [] ->
 	Term.mkApp (Lazy.force coq_nil, [|typ|])
-    | (step :: l) -> 
+    | (step :: l) ->
 	Term.mkApp (Lazy.force coq_cons, [|typ; step; loop l |]) in
   loop l
 
@@ -215,16 +215,16 @@ let mk_plist l = mk_list Term.mkProp l
 let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l
 
 
-type parse_term = 
-  | Tplus of Term.constr * Term.constr 
+type parse_term =
+  | Tplus of Term.constr * Term.constr
   | Tmult of Term.constr * Term.constr
   | Tminus of Term.constr * Term.constr
   | Topp of Term.constr
   | Tsucc of Term.constr
   | Tnum of Bigint.bigint
-  | Tother 
+  | Tother
 
-type parse_rel = 
+type parse_rel =
   | Req of Term.constr * Term.constr
   | Rne of Term.constr * Term.constr
   | Rlt of Term.constr * Term.constr
@@ -240,12 +240,12 @@ type parse_rel =
   | Riff of Term.constr * Term.constr
   | Rother
 
-let parse_logic_rel c = 
+let parse_logic_rel c =
  try match destructurate c with
    | Kapp("True",[]) -> Rtrue
    | Kapp("False",[]) -> Rfalse
    | Kapp("not",[t]) -> Rnot t
-   | Kapp("or",[t1;t2]) -> Ror (t1,t2) 
+   | Kapp("or",[t1;t2]) -> Ror (t1,t2)
    | Kapp("and",[t1;t2]) -> Rand (t1,t2)
    | Kimp(t1,t2) -> Rimp (t1,t2)
    | Kapp("iff",[t1;t2]) -> Riff (t1,t2)
@@ -255,7 +255,7 @@ let parse_logic_rel c =
 
 module type Int = sig
   val typ : Term.constr Lazy.t
-  val plus : Term.constr Lazy.t 
+  val plus : Term.constr Lazy.t
   val mult : Term.constr Lazy.t
   val opp : Term.constr Lazy.t
   val minus : Term.constr Lazy.t
@@ -264,10 +264,10 @@ module type Int = sig
   val parse_term : Term.constr -> parse_term
   val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
   (* check whether t is built only with numbers and + * - *)
-  val is_scalar : Term.constr -> bool 
+  val is_scalar : Term.constr -> bool
 end
 
-module Z : Int = struct 
+module Z : Int = struct
 
 let typ = lazy (constant "Z")
 let plus = lazy (constant "Zplus")
@@ -297,16 +297,16 @@ let recognize t =
       | "Z0",[] -> Bigint.zero
       | _ -> failwith "not a number";;
 
-let rec mk_positive n = 
-  if n=Bigint.one then Lazy.force coq_xH 
+let rec mk_positive n =
+  if n=Bigint.one then Lazy.force coq_xH
   else
     let (q,r) = Bigint.euclid n Bigint.two in
     Term.mkApp
       ((if r = Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI),
-       [| mk_positive q |]) 
+       [| mk_positive q |])
 
 let mk_Z n =
-  if n = Bigint.zero then Lazy.force coq_Z0 
+  if n = Bigint.zero then Lazy.force coq_Z0
   else if Bigint.is_strictly_pos n then
     Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
   else
@@ -314,7 +314,7 @@ let mk_Z n =
 
 let mk = mk_Z
 
-let parse_term t = 
+let parse_term t =
   try match destructurate t with
     | Kapp("Zplus",[t1;t2]) -> Tplus (t1,t2)
     | Kapp("Zminus",[t1;t2]) -> Tminus (t1,t2)
@@ -322,21 +322,21 @@ let parse_term t =
     | Kapp("Zopp",[t]) -> Topp t
     | Kapp("Zsucc",[t]) -> Tsucc t
     | Kapp("Zpred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
-    | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> 
+    | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
 	(try Tnum (recognize t) with _ -> Tother)
     | _ -> Tother
   with e when Logic.catchable_exception e -> Tother
-    
-let parse_rel gl t = 
-  try match destructurate t with 
-    | Kapp("eq",[typ;t1;t2]) 
+
+let parse_rel gl t =
+  try match destructurate t with
+    | Kapp("eq",[typ;t1;t2])
       when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2)
     | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
     | Kapp("Zle",[t1;t2]) -> Rle (t1,t2)
     | Kapp("Zlt",[t1;t2]) -> Rlt (t1,t2)
     | Kapp("Zge",[t1;t2]) -> Rge (t1,t2)
     | Kapp("Zgt",[t1;t2]) -> Rgt (t1,t2)
-    | _ -> parse_logic_rel t 
+    | _ -> parse_logic_rel t
   with e when Logic.catchable_exception e -> Rother
 
 let is_scalar t =
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 0f00e9184..b8db71e40 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -168,7 +168,7 @@ module type Int =
     val parse_term : Term.constr -> parse_term
     (* parsing a relation expression, including = < <= >= > *)
     val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
-    (* Is a particular term only made of numbers and + * - ? *) 
+    (* Is a particular term only made of numbers and + * - ? *)
     val is_scalar : Term.constr -> bool
   end
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 39b6c2106..2db86e005 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -11,23 +11,23 @@
 open Refl_omega
 open Refiner
 
-let romega_tactic l = 
-  let tacs = List.map 
-    (function  
+let romega_tactic l =
+  let tacs = List.map
+    (function
        | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
        | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
        | "N" -> Tacinterp.interp <:tactic<zify_N>>
        | "Z" -> Tacinterp.interp <:tactic<zify_op>>
        | s -> Util.error ("No ROmega knowledge base for type "^s))
     (Util.list_uniquize (List.sort compare l))
-  in 
+  in
   tclTHEN
     (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
-    (tclTHEN 
-       (* because of the contradiction process in (r)omega, 
+    (tclTHEN
+       (* because of the contradiction process in (r)omega,
           we'd better leave as little as possible in the conclusion,
           for an easier decidability argument. *)
-       Tactics.intros 
+       Tactics.intros
        total_reflexive_omega_tactic)
 
 
@@ -36,7 +36,7 @@ TACTIC EXTEND romega
 END
 
 TACTIC EXTEND romega'
-| [ "romega" "with" ne_ident_list(l) ] -> 
+| [ "romega" "with" ne_ident_list(l) ] ->
     [ romega_tactic (List.map Names.string_of_id l) ]
 | [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ]
 END
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index fc4f7a8f0..570bb1877 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -28,7 +28,7 @@ let mkApp = Term.mkApp
 (* \section{Types}
   \subsection{How to walk in a term}
   To represent how to get to a proposition. Only choice points are
-  kept (branch to choose in a disjunction  and identifier of the disjunctive 
+  kept (branch to choose in a disjunction  and identifier of the disjunctive
   connector) *)
 type direction = Left of int | Right of int
 
@@ -58,11 +58,11 @@ type oformula =
 (* Operators for comparison recognized by Omega *)
 type comparaison = Eq | Leq | Geq | Gt | Lt | Neq
 
-(* Type des prédicats réifiés (fragment de calcul propositionnel. Les 
+(* Type des prédicats réifiés (fragment de calcul propositionnel. Les
  * quantifications sont externes au langage) *)
-type oproposition = 
+type oproposition =
     Pequa of Term.constr * oequation
-  | Ptrue 
+  | Ptrue
   | Pfalse
   | Pnot of oproposition
   | Por of int * oproposition * oproposition
@@ -77,16 +77,16 @@ and oequation = {
     e_right: oformula;			(* formule brute droite *)
     e_trace: Term.constr;		(* tactique de normalisation *)
     e_origin: occurence;		(* l'hypothèse dont vient le terme *)
-    e_negated: bool;			(* vrai si apparait en position nié 
+    e_negated: bool;			(* vrai si apparait en position nié
 					   après normalisation *)
-    e_depends: direction  list;		(* liste des points de disjonction dont 
-					   dépend l'accès à l'équation avec la 
+    e_depends: direction  list;		(* liste des points de disjonction dont
+					   dépend l'accès à l'équation avec la
 					   direction (branche) pour y accéder *)
     e_omega: afine		(* la fonction normalisée *)
-  } 
+  }
 
-(* \subsection{Proof context} 
-  This environment codes 
+(* \subsection{Proof context}
+  This environment codes
   \begin{itemize}
   \item the terms and propositions that are given as
   parameters of the reified proof (and are represented as variables in the
@@ -101,7 +101,7 @@ type environment = {
   mutable props : Term.constr list;
   (* Les variables introduites par omega *)
   mutable om_vars : (oformula * int) list;
-  (* Traduction des indices utilisés ici en les indices finaux utilisés par 
+  (* Traduction des indices utilisés ici en les indices finaux utilisés par
    * la tactique Omega après dénombrement des variables utiles *)
   real_indices : (int,int) Hashtbl.t;
   mutable cnt_connectors : int;
@@ -119,7 +119,7 @@ type solution = {
   s_trace : action list }
 
 (* Arbre de solution résolvant complètement un ensemble de systèmes *)
-type solution_tree = 
+type solution_tree =
     Leaf of solution
     (* un noeud interne représente un point de branchement correspondant à
        l'élimination d'un connecteur générant plusieurs buts
@@ -130,37 +130,37 @@ type solution_tree =
 (* Représentation de l'environnement extrait du but initial sous forme de
    chemins pour extraire des equations ou d'hypothèses *)
 
-type context_content = 
+type context_content =
     CCHyp of occurence
   | CCEqua of int
 
 (* \section{Specific utility functions to handle base types} *)
-(* Nom arbitraire de l'hypothèse codant la négation du but final *)  
+(* Nom arbitraire de l'hypothèse codant la négation du but final *)
 let id_concl = Names.id_of_string "__goal__"
 
 (* Initialisation de l'environnement de réification de la tactique *)
 let new_environment () = {
-  terms = []; props = []; om_vars = []; cnt_connectors = 0; 
+  terms = []; props = []; om_vars = []; cnt_connectors = 0;
   real_indices = Hashtbl.create 7;
   equations = Hashtbl.create 7;
   constructors = Hashtbl.create 7;
 }
 
 (* Génération d'un nom d'équation *)
-let new_connector_id env =  
+let new_connector_id env =
    env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors
 
 (* Calcul de la branche complémentaire *)
 let barre = function Left x -> Right x | Right x -> Left x
 
 (* Identifiant associé à une branche *)
-let indice = function Left x | Right x -> x 
+let indice = function Left x | Right x -> x
 
 (* Affichage de l'environnement de réification (termes et propositions) *)
-let print_env_reification env = 
+let print_env_reification env =
   let rec loop c i = function
       [] -> Printf.printf "  ===============================\n\n"
-    | t :: l -> 
+    | t :: l ->
 	Printf.printf "  (%c%02d) := " c i;
 	Pp.ppnl (Printer.pr_lconstr t);
 	Pp.flush_all ();
@@ -173,16 +173,16 @@ let print_env_reification env =
 (* \subsection{Gestion des environnements de variable pour Omega} *)
 (* generation d'identifiant d'equation pour Omega *)
 
-let new_omega_eq, rst_omega_eq = 
-  let cpt = ref 0 in 
-  (function () -> incr cpt; !cpt), 
+let new_omega_eq, rst_omega_eq =
+  let cpt = ref 0 in
+  (function () -> incr cpt; !cpt),
   (function () -> cpt:=0)
 
 (* generation d'identifiant de variable pour Omega *)
 
-let new_omega_var, rst_omega_var = 
-  let cpt = ref 0 in 
-  (function () -> incr cpt; !cpt), 
+let new_omega_var, rst_omega_var =
+  let cpt = ref 0 in
+  (function () -> incr cpt; !cpt),
   (function () -> cpt:=0)
 
 (* Affichage des variables d'un système *)
@@ -195,8 +195,8 @@ let display_omega_var i = Printf.sprintf "OV%d" i
 
 let intern_omega env t =
   begin try List.assoc t env.om_vars
-  with Not_found -> 
-    let v = new_omega_var () in 
+  with Not_found ->
+    let v = new_omega_var () in
     env.om_vars <- (t,v) :: env.om_vars; v
   end
 
@@ -207,14 +207,14 @@ let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars
 
 (* Récupère le terme associé à une variable *)
 let unintern_omega env id =
-  let rec loop = function 
-	[] -> failwith "unintern" 
+  let rec loop = function
+	[] -> failwith "unintern"
       | ((t,j)::l) -> if id = j then t else loop l in
   loop env.om_vars
 
-(* \subsection{Gestion des environnements de variable pour la réflexion} 
+(* \subsection{Gestion des environnements de variable pour la réflexion}
    Gestion des environnements de traduction entre termes des constructions
-   non réifiés et variables des termes reifies. Attention il s'agit de 
+   non réifiés et variables des termes reifies. Attention il s'agit de
    l'environnement initial contenant tout. Il faudra le réduire après
    calcul des variables utiles. *)
 
@@ -224,7 +224,7 @@ let add_reified_atom t env =
     let i = List.length env.terms in
     env.terms <- env.terms @ [t]; i
 
-let get_reified_atom env = 
+let get_reified_atom env =
   try List.nth env.terms with _ -> failwith "get_reified_atom"
 
 (* \subsection{Gestion de l'environnement de proposition pour Omega} *)
@@ -245,33 +245,33 @@ let add_equation env e =
   with Not_found -> Hashtbl.add env.equations id e
 
 (* accès a une equation *)
-let get_equation env id = 
+let get_equation env id =
   try Hashtbl.find env.equations id
   with e -> Printf.printf "Omega Equation %d non trouvée\n" id; raise e
 
 (* Affichage des termes réifiés *)
-let rec oprint ch = function 
+let rec oprint ch = function
   | Oint n -> Printf.fprintf ch "%s" (Bigint.to_string n)
-  | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2  
-  | Omult (t1,t2) -> Printf.fprintf ch "(%a * %a)" oprint t1 oprint t2 
-  | Ominus(t1,t2) -> Printf.fprintf ch "(%a - %a)" oprint t1 oprint t2 
+  | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2
+  | Omult (t1,t2) -> Printf.fprintf ch "(%a * %a)" oprint t1 oprint t2
+  | Ominus(t1,t2) -> Printf.fprintf ch "(%a - %a)" oprint t1 oprint t2
   | Oopp t1 ->Printf.fprintf ch "~ %a" oprint t1
   | Oatom n -> Printf.fprintf ch "V%02d" n
   | Oufo x ->  Printf.fprintf ch "?"
 
 let rec pprint ch = function
     Pequa (_,{ e_comp=comp; e_left=t1; e_right=t2 })  ->
-      let connector = 
-	match comp with 
+      let connector =
+	match comp with
 	  Eq -> "=" | Leq -> "<=" | Geq -> ">="
 	| Gt -> ">" | Lt -> "<" | Neq -> "!=" in
-      Printf.fprintf ch "%a %s %a" oprint t1 connector oprint t2  
+      Printf.fprintf ch "%a %s %a" oprint t1 connector oprint t2
   | Ptrue -> Printf.fprintf ch "TT"
   | Pfalse -> Printf.fprintf ch "FF"
   | Pnot t -> Printf.fprintf ch "not(%a)" pprint t
-  | Por (_,t1,t2) -> Printf.fprintf ch "(%a or %a)" pprint t1 pprint t2  
-  | Pand(_,t1,t2) -> Printf.fprintf ch "(%a and %a)" pprint t1 pprint t2  
-  | Pimp(_,t1,t2) -> Printf.fprintf ch "(%a => %a)" pprint t1 pprint t2  
+  | Por (_,t1,t2) -> Printf.fprintf ch "(%a or %a)" pprint t1 pprint t2
+  | Pand(_,t1,t2) -> Printf.fprintf ch "(%a and %a)" pprint t1 pprint t2
+  | Pimp(_,t1,t2) -> Printf.fprintf ch "(%a => %a)" pprint t1 pprint t2
   | Pprop c -> Printf.fprintf ch "Prop"
 
 let rec weight env = function
@@ -287,21 +287,21 @@ let rec weight env = function
 
 (* \subsection{Oformula vers Omega} *)
 
-let omega_of_oformula env kind = 
+let omega_of_oformula env kind =
   let rec loop accu = function
-    | Oplus(Omult(v,Oint n),r) -> 
+    | Oplus(Omult(v,Oint n),r) ->
 	loop ({v=intern_omega env v; c=n} :: accu) r
     | Oint n ->
 	let id = new_omega_eq () in
 	(*i tag_equation name id; i*)
-	{kind = kind; body = List.rev accu; 
+	{kind = kind; body = List.rev accu;
 	 constant = n; id = id}
     | t -> print_string "CO"; oprint stdout t; failwith "compile_equation" in
   loop []
 
 (* \subsection{Omega vers Oformula} *)
 
-let rec oformula_of_omega env af = 
+let rec oformula_of_omega env af =
   let rec loop = function
     | ({v=v; c=n}::r) ->
 	Oplus(Omult(unintern_omega env v,Oint n),loop r)
@@ -330,8 +330,8 @@ let rec coq_of_formula env t =
 
 let reified_of_atom env i =
   try Hashtbl.find env.real_indices i
-  with Not_found -> 
-    Printf.printf "Atome %d non trouvé\n" i; 
+  with Not_found ->
+    Printf.printf "Atome %d non trouvé\n" i;
     Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices;
     raise Not_found
 
@@ -352,55 +352,55 @@ let reified_of_formula env f =
   begin try reified_of_formula env f with e -> oprint stderr f; raise e end
 
 let rec reified_of_proposition env = function
-    Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) -> 
+    Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) ->
       app coq_p_eq [| reified_of_formula env t1; reified_of_formula env t2 |]
-  | Pequa (_,{ e_comp=Leq; e_left=t1; e_right=t2 }) -> 
+  | Pequa (_,{ e_comp=Leq; e_left=t1; e_right=t2 }) ->
       app coq_p_leq [| reified_of_formula env t1; reified_of_formula env t2 |]
-  | Pequa(_,{ e_comp=Geq; e_left=t1; e_right=t2 }) -> 
+  | Pequa(_,{ e_comp=Geq; e_left=t1; e_right=t2 }) ->
       app coq_p_geq [| reified_of_formula env t1; reified_of_formula env t2 |]
-  | Pequa(_,{ e_comp=Gt; e_left=t1; e_right=t2 }) -> 
+  | Pequa(_,{ e_comp=Gt; e_left=t1; e_right=t2 }) ->
       app coq_p_gt [| reified_of_formula env t1; reified_of_formula env t2 |]
-  | Pequa(_,{ e_comp=Lt; e_left=t1; e_right=t2 }) ->  
+  | Pequa(_,{ e_comp=Lt; e_left=t1; e_right=t2 }) ->
       app coq_p_lt [| reified_of_formula env t1; reified_of_formula env t2 |]
-  | Pequa(_,{ e_comp=Neq; e_left=t1; e_right=t2 }) -> 
+  | Pequa(_,{ e_comp=Neq; e_left=t1; e_right=t2 }) ->
       app coq_p_neq [| reified_of_formula env t1; reified_of_formula env t2 |]
   | Ptrue -> Lazy.force coq_p_true
   | Pfalse -> Lazy.force coq_p_false
-  | Pnot t -> 
+  | Pnot t ->
       app coq_p_not [| reified_of_proposition env t |]
-  | Por (_,t1,t2) -> 
+  | Por (_,t1,t2) ->
       app coq_p_or
 	[| reified_of_proposition env t1; reified_of_proposition env t2 |]
-  | Pand(_,t1,t2) -> 
+  | Pand(_,t1,t2) ->
       app coq_p_and
 	[| reified_of_proposition env t1; reified_of_proposition env t2 |]
-  | Pimp(_,t1,t2) -> 
+  | Pimp(_,t1,t2) ->
       app coq_p_imp
 	[| reified_of_proposition env t1; reified_of_proposition env t2 |]
   | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |]
 
 let reified_of_proposition env f =
-  begin try reified_of_proposition env f 
+  begin try reified_of_proposition env f
   with e -> pprint stderr f; raise e end
 
 (* \subsection{Omega vers COQ réifié} *)
 
-let reified_of_omega env body constant = 
-  let coeff_constant = 
+let reified_of_omega env body constant =
+  let coeff_constant =
     app coq_t_int [| Z.mk constant |] in
   let mk_coeff {c=c; v=v} t =
-    let coef = 
-      app coq_t_mult 
-	[| reified_of_formula env (unintern_omega env v); 
+    let coef =
+      app coq_t_mult
+	[| reified_of_formula env (unintern_omega env v);
 	   app coq_t_int [| Z.mk c |] |] in
     app coq_t_plus [|coef; t |] in
   List.fold_right mk_coeff body coeff_constant
 
-let reified_of_omega env body c  = 
-  begin try 
-    reified_of_omega env body c 
-  with e -> 
-    display_eq display_omega_var (body,c); raise e 
+let reified_of_omega env body c  =
+  begin try
+    reified_of_omega env body c
+  with e ->
+    display_eq display_omega_var (body,c); raise e
   end
 
 (* \section{Opérations sur les équations}
@@ -423,13 +423,13 @@ let rec vars_of_formula = function
   | Oufo _ -> []
 
 let rec vars_of_equations = function
-  | [] -> [] 
-  | e::l -> 
+  | [] -> []
+  | e::l ->
       (vars_of_formula e.e_left) @@
       (vars_of_formula e.e_right) @@
       (vars_of_equations l)
 
-let rec vars_of_prop = function 
+let rec vars_of_prop = function
   | Pequa(_,e) -> vars_of_equations [e]
   | Pnot p -> vars_of_prop p
   | Por(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
@@ -440,16 +440,16 @@ let rec vars_of_prop = function
 (* \subsection{Multiplication par un scalaire} *)
 
 let rec scalar n = function
-   Oplus(t1,t2) -> 
-     let tac1,t1' = scalar  n t1 and 
+   Oplus(t1,t2) ->
+     let tac1,t1' = scalar  n t1 and
          tac2,t2' = scalar  n t2 in
-     do_list [Lazy.force coq_c_mult_plus_distr; do_both tac1 tac2], 
+     do_list [Lazy.force coq_c_mult_plus_distr; do_both tac1 tac2],
      Oplus(t1',t2')
  | Oopp t ->
      do_list [Lazy.force coq_c_mult_opp_left], Omult(t,Oint(Bigint.neg n))
- | Omult(t1,Oint x) -> 
+ | Omult(t1,Oint x) ->
      do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x))
- | Omult(t1,t2) -> 
+ | Omult(t1,t2) ->
      Util.error "Omega: Can't solve a goal with non-linear products"
  | (Oatom _ as t) -> do_list [], Omult(t,Oint n)
  | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i)
@@ -459,16 +459,16 @@ let rec scalar n = function
 (* \subsection{Propagation de l'inversion} *)
 
 let rec negate = function
-   Oplus(t1,t2) -> 
-     let tac1,t1' = negate t1 and 
+   Oplus(t1,t2) ->
+     let tac1,t1' = negate t1 and
          tac2,t2' = negate t2 in
      do_list [Lazy.force coq_c_opp_plus ; (do_both tac1 tac2)],
      Oplus(t1',t2')
  | Oopp t ->
      do_list [Lazy.force coq_c_opp_opp], t
- | Omult(t1,Oint x) -> 
+ | Omult(t1,Oint x) ->
      do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x))
- | Omult(t1,t2) -> 
+ | Omult(t1,t2) ->
      Util.error "Omega: Can't solve a goal with non-linear products"
  | (Oatom _ as t) ->
      do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone))
@@ -493,29 +493,29 @@ let rec shuffle_path k1 e1 k2 e2 =
 	  Lazy.force coq_f_left :: loop(l1,l2'))
 	else (
 	  Lazy.force coq_f_right :: loop(l1',l2))
-    | ({c=c1;v=v1}::l1), [] -> 
+    | ({c=c1;v=v1}::l1), [] ->
 	  Lazy.force coq_f_left :: loop(l1,[])
-    | [],({c=c2;v=v2}::l2) -> 
+    | [],({c=c2;v=v2}::l2) ->
 	  Lazy.force coq_f_right :: loop([],l2)
     | [],[] -> flush stdout; [] in
   mk_shuffle_list (loop (e1,e2))
 
 (* \subsubsection{Version sans coefficients} *)
-let rec shuffle env (t1,t2) = 
+let rec shuffle env (t1,t2) =
   match t1,t2 with
     Oplus(l1,r1), Oplus(l2,r2) ->
-      if weight env l1 > weight env l2 then 
+      if weight env l1 > weight env l2 then
 	let l_action,t' = shuffle env (r1,t2) in
 	do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action], Oplus(l1,t')
-      else 
+      else
 	let l_action,t' = shuffle env (t1,r2) in
 	do_list [Lazy.force coq_c_plus_permute;do_right l_action], Oplus(l2,t')
-  | Oplus(l1,r1), t2 -> 
+  | Oplus(l1,r1), t2 ->
       if weight env l1 > weight env t2 then
         let (l_action,t') = shuffle env (r1,t2) in
 	do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action],Oplus(l1, t')
       else do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1)
-  | t1,Oplus(l2,r2) -> 
+  | t1,Oplus(l2,r2) ->
       if weight env l2 > weight env t1 then
         let (l_action,t') = shuffle env (t1,r2) in
 	do_list [Lazy.force coq_c_plus_permute;do_right l_action], Oplus(l2,t')
@@ -531,16 +531,16 @@ let rec shuffle env (t1,t2) =
 
 let shrink_pair f1 f2 =
   begin match f1,f2 with
-     Oatom v,Oatom _ -> 
+     Oatom v,Oatom _ ->
        Lazy.force coq_c_red1, Omult(Oatom v,Oint two)
-   | Oatom v, Omult(_,c2) -> 
+   | Oatom v, Omult(_,c2) ->
        Lazy.force coq_c_red2, Omult(Oatom v,Oplus(c2,Oint one))
-   | Omult (v1,c1),Oatom v -> 
+   | Omult (v1,c1),Oatom v ->
        Lazy.force coq_c_red3, Omult(Oatom v,Oplus(c1,Oint one))
    | Omult (Oatom v,c1),Omult (v2,c2) ->
        Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2))
-   | t1,t2 -> 
-       oprint stdout t1; print_newline (); oprint stdout t2; print_newline (); 
+   | t1,t2 ->
+       oprint stdout t1; print_newline (); oprint stdout t2; print_newline ();
        flush Pervasives.stdout; Util.error "shrink.1"
   end
 
@@ -554,7 +554,7 @@ let reduce_factor = function
   | Omult(Oatom v,c) ->
       let rec compute = function
           Oint n -> n
-	| Oplus(t1,t2) -> compute t1 + compute t2 
+	| Oplus(t1,t2) -> compute t1 + compute t2
 	| _ -> Util.error "condense.1" in
 	[Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c))
   | t -> Util.error "reduce_factor.1"
@@ -570,24 +570,24 @@ let rec condense env = function
 	assoc_tac :: do_left (do_list [shrink_tac]) :: tac_list, t'
       end else begin
 	let tac,f = reduce_factor f1 in
-	let tac',t' = condense env t in 
-	[do_both (do_list tac) (do_list tac')], Oplus(f,t') 
+	let tac',t' = condense env t in
+	[do_both (do_list tac) (do_list tac')], Oplus(f,t')
       end
-  | Oplus(f1,Oint n) -> 
-      let tac,f1' = reduce_factor f1 in 
+  | Oplus(f1,Oint n) ->
+      let tac,f1' = reduce_factor f1 in
       [do_left (do_list tac)],Oplus(f1',Oint n)
-  | Oplus(f1,f2) -> 
+  | Oplus(f1,f2) ->
       if weight env f1 = weight env f2 then begin
 	let tac_shrink,t = shrink_pair f1 f2 in
 	let tac,t' = condense env t in
 	tac_shrink :: tac,t'
       end else begin
 	let tac,f = reduce_factor f1 in
-	let tac',t' = condense env f2 in 
-	[do_both (do_list tac) (do_list tac')],Oplus(f,t') 
+	let tac',t' = condense env f2 in
+	[do_both (do_list tac) (do_list tac')],Oplus(f,t')
       end
   | (Oint _ as t)-> [],t
-  | t -> 
+  | t ->
       let tac,t' = reduce_factor t in
       let final = Oplus(t',Oint zero) in
       tac @ [Lazy.force coq_c_red6], final
@@ -598,8 +598,8 @@ let rec clear_zero = function
    Oplus(Omult(Oatom v,Oint n),r) when n=zero ->
      let tac',t = clear_zero r in
      Lazy.force coq_c_red5 :: tac',t
-  | Oplus(f,r) -> 
-      let tac,t = clear_zero r in 
+  | Oplus(f,r) ->
+      let tac,t = clear_zero r in
       (if tac = [] then [] else [do_right (do_list tac)]),Oplus(f,t)
   | t -> [],t;;
 
@@ -641,14 +641,14 @@ let normalize_linear_term env t =
 (* Cette fonction reproduit très exactement le comportement de [p_invert] *)
 let negate_oper = function
     Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq
- 
-let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) = 
+
+let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) =
   let mk_step t1 t2 f kind =
     let t = f t1 t2 in
     let trace, oterm = normalize_linear_term env t in
-    let equa = omega_of_oformula env kind oterm in 
-    { e_comp = oper; e_left = t1; e_right = t2; 
-      e_negated = negated; e_depends = depends; 
+    let equa = omega_of_oformula env kind oterm in
+    { e_comp = oper; e_left = t1; e_right = t2;
+      e_negated = negated; e_depends = depends;
       e_origin = { o_hyp = origin; o_path = List.rev path };
       e_trace = trace; e_omega = equa } in
   try match (if negated then (negate_oper oper) else oper) with
@@ -660,36 +660,36 @@ let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) =
         mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o2,Oint negone),Oopp o1))
 	  INEQ
     | Gt ->
-        mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o1,Oint negone),Oopp o2)) 
+        mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o1,Oint negone),Oopp o2))
 	  INEQ
   with e when Logic.catchable_exception e -> raise e
 
 (* \section{Compilation des hypothèses} *)
 
 let rec oformula_of_constr env t =
-  match Z.parse_term t with 
+  match Z.parse_term t with
     | Tplus (t1,t2) -> binop env (fun x y -> Oplus(x,y)) t1 t2
     | Tminus (t1,t2) -> binop env (fun x y -> Ominus(x,y)) t1 t2
-    | Tmult (t1,t2) when Z.is_scalar t1 || Z.is_scalar t2 -> 
+    | Tmult (t1,t2) when Z.is_scalar t1 || Z.is_scalar t2 ->
 	binop env (fun x y -> Omult(x,y)) t1 t2
     | Topp t -> Oopp(oformula_of_constr env t)
     | Tsucc t -> Oplus(oformula_of_constr env t, Oint one)
     | Tnum n -> Oint n
     | _ -> Oatom (add_reified_atom t env)
 
-and binop env c t1 t2 = 
+and binop env c t1 t2 =
   let t1' = oformula_of_constr env t1 in
   let t2' = oformula_of_constr env t2 in
   c t1' t2'
 
-and binprop env (neg2,depends,origin,path) 
+and binprop env (neg2,depends,origin,path)
              add_to_depends neg1 gl c t1 t2 =
   let i = new_connector_id env in
   let depends1 = if add_to_depends then Left i::depends else depends in
   let depends2 = if add_to_depends then Right i::depends else depends in
   if add_to_depends then
     Hashtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path};
-  let t1' = 
+  let t1' =
     oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in
   let t2' =
     oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in
@@ -704,31 +704,31 @@ and mk_equation env ctxt c connector t1 t2 =
   add_equation env omega;
   Pequa (c,omega)
 
-and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = 
-  match Z.parse_rel gl c with 
+and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
+  match Z.parse_rel gl c with
     | Req (t1,t2) -> mk_equation env ctxt c Eq t1 t2
     | Rne (t1,t2) -> mk_equation env ctxt c Neq t1 t2
     | Rle (t1,t2) -> mk_equation env ctxt c Leq t1 t2
     | Rlt (t1,t2) -> mk_equation env ctxt c Lt t1 t2
     | Rge (t1,t2) -> mk_equation env ctxt c Geq t1 t2
     | Rgt (t1,t2) -> mk_equation env ctxt c Gt t1 t2
-    | Rtrue -> Ptrue 
+    | Rtrue -> Ptrue
     | Rfalse -> Pfalse
-    | Rnot t -> 
-	let t' = 
-	  oproposition_of_constr 
-	    env (not negated, depends, origin,(O_mono::path)) gl t in 
+    | Rnot t ->
+	let t' =
+	  oproposition_of_constr
+	    env (not negated, depends, origin,(O_mono::path)) gl t in
 	Pnot t'
-    | Ror (t1,t2) -> 
+    | Ror (t1,t2) ->
 	binprop env ctxt (not negated) negated gl (fun i x y -> Por(i,x,y)) t1 t2
-    | Rand (t1,t2) -> 
+    | Rand (t1,t2) ->
 	binprop env ctxt negated negated gl
 	  (fun i x y -> Pand(i,x,y)) t1 t2
     | Rimp (t1,t2) ->
-	binprop env ctxt (not negated) (not negated) gl 
+	binprop env ctxt (not negated) (not negated) gl
 	  (fun i x y -> Pimp(i,x,y)) t1 t2
     | Riff (t1,t2) ->
-	binprop env ctxt negated negated gl 
+	binprop env ctxt negated negated gl
 	  (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1)
     | _ -> Pprop c
 
@@ -751,30 +751,30 @@ let reify_gl env gl =
 	  Printf.printf "\n"
 	end;
 	(i,t') :: loop lhyps
-    | [] -> 
-	if !debug then print_env_reification env; 
+    | [] ->
+	if !debug then print_env_reification env;
 	[] in
   let t_lhyps = loop (Tacmach.pf_hyps_types gl) in
-  (id_concl,t_concl) :: t_lhyps 
+  (id_concl,t_concl) :: t_lhyps
 
 let rec destructurate_pos_hyp orig list_equations list_depends = function
   | Pequa (_,e) -> [e :: list_equations]
   | Ptrue | Pfalse | Pprop _ -> [list_equations]
   | Pnot t -> destructurate_neg_hyp orig list_equations list_depends t
-  | Por (i,t1,t2) -> 
-      let s1 = 
+  | Por (i,t1,t2) ->
+      let s1 =
 	destructurate_pos_hyp orig list_equations (i::list_depends) t1 in
-      let s2 = 
+      let s2 =
 	destructurate_pos_hyp orig list_equations (i::list_depends) t2 in
       s1 @ s2
-  | Pand(i,t1,t2) -> 
+  | Pand(i,t1,t2) ->
       let list_s1 =
 	destructurate_pos_hyp orig list_equations (list_depends) t1 in
-      let rec loop = function 
+      let rec loop = function
 	  le1 :: ll -> destructurate_pos_hyp orig le1 list_depends t2 @ loop ll
 	| [] -> [] in
       loop list_s1
-  | Pimp(i,t1,t2) -> 
+  | Pimp(i,t1,t2) ->
       let s1 =
 	destructurate_neg_hyp orig list_equations (i::list_depends) t1 in
       let s2 =
@@ -785,30 +785,30 @@ and destructurate_neg_hyp orig list_equations list_depends = function
   | Pequa (_,e) -> [e :: list_equations]
   | Ptrue | Pfalse | Pprop _ -> [list_equations]
   | Pnot t -> destructurate_pos_hyp orig list_equations list_depends t
-  | Pand (i,t1,t2) -> 
+  | Pand (i,t1,t2) ->
       let s1 =
 	destructurate_neg_hyp orig list_equations (i::list_depends) t1 in
       let s2 =
 	destructurate_neg_hyp orig list_equations (i::list_depends) t2 in
       s1 @ s2
-  | Por(_,t1,t2) -> 
+  | Por(_,t1,t2) ->
       let list_s1 =
 	destructurate_neg_hyp orig list_equations list_depends t1 in
-      let rec loop = function 
+      let rec loop = function
 	  le1 :: ll -> destructurate_neg_hyp orig le1 list_depends t2 @ loop ll
 	| [] -> [] in
       loop list_s1
-  | Pimp(_,t1,t2) -> 
+  | Pimp(_,t1,t2) ->
       let list_s1 =
 	destructurate_pos_hyp orig list_equations list_depends t1 in
-      let rec loop = function 
+      let rec loop = function
 	  le1 :: ll -> destructurate_neg_hyp orig le1 list_depends t2 @ loop ll
 	| [] -> [] in
       loop list_s1
 
 let destructurate_hyps syst =
   let rec loop = function
-      (i,t) :: l -> 
+      (i,t) :: l ->
 	let l_syst1 = destructurate_pos_hyp i []  [] t in
 	let l_syst2 = loop l in
 	list_cartesian (@) l_syst1 l_syst2
@@ -819,23 +819,23 @@ let destructurate_hyps syst =
 
 (* Affichage des dépendances de système *)
 let display_depend = function
-    Left i -> Printf.printf " L%d" i 
+    Left i -> Printf.printf " L%d" i
   | Right i -> Printf.printf " R%d" i
 
-let display_systems syst_list = 
-  let display_omega om_e = 
+let display_systems syst_list =
+  let display_omega om_e =
     Printf.printf "  E%d : %a %s 0\n"
       om_e.id
-      (fun _ -> display_eq display_omega_var) 
+      (fun _ -> display_eq display_omega_var)
       (om_e.body, om_e.constant)
       (operator_of_eq om_e.kind) in
 
-  let display_equation oformula_eq = 
+  let display_equation oformula_eq =
     pprint stdout (Pequa (Lazy.force coq_c_nop,oformula_eq)); print_newline ();
     display_omega oformula_eq.e_omega;
-    Printf.printf "  Depends on:"; 
+    Printf.printf "  Depends on:";
     List.iter display_depend oformula_eq.e_depends;
-    Printf.printf "\n  Path: %s" 
+    Printf.printf "\n  Path: %s"
       (String.concat ""
 	 (List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M")
 	    oformula_eq.e_origin.o_path));
@@ -852,10 +852,10 @@ let display_systems syst_list =
    calcul des hypothèses *)
 
 let rec hyps_used_in_trace = function
-  | act :: l -> 
+  | act :: l ->
       begin match act with
 	| HYP e -> [e.id] @@ (hyps_used_in_trace l)
-	| SPLIT_INEQ (_,(_,act1),(_,act2)) -> 
+	| SPLIT_INEQ (_,(_,act1),(_,act2)) ->
 	    hyps_used_in_trace act1 @@ hyps_used_in_trace act2
 	| _ -> hyps_used_in_trace l
       end
@@ -866,33 +866,33 @@ let rec hyps_used_in_trace = function
    éviter les créations de variable au vol *)
 
 let rec variable_stated_in_trace = function
-  | act :: l -> 
+  | act :: l ->
       begin match act with
 	| STATE action ->
 	    (*i nlle_equa: afine, def: afine, eq_orig: afine, i*)
             (*i coef: int, var:int                            i*)
 	    action :: variable_stated_in_trace l
-	| SPLIT_INEQ (_,(_,act1),(_,act2)) -> 
+	| SPLIT_INEQ (_,(_,act1),(_,act2)) ->
 	    variable_stated_in_trace act1 @ variable_stated_in_trace act2
 	| _ -> variable_stated_in_trace l
       end
   | [] -> []
 ;;
 
-let add_stated_equations env tree = 
+let add_stated_equations env tree =
   (* Il faut trier les variables par ordre d'introduction pour ne pas risquer
      de définir dans le mauvais ordre *)
-  let stated_equations = 
-    let cmpvar x y = Pervasives.(-) x.st_var y.st_var in 
+  let stated_equations =
+    let cmpvar x y = Pervasives.(-) x.st_var y.st_var in
     let rec loop = function
       | Tree(_,t1,t2) -> List.merge cmpvar (loop t1) (loop t2)
-      | Leaf s -> List.sort cmpvar (variable_stated_in_trace s.s_trace) 
+      | Leaf s -> List.sort cmpvar (variable_stated_in_trace s.s_trace)
     in loop tree
-  in 
-  let add_env st = 
+  in
+  let add_env st =
     (* On retransforme la définition de v en formule reifiée *)
     let v_def = oformula_of_omega env st.st_def in
-    (* Notez que si l'ordre de création des variables n'est pas respecté, 
+    (* Notez que si l'ordre de création des variables n'est pas respecté,
      * ca va planter *)
     let coq_v = coq_of_formula env v_def in
     let v = add_reified_atom coq_v env in
@@ -902,33 +902,33 @@ let add_stated_equations env tree =
      * l'environnement pour le faire correctement *)
     let term_to_reify = (v_def,Oatom v) in
     (* enregistre le lien entre la variable omega et la variable Coq *)
-    intern_omega_force env (Oatom v) st.st_var; 
+    intern_omega_force env (Oatom v) st.st_var;
     (v, term_to_generalize,term_to_reify,st.st_def.id) in
  List.map add_env stated_equations
 
-(* Calcule la liste des éclatements à réaliser sur les hypothèses 
+(* Calcule la liste des éclatements à réaliser sur les hypothèses
    nécessaires pour extraire une liste d'équations donnée *)
 
-(* PL: experimentally, the result order of the following function seems 
+(* PL: experimentally, the result order of the following function seems
    _very_ crucial for efficiency. No idea why. Do not remove the List.rev
-   or modify the current semantics of Util.list_union (some elements of first 
+   or modify the current semantics of Util.list_union (some elements of first
    arg, then second arg), unless you know what you're doing. *)
 
 let rec get_eclatement env = function
-    i :: r -> 
+    i :: r ->
       let l = try (get_equation env i).e_depends with Not_found -> [] in
       list_union (List.rev l) (get_eclatement env r)
   | [] -> []
 
-let select_smaller l = 
+let select_smaller l =
   let comp (_,x) (_,y) = Pervasives.(-) (List.length x) (List.length y) in
   try List.hd (List.sort comp l) with Failure _ -> failwith "select_smaller"
 
 let filter_compatible_systems required systems =
   let rec select = function
-      (x::l) -> 
+      (x::l) ->
 	if List.mem x required then select l
-	else if List.mem (barre x) required then failwith "Exit" 
+	else if List.mem (barre x) required then failwith "Exit"
 	else x :: select l
     | [] -> [] in
   map_succeed (function (sol,splits) -> (sol,select splits)) systems
@@ -938,8 +938,8 @@ let rec equas_of_solution_tree = function
   | Leaf s -> s.s_equa_deps
 
 (* [really_useful_prop] pushes useless props in a new Pprop variable *)
-(* Things get shorter, but may also get wrong, since a Prop is considered 
-   to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance 
+(* Things get shorter, but may also get wrong, since a Prop is considered
+   to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance
    Pfalse is decidable. So should not be used on conclusion (??) *)
 
 let really_useful_prop l_equa c =
@@ -953,21 +953,21 @@ let really_useful_prop l_equa c =
     (* Attention : implications sur le lifting des variables à comprendre ! *)
     | Pimp(_,t1,t2) -> Term.mkArrow (real_of t1) (real_of t2)
     | Pprop t -> t in
-  let rec loop c = 
-    match c with 
+  let rec loop c =
+    match c with
       Pequa(_,e) ->
 	if List.mem e.e_omega.id l_equa then Some c else None
     | Ptrue -> None
     | Pfalse -> None
-    | Pnot t1 -> 
+    | Pnot t1 ->
 	begin match loop t1 with None -> None | Some t1' -> Some (Pnot t1') end
     | Por(i,t1,t2) -> binop (fun (t1,t2) -> Por(i,t1,t2)) t1 t2
     | Pand(i,t1,t2) -> binop (fun (t1,t2) -> Pand(i,t1,t2)) t1 t2
     | Pimp(i,t1,t2) -> binop (fun (t1,t2) -> Pimp(i,t1,t2)) t1 t2
     | Pprop t -> None
-  and binop f t1 t2 = 
+  and binop f t1 t2 =
     begin match loop t1, loop t2 with
-      None, None -> None 
+      None, None -> None
     | Some t1',Some t2' -> Some (f(t1',t2'))
     | Some t1',None -> Some (f(t1',Pprop (real_of t2)))
     | None,Some t2' -> Some (f(Pprop (real_of t1),t2'))
@@ -977,36 +977,36 @@ let really_useful_prop l_equa c =
   | Some t -> t
 
 let rec display_solution_tree ch = function
-    Leaf t -> 
-      output_string ch 
-       (Printf.sprintf "%d[%s]" 
+    Leaf t ->
+      output_string ch
+       (Printf.sprintf "%d[%s]"
 	 t.s_index
          (String.concat " " (List.map string_of_int t.s_equa_deps)))
-  | Tree(i,t1,t2) -> 
-      Printf.fprintf ch "S%d(%a,%a)" i 
+  | Tree(i,t1,t2) ->
+      Printf.fprintf ch "S%d(%a,%a)" i
 	display_solution_tree t1 display_solution_tree t2
 
-let rec solve_with_constraints all_solutions path = 
+let rec solve_with_constraints all_solutions path =
   let rec build_tree sol buf = function
       [] -> Leaf sol
-    | (Left i :: remainder) -> 
+    | (Left i :: remainder) ->
 	Tree(i,
-	     build_tree sol (Left i :: buf) remainder, 
+	     build_tree sol (Left i :: buf) remainder,
 	     solve_with_constraints all_solutions (List.rev(Right i :: buf)))
-    | (Right i :: remainder) -> 
+    | (Right i :: remainder) ->
 	 Tree(i,
 	      solve_with_constraints all_solutions (List.rev (Left i ::  buf)),
 	      build_tree sol (Right i :: buf) remainder) in
   let weighted = filter_compatible_systems path all_solutions in
   let (winner_sol,winner_deps) =
-    try select_smaller weighted 
-    with e ->  
-      Printf.printf "%d - %d\n" 
+    try select_smaller weighted
+    with e ->
+      Printf.printf "%d - %d\n"
 	(List.length weighted) (List.length all_solutions);
       List.iter display_depend path; raise e in
-  build_tree winner_sol (List.rev path) winner_deps 
+  build_tree winner_sol (List.rev path) winner_deps
 
-let find_path {o_hyp=id;o_path=p} env = 
+let find_path {o_hyp=id;o_path=p} env =
   let rec loop_path = function
       ([],l) -> Some l
     | (x1::l1,x2::l2) when x1 = x2 -> loop_path (l1,l2)
@@ -1021,8 +1021,8 @@ let find_path {o_hyp=id;o_path=p} env =
     | [] -> failwith "find_path" in
   loop_id 0 env
 
-let mk_direction_list l = 
-  let trans = function 
+let mk_direction_list l =
+  let trans = function
       O_left -> coq_d_left | O_right -> coq_d_right | O_mono -> coq_d_mono in
   mk_list (Lazy.force coq_direction) (List.map (fun d-> Lazy.force(trans d)) l)
 
@@ -1036,33 +1036,33 @@ let get_hyp env_hyp i =
 let replay_history env env_hyp =
   let rec loop env_hyp t =
     match t with
-      | CONTRADICTION (e1,e2) :: l -> 
+      | CONTRADICTION (e1,e2) :: l ->
 	  let trace = mk_nat (List.length e1.body) in
 	  mkApp (Lazy.force coq_s_contradiction,
-		 [| trace ; mk_nat (get_hyp env_hyp e1.id); 
+		 [| trace ; mk_nat (get_hyp env_hyp e1.id);
 		    mk_nat (get_hyp env_hyp e2.id) |])
       | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
 	  mkApp (Lazy.force coq_s_div_approx,
-		 [| Z.mk k; Z.mk d; 
+		 [| Z.mk k; Z.mk d;
 		    reified_of_omega env e2.body e2.constant;
-		    mk_nat (List.length e2.body); 
+		    mk_nat (List.length e2.body);
 		    loop env_hyp l; mk_nat (get_hyp env_hyp e1.id) |])
       | NOT_EXACT_DIVIDE (e1,k) :: l ->
 	  let e2_constant = floor_div e1.constant k in
 	  let d = e1.constant - e2_constant * k in
 	  let e2_body = map_eq_linear (fun c -> c / k) e1.body in
           mkApp (Lazy.force coq_s_not_exact_divide,
-		 [|Z.mk k; Z.mk d; 
-		   reified_of_omega env e2_body e2_constant; 
-		   mk_nat (List.length e2_body); 
+		 [|Z.mk k; Z.mk d;
+		   reified_of_omega env e2_body e2_constant;
+		   mk_nat (List.length e2_body);
 		   mk_nat (get_hyp env_hyp e1.id)|])
       | EXACT_DIVIDE (e1,k) :: l ->
-	  let e2_body =  
+	  let e2_body =
 	    map_eq_linear (fun c -> c / k) e1.body in
 	  let e2_constant = floor_div e1.constant k in
           mkApp (Lazy.force coq_s_exact_divide,
-		 [|Z.mk k; 
-		   reified_of_omega env e2_body e2_constant; 
+		 [|Z.mk k;
+		   reified_of_omega env e2_body e2_constant;
 		   mk_nat (List.length e2_body);
 		   loop env_hyp l; mk_nat (get_hyp env_hyp e1.id)|])
       | (MERGE_EQ(e3,e1,e2)) :: l ->
@@ -1072,22 +1072,22 @@ let replay_history env env_hyp =
 		    mk_nat n1; mk_nat n2;
 		    loop (CCEqua e3:: env_hyp) l |])
       | SUM(e3,(k1,e1),(k2,e2)) :: l ->
-	  let n1 = get_hyp env_hyp e1.id 
+	  let n1 = get_hyp env_hyp e1.id
 	  and n2 = get_hyp env_hyp e2.id in
 	  let trace = shuffle_path k1 e1.body k2 e2.body in
           mkApp (Lazy.force coq_s_sum,
 		 [| Z.mk k1; mk_nat n1; Z.mk k2;
 		    mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |])
-      | CONSTANT_NOT_NUL(e,k) :: l -> 
+      | CONSTANT_NOT_NUL(e,k) :: l ->
           mkApp (Lazy.force coq_s_constant_not_nul,
 		 [|  mk_nat (get_hyp env_hyp e) |])
       | CONSTANT_NEG(e,k) :: l ->
           mkApp (Lazy.force coq_s_constant_neg,
 		 [|  mk_nat (get_hyp env_hyp e) |])
-      | STATE {st_new_eq=new_eq; st_def =def; 
+      | STATE {st_new_eq=new_eq; st_def =def;
 		      st_orig=orig; st_coef=m;
                       st_var=sigma } :: l ->
-	  let n1 = get_hyp env_hyp orig.id 
+	  let n1 = get_hyp env_hyp orig.id
 	  and n2 = get_hyp env_hyp def.id in
 	  let v = unintern_omega env sigma in
 	  let o_def = oformula_of_omega env def in
@@ -1096,26 +1096,26 @@ let replay_history env env_hyp =
 	     Oplus (o_orig,Omult (Oplus (Oopp v,o_def), Oint m)) in
           let trace,_ = normalize_linear_term env body in
 	  mkApp (Lazy.force coq_s_state,
-		 [| Z.mk m; trace; mk_nat n1; mk_nat n2; 
+		 [| Z.mk m; trace; mk_nat n1; mk_nat n2;
 		    loop (CCEqua new_eq.id :: env_hyp) l |])
       |	HYP _ :: l -> loop env_hyp l
       |	CONSTANT_NUL e :: l ->
-	  mkApp (Lazy.force coq_s_constant_nul, 
+	  mkApp (Lazy.force coq_s_constant_nul,
 		 [|  mk_nat (get_hyp env_hyp e) |])
       |	NEGATE_CONTRADICT(e1,e2,true) :: l ->
-	  mkApp (Lazy.force coq_s_negate_contradict, 
+	  mkApp (Lazy.force coq_s_negate_contradict,
 		 [|  mk_nat (get_hyp env_hyp e1.id);
 		     mk_nat (get_hyp env_hyp e2.id) |])
       |	NEGATE_CONTRADICT(e1,e2,false) :: l ->
-	  mkApp (Lazy.force coq_s_negate_contradict_inv, 
-		 [|  mk_nat (List.length e2.body); 
+	  mkApp (Lazy.force coq_s_negate_contradict_inv,
+		 [|  mk_nat (List.length e2.body);
 		     mk_nat (get_hyp env_hyp e1.id);
 		     mk_nat (get_hyp env_hyp e2.id) |])
       | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
 	  let i =  get_hyp env_hyp e.id in
 	  let r1 = loop (CCEqua e1 :: env_hyp) l1 in
 	  let r2 = loop (CCEqua e2 :: env_hyp) l2 in
-	  mkApp (Lazy.force coq_s_split_ineq, 
+	  mkApp (Lazy.force coq_s_split_ineq,
                   [| mk_nat (List.length e.body); mk_nat i; r1 ; r2 |])
       |	(FORGET_C _ | FORGET _ | FORGET_I _) :: l ->
 	  loop env_hyp l
@@ -1125,14 +1125,14 @@ let replay_history env env_hyp =
 
 let rec decompose_tree env ctxt = function
    Tree(i,left,right) ->
-     let org = 
-       try Hashtbl.find env.constructors i 
+     let org =
+       try Hashtbl.find env.constructors i
        with Not_found ->
 	 failwith (Printf.sprintf "Cannot find constructor %d" i) in
      let (index,path) = find_path org ctxt in
      let left_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_left]} in
      let right_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_right]} in
-     app coq_e_split 
+     app coq_e_split
        [| mk_nat index;
 	  mk_direction_list path;
 	  decompose_tree env (left_hyp::ctxt) left;
@@ -1141,15 +1141,15 @@ let rec decompose_tree env ctxt = function
       decompose_tree_hyps s.s_trace env ctxt  s.s_equa_deps
 and decompose_tree_hyps trace env ctxt = function
     [] -> app coq_e_solve [| replay_history env ctxt trace |]
-  | (i::l) -> 
+  | (i::l) ->
       let equation =
-        try Hashtbl.find env.equations i 
+        try Hashtbl.find env.equations i
         with Not_found ->
 	  failwith (Printf.sprintf "Cannot find equation %d" i) in
       let (index,path) = find_path equation.e_origin ctxt in
       let full_path = if equation.e_negated then path @ [O_mono] else path in
-      let cont = 
-	decompose_tree_hyps trace env 
+      let cont =
+	decompose_tree_hyps trace env
 	   (CCEqua equation.e_omega.id :: ctxt) l in
       app coq_e_extract [|mk_nat index;
 			  mk_direction_list full_path;
@@ -1165,13 +1165,13 @@ de faire rejouer cette solution par la tactique réflexive. *)
 
 let resolution env full_reified_goal systems_list =
   let num = ref 0 in
-  let solve_system list_eq = 
+  let solve_system list_eq =
     let index = !num in
     let system = List.map (fun eq -> eq.e_omega) list_eq in
-    let trace = 
-      simplify_strong 
-	(new_omega_eq,new_omega_var,display_omega_var) 
-	system in 
+    let trace =
+      simplify_strong
+	(new_omega_eq,new_omega_var,display_omega_var)
+	system in
     (* calcule les hypotheses utilisées pour la solution *)
     let vars = hyps_used_in_trace trace in
     let splits = get_eclatement env vars in
@@ -1201,11 +1201,11 @@ let resolution env full_reified_goal systems_list =
   let l_hyps = id_concl :: list_remove id_concl l_hyps' in
   let useful_hyps =
     List.map (fun id -> List.assoc id full_reified_goal) l_hyps in
-  let useful_vars = 
+  let useful_vars =
     let really_useful_vars = vars_of_equations equations in
-    let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in     
+    let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in
     really_useful_vars @@ concl_vars
-  in 
+  in
   (* variables a introduire *)
   let to_introduce = add_stated_equations env solution_tree in
   let stated_vars =  List.map (fun (v,_,_,_) -> v) to_introduce in
@@ -1217,19 +1217,19 @@ let resolution env full_reified_goal systems_list =
   let all_vars_env = useful_vars @ stated_vars in
   let basic_env =
     let rec loop i = function
-	var :: l -> 
-	  let t = get_reified_atom env var in 
+	var :: l ->
+	  let t = get_reified_atom env var in
 	  Hashtbl.add env.real_indices var i; t :: loop (succ i) l
       |	[] -> [] in
     loop 0 all_vars_env in
   let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in
   (* On peut maintenant généraliser le but : env est a jour *)
   let l_reified_stated =
-     List.map (fun (_,_,(l,r),_) -> 
-                 app coq_p_eq [| reified_of_formula env l; 
+     List.map (fun (_,_,(l,r),_) ->
+                 app coq_p_eq [| reified_of_formula env l;
                                  reified_of_formula env r |])
               to_introduce in
-  let reified_concl = 
+  let reified_concl =
     match useful_hyps with
       (Pnot p) :: _ -> reified_of_proposition env p
     | _ ->  reified_of_proposition env Pfalse in
@@ -1239,51 +1239,51 @@ let resolution env full_reified_goal systems_list =
          reified_of_proposition env (really_useful_prop useful_equa_id p))
       (List.tl useful_hyps)) in
   let env_props_reified = mk_plist env.props in
-  let reified_goal = 
+  let reified_goal =
     mk_list (Lazy.force coq_proposition)
             (l_reified_stated @ l_reified_terms) in
-  let reified = 
-    app coq_interp_sequent 
+  let reified =
+    app coq_interp_sequent
        [| reified_concl;env_props_reified;env_terms_reified;reified_goal|] in
-  let normalize_equation e = 
+  let normalize_equation e =
     let rec loop = function
 	[] -> app (if e.e_negated then coq_p_invert else coq_p_step)
 	          [| e.e_trace |]
       |	((O_left | O_mono) :: l) -> app coq_p_left [| loop l |]
       |	(O_right :: l) -> app coq_p_right [| loop l |] in
-    let correct_index = 
-      let i = list_index0 e.e_origin.o_hyp l_hyps in 
-      (* PL: it seems that additionnally introduced hyps are in the way during 
-             normalization, hence this index shifting... *) 
+    let correct_index =
+      let i = list_index0 e.e_origin.o_hyp l_hyps in
+      (* PL: it seems that additionnally introduced hyps are in the way during
+             normalization, hence this index shifting... *)
       if i=0 then 0 else Pervasives.(+) i (List.length to_introduce)
-    in 	
+    in
     app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in
   let normalization_trace =
     mk_list (Lazy.force coq_h_step) (List.map normalize_equation equations) in
 
   let initial_context =
     List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) (List.tl l_hyps) in
-  let context = 
+  let context =
     CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
   let decompose_tactic = decompose_tree env context solution_tree in
 
-  Tactics.generalize 
+  Tactics.generalize
     (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
-  Tactics.change_in_concl None reified >> 
+  Tactics.change_in_concl None reified >>
   Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
   show_goal >>
   Tactics.normalise_vm_in_concl >>
-  (*i Alternatives to the previous line: 
-   - Normalisation without VM: 
+  (*i Alternatives to the previous line:
+   - Normalisation without VM:
       Tactics.normalise_in_concl
-   - Skip the conversion check and rely directly on the QED: 
-      Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >> 
+   - Skip the conversion check and rely directly on the QED:
+      Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >>
   i*)
   Tactics.apply (Lazy.force coq_I)
 
-let total_reflexive_omega_tactic gl = 
+let total_reflexive_omega_tactic gl =
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
-  rst_omega_eq (); 
+  rst_omega_eq ();
   rst_omega_var ();
   try
   let env = new_environment () in