adaptation V8 version Pierre Cregut

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

6 files changed, 3249 insertions, 1174 deletions

diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index f1ffcf13d2..b3895b2a5a 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -7,4 +7,5 @@
  *************************************************************************)
 
 Require Import Omega.
-Require Import ReflOmegaCore.
\ No newline at end of file
+Require Import ReflOmegaCore.
+
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index b69f40df82..3dfb559395 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -1,25 +1,41 @@
 (*************************************************************************
 
    PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
-   Licence : LGPL version 2.1
+   Author: Pierre Crégut - France Télécom R&D
+   Licence du projet : LGPL version 2.1
 
  *************************************************************************)
 
 Require Import Arith.
 Require Import List.
 Require Import Bool.
-Require Import ZArith_base.
+Require Import ZArith.
 Require Import OmegaLemmas.
 
-(* \subsection{Définition des types} *)
-
-(* \subsubsection{Définition des termes dans Z réifiés}
-   Les termes comprennent les entiers relatifs [Tint] et les 
-   variables [Tvar] ainsi que les opérations de base sur Z (addition,
-   multiplication, opposé et soustraction). Les deux denières sont
-   rapidement traduites dans les deux premières durant la normalisation
-   des termes. *)
+(* \subsection{Definition of basic types} *)
+
+(* \subsubsection{Environment of propositions (lists) *)
+Inductive PropList : Type :=
+  | Pnil : PropList
+  | Pcons : Prop -> PropList -> PropList.
+
+(* Access function for the environment with a default *)
+Fixpoint nthProp (n : nat) (l : PropList) (default : Prop) {struct l} :
+ Prop :=
+  match n, l with
+  | O, Pcons x l' => x
+  | O, other => default
+  | S m, Pnil => default
+  | S m, Pcons x t => nthProp m t default
+  end.
+   
+(* \subsubsection{Définition of reified integer expressions}
+   Terms are either:
+   \begin{itemize}
+   \item integers [Tint]
+   \item variables [Tvar]
+   \item operation over integers (addition, product, opposite, subtraction)
+   The last two are translated in additions and products. *)
 
 Inductive term : Set :=
   | Tint : Z -> term
@@ -29,32 +45,47 @@ Inductive term : Set :=
   | Topp : term -> term
   | Tvar : nat -> term.
 
-(* \subsubsection{Définition des buts réifiés} *)
-(* Définition très restreinte des prédicats manipulés (à enrichir). 
-   La prise en compte des négations et des diséquations demande la
-   prise en compte de la résolution en parallèle de plusieurs buts.
-   Ceci n'est possible qu'en modifiant de manière drastique la définition
-   de normalize qui doit pouvoir générer des listes de buts. Il faut
-   donc aussi modifier la normalisation qui peut elle aussi amener la
-   génération d'une liste de but et donc l'application d'une liste de
-   tactiques de résolution ([execute_omega])  *)
+(* \subsubsection{Definition of reified goals} *)
+(* Very restricted definition of handled predicates that should be extended
+   to cover a wider set of operations.
+   Taking care of negations and disequations require solving more than a
+   goal in parallel. This is a major improvement over previous versions. *)
+
 Inductive proposition : Set :=
-  | EqTerm : term -> term -> proposition
-  | LeqTerm : term -> term -> proposition
-  | TrueTerm : proposition
-  | FalseTerm : proposition
-  | Tnot : proposition -> proposition
+  | EqTerm : term -> term -> proposition (* egalité entre termes *)
+  | LeqTerm : term -> term -> proposition (* plus petit ou egal *)
+  | TrueTerm : proposition (* vrai *)
+  | FalseTerm : proposition (* faux *)
+  | Tnot : proposition -> proposition (* négation *)
   | GeqTerm : term -> term -> proposition
   | GtTerm : term -> term -> proposition
   | LtTerm : term -> term -> proposition
-  | NeqTerm : term -> term -> proposition.
+  | NeqTerm : term -> term -> proposition
+  | Tor : proposition -> proposition -> proposition
+  | Tand : proposition -> proposition -> proposition
+  | Timp : proposition -> proposition -> proposition
+  | Tprop : nat -> proposition.
 
-(* Définition des hypothèses *)
-Notation hyps := (list proposition).      
+(* Definition of goals as a list of hypothesis *)
+Notation hyps := (list proposition) (only parsing).      
 
+(* Definition of lists of subgoals  (set of open goals) *)
+Notation lhyps := (list (list proposition)) (only parsing).
+
+(* a syngle goal packed in a subgoal list *)
+Notation singleton := (fun a : list proposition => a :: nil) (only parsing).
+
+(* an absurd goal *)
 Definition absurd := FalseTerm :: nil.
 
-(* \subsubsection{Traces de fusion d'équations} *)
+(* \subsubsection{Traces for merging equations}
+   This inductive type describes how the monomial of two equations should be
+   merged when the equations are added.
+
+   For [F_equal], both equations have the same head variable and coefficient
+   must be added, furthermore if coefficients are opposite, [F_cancel] should
+   be used to collapse the term. [F_left] and [F_right] indicate which monomial
+   should be put first in the result *)
 
 Inductive t_fusion : Set :=
   | F_equal : t_fusion
@@ -62,25 +93,135 @@ Inductive t_fusion : Set :=
   | F_left : t_fusion
   | F_right : t_fusion.
 
-(* \subsection{Egalité décidable efficace} *)
-(* Pour chaque type de donnée réifié, on calcule un test d'égalité efficace.
+(* \subsubsection{Rewriting steps to normalize terms} *)
+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 *)
+  | C_LEFT : step -> step
+             (* apply the rewriting step to the second branch *)
+  | C_RIGHT : step -> step
+              (* apply two steps consecutively to a term *)
+  | C_SEQ : step -> step -> step
+                    (* empty step *)
+  | C_NOP : step
+      (* the following operations correspond to actual rewriting *)
+  | C_OPP_PLUS : step
+  | C_OPP_OPP : step
+  | C_OPP_MULT_R : step
+  | C_OPP_ONE :
+      step
+      (* This is a special step that reduces the term (computation) *)
+  | C_REDUCE : step
+  | C_MULT_PLUS_DISTR : step
+  | C_MULT_OPP_LEFT : step
+  | C_MULT_ASSOC_R : step
+  | C_PLUS_ASSOC_R : step
+  | C_PLUS_ASSOC_L : step
+  | C_PLUS_PERMUTE : step
+  | C_PLUS_SYM : step
+  | C_RED0 : step
+  | C_RED1 : step
+  | C_RED2 : step
+  | C_RED3 : step
+  | C_RED4 : step
+  | C_RED5 : step
+  | C_RED6 : step
+  | C_MULT_ASSOC_REDUCED : step
+  | C_MINUS : step
+  | C_MULT_SYM : step.
+
+(* \subsubsection{Omega steps} *)
+(* The following inductive type describes steps as they can be found in
+   the trace coming from the decision procedure Omega. *)
+
+Inductive t_omega : Set :=
+ (* n = 0 n!= 0 *)
+  | O_CONSTANT_NOT_NUL : nat -> t_omega
+  | O_CONSTANT_NEG :
+      nat -> t_omega
+      (* division et approximation of an equation *)
+  | O_DIV_APPROX :
+      Z ->
+      Z ->
+      term ->
+      nat ->
+      t_omega -> nat -> t_omega
+                 (* no solution because no exact division *)
+  | O_NOT_EXACT_DIVIDE :
+      Z -> Z -> term -> nat -> nat -> t_omega
+                               (* exact division *)
+  | O_EXACT_DIVIDE : Z -> term -> nat -> t_omega -> nat -> t_omega
+  | O_SUM : Z -> nat -> Z -> nat -> list t_fusion -> t_omega -> t_omega
+  | O_CONTRADICTION : nat -> nat -> nat -> t_omega
+  | O_MERGE_EQ : nat -> nat -> nat -> t_omega -> t_omega
+  | O_SPLIT_INEQ : nat -> nat -> t_omega -> t_omega -> t_omega
+  | O_CONSTANT_NUL : nat -> t_omega
+  | O_NEGATE_CONTRADICT : nat -> nat -> t_omega
+  | O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega
+  | O_STATE : Z -> step -> nat -> nat -> t_omega -> t_omega.
+
+(* \subsubsection{Règles pour normaliser les hypothèses} *)
+(* Ces règles indiquent comment normaliser les propositions utiles 
+   de chaque hypothèse utile avant la décomposition des hypothèses et 
+   incluent l'étape d'inversion pour la suppression des négations *)
+Inductive p_step : Set :=
+  | P_LEFT : p_step -> p_step
+  | P_RIGHT : p_step -> p_step
+  | P_INVERT : step -> p_step
+  | P_STEP : step -> p_step
+  | P_NOP : p_step.
+(* Liste des normalisations a effectuer : avec un constructeur dans le
+   type [p_step] permettant
+   de parcourir à la fois les branches gauches et droit, on pourrait n'avoir
+   qu'une normalisation par hypothèse. Et comme toutes les hypothèses sont 
+   utiles (sinon on ne les incluerait pas), on pourrait remplacer [h_step] 
+   par une simple liste *)
+
+Inductive h_step : Set :=
+    pair_step : nat -> p_step -> h_step.
+
+(* \subsubsection{Règles pour décomposer les hypothèses} *)
+(* Ce type permet de se diriger dans les constructeurs logiques formant les
+   prédicats des hypothèses pour aller les décomposer. Ils permettent
+   en particulier d'extraire une hypothèse d'une conjonction avec
+   éventuellement le bon niveau de négations. *)
+
+Inductive direction : Set :=
+  | D_left : direction
+  | D_right : direction
+  | D_mono : direction.
+
+(* Ce type permet d'extraire les composants utiles des hypothèses : que ce
+   soit des hypothèses générées par éclatement d'une disjonction, ou 
+   des équations. Le constructeur terminal indique comment résoudre le système
+   obtenu en recourrant au type de trace d'Omega [t_omega] *)
+
+Inductive e_step : Set :=
+  | E_SPLIT : nat -> list direction -> e_step -> e_step -> e_step
+  | E_EXTRACT : nat -> list direction -> e_step -> e_step
+  | E_SOLVE : t_omega -> e_step.
+
+(* \subsection{Egalité décidable efficace} *)
+(* Pour chaque type de donnée réifié, on calcule un test d'égalité efficace.
    Ce n'est pas le cas de celui rendu par [Decide Equality].
    
-   Puis on prouve deux théorèmes permettant d'éliminer de telles égalités :
+   Puis on prouve deux théorèmes permettant d'éliminer de telles égalités :
    \begin{verbatim}
    (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2.
    (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2.
    \end{verbatim} *)
 
-(* Ces deux tactiques permettent de résoudre pas mal de cas. L'une pour
-   les théorèmes positifs, l'autre pour les théorèmes négatifs *)
+(* Ces deux tactiques permettent de résoudre pas mal de cas. L'une pour
+   les théorèmes positifs, l'autre pour les théorèmes négatifs *)
 
 Ltac absurd_case := simpl in |- *; intros; discriminate.
 Ltac trivial_case := unfold not in |- *; intros; discriminate.
 
 (* \subsubsection{Entiers naturels} *)
 
-Fixpoint eq_nat (t1 t2:nat) {struct t2} : bool :=
+Fixpoint eq_nat (t1 t2 : nat) {struct t2} : bool :=
   match t1 with
   | O => match t2 with
          | O => true
@@ -92,7 +233,7 @@ Fixpoint eq_nat (t1 t2:nat) {struct t2} : bool :=
             end
   end.
 
-Theorem eq_nat_true : forall t1 t2:nat, eq_nat t1 t2 = true -> t1 = t2.
+Theorem eq_nat_true : forall t1 t2 : nat, eq_nat t1 t2 = true -> t1 = t2.
 
 simple induction t1;
  [ intro t2; case t2; [ trivial | absurd_case ]
@@ -102,7 +243,7 @@ simple induction t1;
 
 Qed.
   
-Theorem eq_nat_false : forall t1 t2:nat, eq_nat t1 t2 = false -> t1 <> t2.
+Theorem eq_nat_false : forall t1 t2 : nat, eq_nat t1 t2 = false -> t1 <> t2.
 
 simple induction t1;
  [ intro t2; case t2; [ simpl in |- *; intros; discriminate | trivial_case ]
@@ -114,7 +255,7 @@ Qed.
 
 (* \subsubsection{Entiers positifs} *)
 
-Fixpoint eq_pos (p1 p2:positive) {struct p2} : bool :=
+Fixpoint eq_pos (p1 p2 : positive) {struct p2} : bool :=
   match p1 with
   | xI n1 => match p2 with
              | xI n2 => eq_pos n1 n2
@@ -130,7 +271,7 @@ Fixpoint eq_pos (p1 p2:positive) {struct p2} : bool :=
           end
   end.
 
-Theorem eq_pos_true : forall t1 t2:positive, eq_pos t1 t2 = true -> t1 = t2.
+Theorem eq_pos_true : forall t1 t2 : positive, eq_pos t1 t2 = true -> t1 = t2.
 
 simple induction t1;
  [ intros p H t2; case t2;
@@ -146,7 +287,7 @@ simple induction t1;
 Qed.
   
 Theorem eq_pos_false :
- forall t1 t2:positive, eq_pos t1 t2 = false -> t1 <> t2.
+ forall t1 t2 : positive, eq_pos t1 t2 = false -> t1 <> t2.
 
 simple induction t1;
  [ intros p H t2; case t2;
@@ -164,7 +305,7 @@ Qed.
 
 (* \subsubsection{Entiers relatifs} *)
 
-Definition eq_Z (z1 z2:Z) : bool :=
+Definition eq_Z (z1 z2 : Z) : bool :=
   match z1 with
   | Z0 => match z2 with
           | Z0 => true
@@ -180,7 +321,7 @@ Definition eq_Z (z1 z2:Z) : bool :=
                end
   end.
 
-Theorem eq_Z_true : forall t1 t2:Z, eq_Z t1 t2 = true -> t1 = t2.
+Theorem eq_Z_true : forall t1 t2 : Z, eq_Z t1 t2 = true -> t1 = t2.
 
 simple induction t1;
  [ intros t2; case t2; [ auto | absurd_case | absurd_case ]
@@ -195,7 +336,7 @@ simple induction t1;
 
 Qed.
 
-Theorem eq_Z_false : forall t1 t2:Z, eq_Z t1 t2 = false -> t1 <> t2.
+Theorem eq_Z_false : forall t1 t2 : Z, eq_Z t1 t2 = false -> t1 <> t2.
 
 simple induction t1;
  [ intros t2; case t2; [ absurd_case | trivial_case | trivial_case ]
@@ -211,9 +352,9 @@ simple induction t1;
        simplify_eq H0; auto ] ].
 Qed.
 
-(* \subsubsection{Termes réifiés} *)
+(* \subsubsection{Termes réifiés} *)
 
-Fixpoint eq_term (t1 t2:term) {struct t2} : bool :=
+Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
   match t1 with
   | Tint st1 => match t2 with
                 | Tint st2 => eq_Z st1 st2
@@ -221,17 +362,17 @@ Fixpoint eq_term (t1 t2:term) {struct t2} : bool :=
                 end
   | Tplus st11 st12 =>
       match t2 with
-      | Tplus st21 st22 => andb (eq_term st11 st21) (eq_term st12 st22)
+      | Tplus st21 st22 => eq_term st11 st21 && eq_term st12 st22
       | _ => false
       end
   | Tmult st11 st12 =>
       match t2 with
-      | Tmult st21 st22 => andb (eq_term st11 st21) (eq_term st12 st22)
+      | Tmult st21 st22 => eq_term st11 st21 && eq_term st12 st22
       | _ => false
       end
   | Tminus st11 st12 =>
       match t2 with
-      | Tminus st21 st22 => andb (eq_term st11 st21) (eq_term st12 st22)
+      | Tminus st21 st22 => eq_term st11 st21 && eq_term st12 st22
       | _ => false
       end
   | Topp st1 => match t2 with
@@ -244,7 +385,7 @@ Fixpoint eq_term (t1 t2:term) {struct t2} : bool :=
                 end
   end.  
 
-Theorem eq_term_true : forall t1 t2:term, eq_term t1 t2 = true -> t1 = t2.
+Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2.
 
 
 simple induction t1; intros until t2; case t2; try absurd_case; simpl in |- *;
@@ -263,7 +404,8 @@ simple induction t1; intros until t2; case t2; try absurd_case; simpl in |- *;
 
 Qed.
 
-Theorem eq_term_false : forall t1 t2:term, eq_term t1 t2 = false -> t1 <> t2.
+Theorem eq_term_false :
+ forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2.
 
 simple induction t1;
  [ intros z t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *;
@@ -293,29 +435,29 @@ simple induction t1;
 
 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 
    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 
-   tel test préserve bien l'information voulue mais calculatoirement de
+   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 
+   tel test préserve bien l'information voulue mais calculatoirement de
    telles fonctions sont trop lentes. *)
 
-(* Le théorème suivant permet de garder dans les hypothèses la valeur
-   du booléen lors de l'élimination. *)
+(* Le théorème suivant permet de garder dans les hypothèses la valeur
+   du booléen lors de l'élimination. *)
 
 Theorem bool_ind2 :
- forall (P:bool -> Prop) (b:bool),
-   (b = true -> P true) -> (b = false -> P false) -> P b.
+ forall (P : bool -> Prop) (b : bool),
+ (b = true -> P true) -> (b = false -> P false) -> P b.
 
 simple induction b; auto.
 Qed.
 
-(* Les tactiques définies si après se comportent exactement comme si on
-   avait utilisé le test précédent et fait une elimination dessus. *)
+(* Les tactiques définies si après se comportent exactement comme si on
+   avait utilisé le test précédent et fait une elimination dessus. *)
 
 Ltac elim_eq_term t1 t2 :=
   pattern (eq_term t1 t2) in |- *; apply bool_ind2; intro Aux;
@@ -334,24 +476,24 @@ Ltac elim_eq_pos t1 t2 :=
 
 (* \subsubsection{Comparaison sur Z} *)
 
-(* Sujet très lié au précédent : on introduit la tactique d'élimination
-   avec son théorème *)
+(* Sujet très lié au précédent : on introduit la tactique d'élimination
+   avec son théorème *)
 
 Theorem relation_ind2 :
- forall (P:Datatypes.comparison -> Prop) (b:Datatypes.comparison),
-   (b = Datatypes.Eq -> P Datatypes.Eq) ->
-   (b = Datatypes.Lt -> P Datatypes.Lt) ->
-   (b = Datatypes.Gt -> P Datatypes.Gt) -> P b.
+ forall (P : Datatypes.comparison -> Prop) (b : Datatypes.comparison),
+ (b = Datatypes.Eq -> P Datatypes.Eq) ->
+ (b = Datatypes.Lt -> P Datatypes.Lt) ->
+ (b = Datatypes.Gt -> P Datatypes.Gt) -> P b.
 
 simple induction b; auto.
 Qed.
 
 Ltac elim_Zcompare t1 t2 := pattern (t1 ?= t2)%Z in |- *; apply relation_ind2.
 
-(* \subsection{Interprétations}
-   \subsubsection{Interprétation des termes dans Z} *)
+(* \subsection{Interprétations}
+   \subsubsection{Interprétation des termes dans Z} *)
 
-Fixpoint interp_term (env:list Z) (t:term) {struct t} : Z :=
+Fixpoint interp_term (env : list Z) (t : term) {struct t} : Z :=
   match t with
   | Tint x => x
   | Tplus t1 t2 => (interp_term env t1 + interp_term env t2)%Z
@@ -361,48 +503,65 @@ Fixpoint interp_term (env:list Z) (t:term) {struct t} : Z :=
   | Tvar n => nth n env 0%Z
   end.
 
-(* \subsubsection{Interprétation des prédicats} *) 
-Fixpoint interp_proposition (env:list Z) (p:proposition) {struct p} : Prop :=
+(* \subsubsection{Interprétation des prédicats} *) 
+Fixpoint interp_proposition (envp : PropList) (env : list Z)
+ (p : proposition) {struct p} : Prop :=
   match p with
   | EqTerm t1 t2 => interp_term env t1 = interp_term env t2
   | LeqTerm t1 t2 => (interp_term env t1 <= interp_term env t2)%Z
   | TrueTerm => True
   | FalseTerm => False
-  | Tnot p' => ~ interp_proposition env p'
+  | Tnot p' => ~ interp_proposition envp env p'
   | GeqTerm t1 t2 => (interp_term env t1 >= interp_term env t2)%Z
   | GtTerm t1 t2 => (interp_term env t1 > interp_term env t2)%Z
   | LtTerm t1 t2 => (interp_term env t1 < interp_term env t2)%Z
   | NeqTerm t1 t2 => Zne (interp_term env t1) (interp_term env t2)
+  | Tor p1 p2 =>
+      interp_proposition envp env p1 \/ interp_proposition envp env p2
+  | Tand p1 p2 =>
+      interp_proposition envp env p1 /\ interp_proposition envp env p2
+  | Timp p1 p2 =>
+      interp_proposition envp env p1 -> interp_proposition envp env p2
+  | Tprop n => nthProp n envp True
   end.
 
-(* \subsubsection{Inteprétation des listes d'hypothèses}
+(* \subsubsection{Inteprétation des listes d'hypothèses}
    \paragraph{Sous forme de conjonction}
-   Interprétation sous forme d'une conjonction d'hypothèses plus faciles
-   à manipuler individuellement *)
+   Interprétation sous forme d'une conjonction d'hypothèses plus faciles
+   à manipuler individuellement *)
 
-Fixpoint interp_hyps (env:list Z) (l:hyps) {struct l} : Prop :=
+Fixpoint interp_hyps (envp : PropList) (env : list Z) 
+ (l : list proposition) {struct l} : Prop :=
   match l with
   | nil => True
-  | p' :: l' => interp_proposition env p' /\ interp_hyps env l'
+  | p' :: l' => interp_proposition envp env p' /\ interp_hyps envp env l'
   end.
 
-(* \paragraph{Sous forme de but}
-   C'est cette interpétation que l'on utilise sur le but (car on utilise
-   [Generalize] et qu'une conjonction est forcément lourde (répétition des
-   types dans les conjonctions intermédiaires) *)
+(* \paragraph{sous forme de but}
+   C'est cette interpétation que l'on utilise sur le but (car on utilise
+   [Generalize] et qu'une conjonction est forcément lourde (répétition des
+   types dans les conjonctions intermédiaires) *)
 
-Fixpoint interp_goal (env:list Z) (l:hyps) {struct l} : Prop :=
+Fixpoint interp_goal_concl (envp : PropList) (env : list Z) 
+ (c : proposition) (l : list proposition) {struct l} : Prop :=
   match l with
-  | nil => False
-  | p' :: l' => interp_proposition env p' -> interp_goal env l'
+  | nil => interp_proposition envp env c
+  | p' :: l' =>
+      interp_proposition envp env p' -> interp_goal_concl envp env c l'
   end.
 
-(* Les théorèmes qui suivent assurent la correspondance entre les deux
-   interprétations. *)
+Notation interp_goal :=
+  (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+   interp_goal_concl envp env FalseTerm l) (only parsing).
+
+(* Les théorèmes qui suivent assurent la correspondance entre les deux
+   interprétations. *)
 
 Theorem goal_to_hyps :
- forall (env:list Z) (l:hyps),
-   (interp_hyps env l -> False) -> interp_goal env l.
+ forall (envp : PropList) (env : list Z) (l : list proposition),
+ (interp_hyps envp env l -> False) ->
+ (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+  interp_goal_concl envp env FalseTerm l) envp env l.
 
 simple induction l;
  [ simpl in |- *; auto
@@ -410,71 +569,84 @@ simple induction l;
 Qed.
 
 Theorem hyps_to_goal :
- forall (env:list Z) (l:hyps),
-   interp_goal env l -> interp_hyps env l -> False.
+ forall (envp : PropList) (env : list Z) (l : list proposition),
+ (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+  interp_goal_concl envp env FalseTerm l) envp env l ->
+ interp_hyps envp env l -> False.
 
 simple induction l; simpl in |- *; [ auto | intros; apply H; elim H1; auto ].
 Qed.
       
-(* \subsection{Manipulations sur les hypothèses} *)
+(* \subsection{Manipulations sur les hypothèses} *)
 
-(* \subsubsection{Définitions de base de stabilité pour la réflexion} *)
-(* Une opération laisse un terme stable si l'égalité est préservée *)
-Definition term_stable (f:term -> term) :=
-  forall (e:list Z) (t:term), interp_term e t = interp_term e (f t).
+(* \subsubsection{Définitions de base de stabilité pour la réflexion} *)
+(* Une opération laisse un terme stable si l'égalité est préservée *)
+Definition term_stable (f : term -> term) :=
+  forall (e : list Z) (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 
-   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
+(* 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 
+   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). *)
 
-Definition valid1 (f:proposition -> proposition) :=
-  forall (e:list Z) (p1:proposition),
-    interp_proposition e p1 -> interp_proposition e (f p1).
+Definition valid1 (f : proposition -> proposition) :=
+  forall (ep : PropList) (e : list Z) (p1 : proposition),
+  interp_proposition ep e p1 -> interp_proposition ep e (f p1).
 
-Definition valid2 (f:proposition -> proposition -> proposition) :=
-  forall (e:list Z) (p1 p2:proposition),
-    interp_proposition e p1 ->
-    interp_proposition e p2 -> interp_proposition e (f p1 p2).
+Definition valid2 (f : proposition -> proposition -> proposition) :=
+  forall (ep : PropList) (e : list Z) (p1 p2 : 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 propositions. 
+(* 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 (e:list Z) (lp:hyps), interp_hyps e lp -> interp_hyps e (f lp).
+Definition valid_hyps (f : list proposition -> list proposition) :=
+  forall (ep : PropList) (e : list Z) (lp : list proposition),
+  interp_hyps ep e lp -> interp_hyps ep e (f lp).
 
-(* Enfin ce théorème élimine la contravariance et nous ramène à une 
-   opération sur les buts *)
+(* Enfin ce théorème élimine la contravariance et nous ramène à une 
+   opération sur les buts *)
 
-Theorem valid_goal :
- forall (env:list Z) (l:hyps) (a:hyps -> hyps),
-   valid_hyps a -> interp_goal env (a l) -> interp_goal env l.
+ Theorem valid_goal :
+  forall (ep : PropList) (env : list Z) (l : list proposition)
+    (a : list proposition -> list proposition),
+  valid_hyps a ->
+  (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+   interp_goal_concl envp env FalseTerm l) ep env (
+    a l) ->
+  (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+   interp_goal_concl envp env FalseTerm l) ep env l.
 
-intros; apply goal_to_hyps; intro H1; apply (hyps_to_goal env (a l) H0);
- apply H; assumption.
+intros; simpl in |- *; apply goal_to_hyps; intro H1;
+ apply (hyps_to_goal ep env (a l) H0); apply H; assumption.
 Qed.
 
-(* \subsubsection{Généralisation à des listes de buts (disjonctions)} *)
+(* \subsubsection{Généralisation a des listes de buts (disjonctions)} *)
 
-Notation lhyps := (list hyps).
 
-Fixpoint interp_list_hyps (env:list Z) (l:lhyps) {struct l} : Prop :=
+Fixpoint interp_list_hyps (envp : PropList) (env : list Z)
+ (l : list (list proposition)) {struct l} : Prop :=
   match l with
   | nil => False
-  | h :: l' => interp_hyps env h \/ interp_list_hyps env l'
+  | h :: l' => interp_hyps envp env h \/ interp_list_hyps envp env l'
   end.
 
-Fixpoint interp_list_goal (env:list Z) (l:lhyps) {struct l} : Prop :=
+Fixpoint interp_list_goal (envp : PropList) (env : list Z)
+ (l : list (list proposition)) {struct l} : Prop :=
   match l with
   | nil => True
-  | h :: l' => interp_goal env h /\ interp_list_goal env l'
+  | h :: l' =>
+      (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+       interp_goal_concl envp env FalseTerm l) envp env h /\
+      interp_list_goal envp env l'
   end.
 
 Theorem list_goal_to_hyps :
- forall (env:list Z) (l:lhyps),
-   (interp_list_hyps env l -> False) -> interp_list_goal env l.
+ forall (envp : PropList) (env : list Z) (l : list (list proposition)),
+ (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l.
 
 simple induction l; simpl in |- *;
  [ auto
@@ -484,35 +656,42 @@ simple induction l; simpl in |- *;
 Qed.
 
 Theorem list_hyps_to_goal :
- forall (env:list Z) (l:lhyps),
-   interp_list_goal env l -> interp_list_hyps env l -> False.
+ forall (envp : PropList) (env : list Z) (l : list (list proposition)),
+ interp_list_goal envp env l -> interp_list_hyps envp env l -> False.
 
 simple induction l; simpl in |- *;
  [ auto
- | intros h1 l1 H [H1 H2] H3; elim H3; intro H4;
+ | intros h1 l1 H (H1, H2) H3; elim H3; intro H4;
     [ apply hyps_to_goal with (1 := H1); assumption | auto ] ].
 Qed.
 
-Definition valid_list_hyps (f:hyps -> lhyps) :=
-  forall (e:list Z) (lp:hyps), interp_hyps e lp -> interp_list_hyps e (f lp).
+Definition valid_list_hyps
+  (f : list proposition -> list (list proposition)) :=
+  forall (ep : PropList) (e : list Z) (lp : list proposition),
+  interp_hyps ep e lp -> interp_list_hyps ep e (f lp).
 
-Definition valid_list_goal (f:hyps -> lhyps) :=
-  forall (e:list Z) (lp:hyps), interp_list_goal e (f lp) -> interp_goal e lp.
+Definition valid_list_goal
+  (f : list proposition -> list (list proposition)) :=
+  forall (ep : PropList) (e : list Z) (lp : list proposition),
+  interp_list_goal ep e (f lp) ->
+  (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+   interp_goal_concl envp env FalseTerm l) ep e lp.
 
 Theorem goal_valid :
- forall f:hyps -> lhyps, valid_list_hyps f -> valid_list_goal f.
+ forall f : list proposition -> list (list proposition),
+ valid_list_hyps f -> valid_list_goal f.
 
-unfold valid_list_goal in |- *; intros f H e lp H1; apply goal_to_hyps;
+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); 
- apply (H e lp); assumption.
+ apply (H ep e lp); assumption.
 Qed.
  
 Theorem append_valid :
- forall (e:list Z) (l1 l2:lhyps),
-   interp_list_hyps e l1 \/ interp_list_hyps e l2 ->
-   interp_list_hyps e (l1 ++ l2).
+ forall (ep : PropList) (e : list Z) (l1 l2 : list (list proposition)),
+ interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 ->
+ interp_list_hyps ep e (l1 ++ l2).
 
-intros e; simple induction l1;
+intros ep e; simple induction l1;
  [ simpl in |- *; intros l2 [H| H]; [ contradiction | trivial ]
  | simpl in |- *; intros h1 t1 HR l2 [[H| H]| H];
     [ auto
@@ -521,14 +700,14 @@ intros e; simple induction l1;
 
 Qed.
 
-(* \subsubsection{Opérateurs valides sur les hypothèses} *)
+(* \subsubsection{Opérateurs valides sur les hypothèses} *)
 
-(* Extraire une hypothèse de la liste *)
-Definition nth_hyps (n:nat) (l:hyps) := nth n l TrueTerm.
+(* Extraire une hypothèse de la liste *)
+Definition nth_hyps (n : nat) (l : list proposition) := nth n l TrueTerm.
 
 Theorem nth_valid :
- forall (e:list Z) (i:nat) (l:hyps),
-   interp_hyps e l -> interp_proposition e (nth_hyps i l).
+ forall (ep : PropList) (e : list Z) (i : nat) (l : list proposition),
+ interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l).
 
 unfold nth_hyps in |- *; simple induction i;
  [ simple induction l; simpl in |- *; [ auto | intros; elim H0; auto ]
@@ -537,24 +716,24 @@ unfold nth_hyps in |- *; simple induction i;
     | intros; simpl in |- *; apply H; elim H1; auto ] ].
 Qed.
 
-(* 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) :=
+(* 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 : list proposition) :=
   f (nth_hyps i l) (nth_hyps j l) :: l.
 
 Theorem apply_oper_2_valid :
- forall (i j:nat) (f:proposition -> proposition -> proposition),
-   valid2 f -> valid_hyps (apply_oper_2 i j f).
+ forall (i j : nat) (f : proposition -> proposition -> proposition),
+ valid2 f -> valid_hyps (apply_oper_2 i j f).
 
 intros i j f Hf; unfold apply_oper_2, valid_hyps in |- *; simpl in |- *;
  intros lp Hlp; split; [ apply Hf; apply nth_valid; assumption | assumption ].
 Qed.
 
-(* Modifier une hypothèse par application d'une opération valide *)
+(* Modifier une hypothèse par application d'une opération valide *)
 
-Fixpoint apply_oper_1 (i:nat) (f:proposition -> proposition) 
- (l:hyps) {struct i} : hyps :=
+Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition)
+ (l : list proposition) {struct i} : list proposition :=
   match l with
   | nil => nil (A:=proposition)
   | p :: l' =>
@@ -565,28 +744,28 @@ Fixpoint apply_oper_1 (i:nat) (f:proposition -> proposition)
   end.
 
 Theorem apply_oper_1_valid :
- forall (i:nat) (f:proposition -> proposition),
-   valid1 f -> valid_hyps (apply_oper_1 i f).
+ forall (i : nat) (f : proposition -> proposition),
+ valid1 f -> valid_hyps (apply_oper_1 i f).
 
-unfold valid_hyps in |- *; intros i f Hf e; elim i;
+unfold valid_hyps in |- *; intros i f Hf ep e; elim i;
  [ intro lp; case lp;
     [ simpl in |- *; trivial
-    | simpl in |- *; intros p l' [H1 H2]; split;
+    | simpl in |- *; intros p l' (H1, H2); split;
        [ apply Hf with (1 := H1) | assumption ] ]
  | intros n Hrec lp; case lp;
     [ simpl in |- *; auto
-    | simpl in |- *; intros p l' [H1 H2]; split;
+    | simpl in |- *; intros p l' (H1, H2); split;
        [ assumption | apply Hrec; assumption ] ] ].
 
 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 
+   réécriture sur un sous terme du terme principal. Avec la composition,
+   cela permet de construire des réécritures complexes proches des 
    tactiques de conversion *)
 
-Definition apply_left (f:term -> term) (t:term) :=
+Definition apply_left (f : term -> term) (t : term) :=
   match t with
   | Tplus x y => Tplus (f x) y
   | Tmult x y => Tmult (f x) y
@@ -594,92 +773,93 @@ Definition apply_left (f:term -> term) (t:term) :=
   | x => x
   end.
 
-Definition apply_right (f:term -> term) (t:term) :=
+Definition apply_right (f : term -> term) (t : term) :=
   match t with
   | Tplus x y => Tplus x (f y)
   | Tmult x y => Tmult x (f y)
   | x => x
   end.
 
-Definition apply_both (f g:term -> term) (t:term) :=
+Definition apply_both (f g : term -> term) (t : term) :=
   match t with
   | Tplus x y => Tplus (f x) (g y)
   | Tmult x y => Tmult (f x) (g y)
   | 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 :
- forall f:term -> term, term_stable f -> term_stable (apply_left f).
+ forall f : term -> term, term_stable f -> term_stable (apply_left f).
 
 unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *;
  intros; elim H; trivial.
 Qed.
 
 Theorem apply_right_stable :
- forall f:term -> term, term_stable f -> term_stable (apply_right f).
+ forall f : term -> term, term_stable f -> term_stable (apply_right f).
 
 unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *;
  intros t0 t1; elim H; trivial.
 Qed.
 
 Theorem apply_both_stable :
- forall f g:term -> term,
-   term_stable f -> term_stable g -> term_stable (apply_both f g).
+ forall f g : term -> term,
+ term_stable f -> term_stable g -> term_stable (apply_both f g).
 
 unfold term_stable in |- *; intros f g H1 H2 e t; case t; auto; simpl in |- *;
  intros t0 t1; elim H1; elim H2; trivial.
 Qed.
 
 Theorem compose_term_stable :
- forall f g:term -> term,
-   term_stable f -> term_stable g -> term_stable (fun t:term => f (g t)).
+ forall f g : term -> term,
+ term_stable f -> term_stable g -> term_stable (fun t : term => f (g t)).
 
 unfold term_stable in |- *; intros f g Hf Hg e t; elim Hf; apply Hg.
 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 
-   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. 
+(* \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 
+   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. 
 
-   Cette tactique itère la décomposition des Case. Elle est
-   constituée de deux fonctions s'appelant mutuellement :
+   Cette tactique itère la décomposition des Case. Elle est
+   constituée de deux fonctions s'appelant mutuellement :
    \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. 
+    \item une fonction récursive qui décompose ce but. Quand elle a trouvé un
+          Case, elle l'élimine. 
    \end{itemize}  
-   Les motifs sur les cas sont très imparfaits et dans certains cas, il
+   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 
    utilise le bon type.
 
-   Chaque élimination introduit correctement exactement le nombre d'hypothèses
-   nécessaires et conserve dans le cas d'une égalité la connaissance du
-   résultat du test en faisant la réécriture. Pour un test de comparaison,
-   on conserve simplement le résultat.
+   Chaque élimination introduit correctement exactement le nombre d'hypothèses
+   nécessaires et conserve dans le cas d'une égalité la connaissance du
+   résultat du test en faisant la réécriture. Pour un test de comparaison,
+   on conserve simplement le résultat.
 
-   Cette fonction déborde très largement la résolution des réécritures
+   Cette fonction déborde très largement la résolution des réécritures
    simples et fait une bonne partie des preuves des pas de Omega.
 *)
 
-(* \subsubsection{La tactique pour prouver la stabilité} *)
+(* \subsubsection{La tactique pour prouver la stabilité} *)
+
 Ltac loop t :=
   match constr:t with
   | (?X1 = ?X2) => 
                     (* Global *)
                     loop X1 || loop X2
   | (_ -> ?X1) => loop X1
-  | (interp_hyps _ ?X1) =>
+  | (interp_hyps _ _ ?X1) =>
       
-  (* Interprétations *)
+  (* Interpretations *)
   loop X1
-  | (interp_list_hyps _ ?X1) => loop X1
-  | (interp_proposition _ ?X1) => loop X1
+  | (interp_list_hyps _ _ ?X1) => loop X1
+  | (interp_proposition _ _ ?X1) => loop X1
   | (interp_term _ ?X1) => loop X1
   | (EqTerm ?X1 ?X2) =>
       
@@ -704,6 +884,10 @@ Ltac loop t :=
     | GtTerm x x0 => _
     | LtTerm x x0 => _
     | NeqTerm x x0 => _
+    | Tor x x0 => _
+    | Tand x x0 => _
+    | Timp x x0 => _
+    | Tprop x => _
     end =>
       
        (* Eliminations *)
@@ -716,7 +900,11 @@ Ltac loop t :=
        | intro; intro
        | intro; intro
        | intro; intro
-       | intro; intro ]; auto; Simplify
+       | intro; intro
+       | intro; intro
+       | intro; intro
+       | intro; intro
+       | intro ]; auto; Simplify
   | match ?X1 with
     | Tint x => _
     | Tplus x x0 => _
@@ -756,11 +944,16 @@ Ltac loop t :=
                   | _ => idtac
                   end.
 
+
 Ltac prove_stable x th :=
-  unfold term_stable, x in |- *; intros; Simplify; simpl in |- *; apply th.
+  match constr:x with
+  | ?X1 =>
+      unfold term_stable, X1 in |- *; intros; Simplify; simpl in |- *;
+       apply th
+  end.
 
-(* \subsubsection{Les règles elle mêmes} *)
-Definition Tplus_assoc_l (t:term) :=
+(* \subsubsection{Les règles elle mêmes} *)
+Definition Tplus_assoc_l (t : term) :=
   match t with
   | Tplus n (Tplus m p) => Tplus (Tplus n m) p
   | _ => t
@@ -771,7 +964,7 @@ Theorem Tplus_assoc_l_stable : term_stable Tplus_assoc_l.
 prove_stable Tplus_assoc_l Zplus_assoc.
 Qed.
 
-Definition Tplus_assoc_r (t:term) :=
+Definition Tplus_assoc_r (t : term) :=
   match t with
   | Tplus (Tplus n m) p => Tplus n (Tplus m p)
   | _ => t
@@ -782,7 +975,7 @@ Theorem Tplus_assoc_r_stable : term_stable Tplus_assoc_r.
 prove_stable Tplus_assoc_r Zplus_assoc_reverse.
 Qed.
 
-Definition Tmult_assoc_r (t:term) :=
+Definition Tmult_assoc_r (t : term) :=
   match t with
   | Tmult (Tmult n m) p => Tmult n (Tmult m p)
   | _ => t
@@ -793,7 +986,7 @@ Theorem Tmult_assoc_r_stable : term_stable Tmult_assoc_r.
 prove_stable Tmult_assoc_r Zmult_assoc_reverse.
 Qed.
 
-Definition Tplus_permute (t:term) :=
+Definition Tplus_permute (t : term) :=
   match t with
   | Tplus n (Tplus m p) => Tplus m (Tplus n p)
   | _ => t
@@ -804,7 +997,7 @@ Theorem Tplus_permute_stable : term_stable Tplus_permute.
 prove_stable Tplus_permute Zplus_permute.
 Qed.
 
-Definition Tplus_sym (t:term) :=
+Definition Tplus_sym (t : term) :=
   match t with
   | Tplus x y => Tplus y x
   | _ => t
@@ -815,7 +1008,7 @@ Theorem Tplus_sym_stable : term_stable Tplus_sym.
 prove_stable Tplus_sym Zplus_comm.
 Qed.
 
-Definition Tmult_sym (t:term) :=
+Definition Tmult_sym (t : term) :=
   match t with
   | Tmult x y => Tmult y x
   | _ => t
@@ -826,7 +1019,7 @@ Theorem Tmult_sym_stable : term_stable Tmult_sym.
 prove_stable Tmult_sym Zmult_comm.
 Qed.
 
-Definition T_OMEGA10 (t:term) :=
+Definition T_OMEGA10 (t : term) :=
   match t with
   | Tplus (Tmult (Tplus (Tmult v (Tint c1)) l1) (Tint k1)) (Tmult (Tplus
     (Tmult v' (Tint c2)) l2) (Tint k2)) =>
@@ -844,7 +1037,7 @@ Theorem T_OMEGA10_stable : term_stable T_OMEGA10.
 prove_stable T_OMEGA10 OMEGA10.
 Qed.
 
-Definition T_OMEGA11 (t:term) :=
+Definition T_OMEGA11 (t : term) :=
   match t with
   | Tplus (Tmult (Tplus (Tmult v1 (Tint c1)) l1) (Tint k1)) l2 =>
       Tplus (Tmult v1 (Tint (c1 * k1))) (Tplus (Tmult l1 (Tint k1)) l2)
@@ -856,7 +1049,7 @@ Theorem T_OMEGA11_stable : term_stable T_OMEGA11.
 prove_stable T_OMEGA11 OMEGA11.
 Qed.
 
-Definition T_OMEGA12 (t:term) :=
+Definition T_OMEGA12 (t : term) :=
   match t with
   | Tplus l1 (Tmult (Tplus (Tmult v2 (Tint c2)) l2) (Tint k2)) =>
       Tplus (Tmult v2 (Tint (c2 * k2))) (Tplus l1 (Tmult l2 (Tint k2)))
@@ -868,7 +1061,7 @@ Theorem T_OMEGA12_stable : term_stable T_OMEGA12.
 prove_stable T_OMEGA12 OMEGA12.
 Qed. 
 
-Definition T_OMEGA13 (t:term) :=
+Definition T_OMEGA13 (t : term) :=
   match t with
   | Tplus (Tplus (Tmult v (Tint (Zpos x))) l1) (Tplus (Tmult v' (Tint (Zneg
     x'))) l2) =>
@@ -897,7 +1090,7 @@ unfold term_stable, T_OMEGA13 in |- *; intros; Simplify; simpl in |- *;
  [ apply OMEGA13 | apply OMEGA14 ].
 Qed.
 
-Definition T_OMEGA15 (t:term) :=
+Definition T_OMEGA15 (t : term) :=
   match t with
   | Tplus (Tplus (Tmult v (Tint c1)) l1) (Tmult (Tplus (Tmult v' (Tint c2))
     l2) (Tint k2)) =>
@@ -915,7 +1108,7 @@ Theorem T_OMEGA15_stable : term_stable T_OMEGA15.
 prove_stable T_OMEGA15 OMEGA15.
 Qed.
 
-Definition T_OMEGA16 (t:term) :=
+Definition T_OMEGA16 (t : term) :=
   match t with
   | Tmult (Tplus (Tmult v (Tint c)) l) (Tint k) =>
       Tplus (Tmult v (Tint (c * k))) (Tmult l (Tint k))
@@ -928,7 +1121,7 @@ Theorem T_OMEGA16_stable : term_stable T_OMEGA16.
 prove_stable T_OMEGA16 OMEGA16.
 Qed.
 
-Definition Tred_factor5 (t:term) :=
+Definition Tred_factor5 (t : term) :=
   match t with
   | Tplus (Tmult x (Tint Z0)) y => y
   | _ => t
@@ -940,7 +1133,7 @@ Theorem Tred_factor5_stable : term_stable Tred_factor5.
 prove_stable Tred_factor5 Zred_factor5.
 Qed.
 
-Definition Topp_plus (t:term) :=
+Definition Topp_plus (t : term) :=
   match t with
   | Topp (Tplus x y) => Tplus (Topp x) (Topp y)
   | _ => t
@@ -952,7 +1145,7 @@ prove_stable Topp_plus Zopp_plus_distr.
 Qed.
 
 
-Definition Topp_opp (t:term) :=
+Definition Topp_opp (t : term) :=
   match t with
   | Topp (Topp x) => x
   | _ => t
@@ -963,7 +1156,7 @@ Theorem Topp_opp_stable : term_stable Topp_opp.
 prove_stable Topp_opp Zopp_involutive.
 Qed.
 
-Definition Topp_mult_r (t:term) :=
+Definition Topp_mult_r (t : term) :=
   match t with
   | Topp (Tmult x (Tint k)) => Tmult x (Tint (- k))
   | _ => t
@@ -974,7 +1167,7 @@ Theorem Topp_mult_r_stable : term_stable Topp_mult_r.
 prove_stable Topp_mult_r Zopp_mult_distr_r.
 Qed.
 
-Definition Topp_one (t:term) :=
+Definition Topp_one (t : term) :=
   match t with
   | Topp x => Tmult x (Tint (-1))
   | _ => t
@@ -985,7 +1178,7 @@ Theorem Topp_one_stable : term_stable Topp_one.
 prove_stable Topp_one Zopp_eq_mult_neg_1.
 Qed.
 
-Definition Tmult_plus_distr (t:term) :=
+Definition Tmult_plus_distr (t : term) :=
   match t with
   | Tmult (Tplus n m) p => Tplus (Tmult n p) (Tmult m p)
   | _ => t
@@ -996,7 +1189,7 @@ Theorem Tmult_plus_distr_stable : term_stable Tmult_plus_distr.
 prove_stable Tmult_plus_distr Zmult_plus_distr_l.
 Qed.
 
-Definition Tmult_opp_left (t:term) :=
+Definition Tmult_opp_left (t : term) :=
   match t with
   | Tmult (Topp x) (Tint y) => Tmult x (Tint (- y))
   | _ => t
@@ -1007,7 +1200,7 @@ Theorem Tmult_opp_left_stable : term_stable Tmult_opp_left.
 prove_stable Tmult_opp_left Zmult_opp_comm.
 Qed.
 
-Definition Tmult_assoc_reduced (t:term) :=
+Definition Tmult_assoc_reduced (t : term) :=
   match t with
   | Tmult (Tmult n (Tint m)) (Tint p) => Tmult n (Tint (m * p))
   | _ => t
@@ -1018,14 +1211,14 @@ Theorem Tmult_assoc_reduced_stable : term_stable Tmult_assoc_reduced.
 prove_stable Tmult_assoc_reduced Zmult_assoc_reverse.
 Qed.
 
-Definition Tred_factor0 (t:term) := Tmult t (Tint 1).
+Definition Tred_factor0 (t : term) := Tmult t (Tint 1).
 
 Theorem Tred_factor0_stable : term_stable Tred_factor0.
 
 prove_stable Tred_factor0 Zred_factor0.
 Qed.
 
-Definition Tred_factor1 (t:term) :=
+Definition Tred_factor1 (t : term) :=
   match t with
   | Tplus x y =>
       match eq_term x y with
@@ -1040,7 +1233,7 @@ Theorem Tred_factor1_stable : term_stable Tred_factor1.
 prove_stable Tred_factor1 Zred_factor1.
 Qed.
 
-Definition Tred_factor2 (t:term) :=
+Definition Tred_factor2 (t : term) :=
   match t with
   | Tplus x (Tmult y (Tint k)) =>
       match eq_term x y with
@@ -1050,8 +1243,8 @@ Definition Tred_factor2 (t:term) :=
   | _ => t
   end.
 
-(* Attention : il faut rendre opaque [Zplus] pour éviter que la tactique
-   de simplification n'aille trop loin et défasse [Zplus 1 k] *)
+(* Attention : il faut rendre opaque [Zplus] pour éviter que la tactique
+   de simplification n'aille trop loin et défasse [Zplus 1 k] *)
 
 Opaque Zplus.
 
@@ -1059,7 +1252,7 @@ Theorem Tred_factor2_stable : term_stable Tred_factor2.
 prove_stable Tred_factor2 Zred_factor2.
 Qed.
 
-Definition Tred_factor3 (t:term) :=
+Definition Tred_factor3 (t : term) :=
   match t with
   | Tplus (Tmult x (Tint k)) y =>
       match eq_term x y with
@@ -1075,7 +1268,7 @@ prove_stable Tred_factor3 Zred_factor3.
 Qed.
 
 
-Definition Tred_factor4 (t:term) :=
+Definition Tred_factor4 (t : term) :=
   match t with
   | Tplus (Tmult x (Tint k1)) (Tmult y (Tint k2)) =>
       match eq_term x y with
@@ -1090,7 +1283,7 @@ Theorem Tred_factor4_stable : term_stable Tred_factor4.
 prove_stable Tred_factor4 Zred_factor4.
 Qed.
 
-Definition Tred_factor6 (t:term) := Tplus t (Tint 0).
+Definition Tred_factor6 (t : term) := Tplus t (Tint 0).
 
 Theorem Tred_factor6_stable : term_stable Tred_factor6.
 
@@ -1099,7 +1292,7 @@ Qed.
 
 Transparent Zplus.
 
-Definition Tminus_def (t:term) :=
+Definition Tminus_def (t : term) :=
   match t with
   | Tminus x y => Tplus x (Topp y)
   | _ => t
@@ -1107,18 +1300,18 @@ Definition Tminus_def (t:term) :=
 
 Theorem Tminus_def_stable : term_stable Tminus_def.
 
-(* Le théorème ne sert à rien. Le but est prouvé avant. *)
+(* Le théorème ne sert à rien. Le but est prouvé avant. *)
 prove_stable Tminus_def False.
 Qed.
 
-(* \subsection{Fonctions de réécriture complexes} *)
+(* \subsection{Fonctions de réécriture complexes} *)
 
-(* \subsubsection{Fonction de réduction} *)
-(* Cette fonction réduit un terme dont la forme normale est un entier. Il
-   suffit pour cela d'échanger le constructeur [Tint] avec les opérateurs
-   réifiés. La réduction est ``gratuite''.  *)
+(* \subsubsection{Fonction de réduction} *)
+(* Cette fonction réduit un terme dont la forme normale est un entier. Il
+   suffit pour cela d'échanger le constructeur [Tint] avec les opérateurs
+   réifiés. La réduction est ``gratuite''.  *)
 
-Fixpoint reduce (t:term) : term :=
+Fixpoint reduce (t : term) : term :=
   match t with
   | Tplus x y =>
       match reduce x with
@@ -1171,13 +1364,13 @@ unfold term_stable in |- *; intros e t; elim t; auto;
 Qed.
 
 (* \subsubsection{Fusions}
-    \paragraph{Fusion de deux équations} *)
-(* On donne une somme de deux équations qui sont supposées normalisées. 
+    \paragraph{Fusion de deux équations} *)
+(* 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]. *)
+   le terme en une équation normalisée. C'est une version très simplifiée
+   du moteur de réécriture [rewrite]. *)
 
-Fixpoint fusion (trace:list t_fusion) (t:term) {struct trace} : term :=
+Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term :=
   match trace with
   | nil => reduce t
   | step :: trace' =>
@@ -1189,11 +1382,11 @@ Fixpoint fusion (trace:list t_fusion) (t:term) {struct trace} : term :=
       end
   end.
     
-Theorem fusion_stable : forall t:list t_fusion, term_stable (fusion t).
+Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t).
 
 simple induction t; simpl in |- *;
  [ exact reduce_stable
- | intros step l H; case step;
+ | intros stp l H; case stp;
     [ apply compose_term_stable;
        [ apply apply_right_stable; assumption | exact T_OMEGA10_stable ]
     | unfold term_stable in |- *; intros e t1; rewrite T_OMEGA10_stable;
@@ -1205,9 +1398,9 @@ simple induction t; simpl in |- *;
 
 Qed.
 
-(* \paragraph{Fusion de deux équations dont une sans coefficient} *)
+(* \paragraph{Fusion de deux équations dont une sans coefficient} *)
 
-Definition fusion_right (trace:list t_fusion) (t:term) : term :=
+Definition fusion_right (trace : list t_fusion) (t : term) : term :=
   match trace with
   | nil => reduce t (* Il faut mettre un compute *)
   | step :: trace' =>
@@ -1220,32 +1413,32 @@ Definition fusion_right (trace:list t_fusion) (t:term) : term :=
   end.
 
 (* \paragraph{Fusion avec anihilation} *)
-(* Normalement le résultat est une constante *)
+(* Normalement le résultat est une constante *)
 
-Fixpoint fusion_cancel (trace:nat) (t:term) {struct trace} : term :=
+Fixpoint fusion_cancel (trace : nat) (t : term) {struct trace} : term :=
   match trace with
   | O => reduce t
   | S trace' => fusion_cancel trace' (T_OMEGA13 t)
   end.
 
-Theorem fusion_cancel_stable : forall t:nat, term_stable (fusion_cancel t).
+Theorem fusion_cancel_stable : forall t : nat, term_stable (fusion_cancel t).
 
 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. 
 
-(* \subsubsection{Opérations afines sur une équation} *)
+(* \subsubsection{Opérations afines sur une équation} *)
 (* \paragraph{Multiplication scalaire et somme d'une constante} *)
 
-Fixpoint scalar_norm_add (trace:nat) (t:term) {struct trace} : term :=
+Fixpoint scalar_norm_add (trace : nat) (t : term) {struct trace} : term :=
   match trace with
   | O => reduce t
   | S trace' => apply_right (scalar_norm_add trace') (T_OMEGA11 t)
   end.
 
 Theorem scalar_norm_add_stable :
- forall t:nat, term_stable (scalar_norm_add t).
+ forall t : nat, term_stable (scalar_norm_add t).
 
 unfold term_stable, scalar_norm_add in |- *; intros trace; elim trace;
  [ exact reduce_stable
@@ -1254,13 +1447,13 @@ unfold term_stable, scalar_norm_add in |- *; intros trace; elim trace;
 Qed.
    
 (* \paragraph{Multiplication scalaire} *)
-Fixpoint scalar_norm (trace:nat) (t:term) {struct trace} : term :=
+Fixpoint scalar_norm (trace : nat) (t : term) {struct trace} : term :=
   match trace with
   | O => reduce t
   | S trace' => apply_right (scalar_norm trace') (T_OMEGA16 t)
   end.
 
-Theorem scalar_norm_stable : forall t:nat, term_stable (scalar_norm t).
+Theorem scalar_norm_stable : forall t : nat, term_stable (scalar_norm t).
 
 unfold term_stable, scalar_norm in |- *; intros trace; elim trace;
  [ exact reduce_stable
@@ -1269,13 +1462,13 @@ unfold term_stable, scalar_norm in |- *; intros trace; elim trace;
 Qed.
 
 (* \paragraph{Somme d'une constante} *)
-Fixpoint add_norm (trace:nat) (t:term) {struct trace} : term :=
+Fixpoint add_norm (trace : nat) (t : term) {struct trace} : term :=
   match trace with
   | O => reduce t
   | S trace' => apply_right (add_norm trace') (Tplus_assoc_r t)
   end.
 
-Theorem add_norm_stable : forall t:nat, term_stable (add_norm t).
+Theorem add_norm_stable : forall t : nat, term_stable (add_norm t).
 
 unfold term_stable, add_norm in |- *; intros trace; elim trace;
  [ exact reduce_stable
@@ -1283,44 +1476,16 @@ unfold term_stable, add_norm in |- *; intros trace; elim trace;
     [ exact (Tplus_assoc_r_stable e t) | exact H ] ].
 Qed.
 
-(* \subsection{La fonction de normalisation des termes (moteur de réécriture)} *)
+(* \subsection{La fonction de normalisation des termes (moteur de réécriture)} *)
 
-Inductive step : Set :=
-  | C_DO_BOTH : step -> step -> step
-  | C_LEFT : step -> step
-  | C_RIGHT : step -> step
-  | C_SEQ : step -> step -> step
-  | C_NOP : step
-  | C_OPP_PLUS : step
-  | C_OPP_OPP : step
-  | C_OPP_MULT_R : step
-  | C_OPP_ONE : step
-  | C_REDUCE : step
-  | C_MULT_PLUS_DISTR : step
-  | C_MULT_OPP_LEFT : step
-  | C_MULT_ASSOC_R : step
-  | C_PLUS_ASSOC_R : step
-  | C_PLUS_ASSOC_L : step
-  | C_PLUS_PERMUTE : step
-  | C_PLUS_SYM : step
-  | C_RED0 : step
-  | C_RED1 : step
-  | C_RED2 : step
-  | C_RED3 : step
-  | C_RED4 : step
-  | C_RED5 : step
-  | C_RED6 : step
-  | C_MULT_ASSOC_REDUCED : step
-  | C_MINUS : step
-  | C_MULT_SYM : step.
 
-Fixpoint rewrite (s:step) : term -> term :=
+Fixpoint rewrite (s : step) : term -> term :=
   match s with
   | C_DO_BOTH s1 s2 => apply_both (rewrite s1) (rewrite s2)
   | C_LEFT s => apply_left (rewrite s)
   | C_RIGHT s => apply_right (rewrite s)
-  | C_SEQ s1 s2 => fun t:term => rewrite s2 (rewrite s1 t)
-  | C_NOP => fun t:term => t
+  | C_SEQ s1 s2 => fun t : term => rewrite s2 (rewrite s1 t)
+  | C_NOP => fun t : term => t
   | C_OPP_PLUS => Topp_plus
   | C_OPP_OPP => Topp_opp
   | C_OPP_MULT_R => Topp_mult_r
@@ -1345,7 +1510,7 @@ Fixpoint rewrite (s:step) : term -> term :=
   | C_MULT_SYM => Tmult_sym
   end.
 
-Theorem rewrite_stable : forall s:step, term_stable (rewrite s).
+Theorem rewrite_stable : forall s : step, term_stable (rewrite s).
 
 simple induction s; simpl in |- *;
  [ intros; apply apply_both_stable; auto
@@ -1377,12 +1542,12 @@ simple induction s; simpl in |- *;
  | exact Tmult_sym_stable ].
 Qed.
 
-(* \subsection{tactiques de résolution d'un but omega normalisé} 
-   Trace de la procédure 
-\subsubsection{Tactiques générant une contradiction}
+(* \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]} *)
 
-Definition constant_not_nul (i:nat) (h:hyps) :=
+Definition constant_not_nul (i : nat) (h : list proposition) :=
   match nth_hyps i h with
   | EqTerm (Tint Z0) (Tint n) =>
       match eq_Z n 0 with
@@ -1393,33 +1558,33 @@ Definition constant_not_nul (i:nat) (h:hyps) :=
   end.
 
 Theorem constant_not_nul_valid :
- forall i:nat, valid_hyps (constant_not_nul i).
+ forall i : nat, valid_hyps (constant_not_nul i).
 
 unfold valid_hyps, constant_not_nul in |- *; intros;
- generalize (nth_valid e i lp); Simplify; simpl in |- *; 
- elim_eq_Z z0 0%Z; auto; simpl in |- *; intros H1 H2; 
+ generalize (nth_valid ep e i lp); Simplify; simpl in |- *;
+ elim_eq_Z ipattern:z0 0%Z; auto; simpl in |- *; intros H1 H2; 
  elim H1; symmetry  in |- *; auto.
 Qed.   
 
 (* \paragraph{[O_CONSTANT_NEG]} *)
 
-Definition constant_neg (i:nat) (h:hyps) :=
+Definition constant_neg (i : nat) (h : list proposition) :=
   match nth_hyps i h with
   | LeqTerm (Tint Z0) (Tint (Zneg n)) => absurd
   | _ => h
   end.
 
-Theorem constant_neg_valid : forall i:nat, valid_hyps (constant_neg i).
+Theorem constant_neg_valid : forall i : nat, valid_hyps (constant_neg i).
 
 unfold valid_hyps, constant_neg in |- *; intros;
- generalize (nth_valid e i lp); Simplify; simpl in |- *; 
+ generalize (nth_valid ep e i lp); Simplify; simpl in |- *;
  unfold Zle in |- *; simpl in |- *; intros H1; elim H1;
  [ assumption | trivial ].
 Qed.   
 
 (* \paragraph{[NOT_EXACT_DIVIDE]} *)
-Definition not_exact_divide (k1 k2:Z) (body:term) (t i:nat) 
-  (l:hyps) :=
+Definition not_exact_divide (k1 k2 : Z) (body : term) 
+  (t i : nat) (l : list proposition) :=
   match nth_hyps i l with
   | EqTerm (Tint Z0) b =>
       match
@@ -1441,11 +1606,11 @@ Definition not_exact_divide (k1 k2:Z) (body:term) (t i:nat)
   end.
 
 Theorem not_exact_divide_valid :
- forall (k1 k2:Z) (body:term) (t i:nat),
-   valid_hyps (not_exact_divide k1 k2 body t i).
+ forall (k1 k2 : Z) (body : term) (t i : nat),
+ valid_hyps (not_exact_divide k1 k2 body t i).
 
 unfold valid_hyps, not_exact_divide in |- *; intros;
- generalize (nth_valid e i lp); Simplify;
+ generalize (nth_valid ep e i lp); Simplify;
  elim_eq_term (scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) t1;
  auto; Simplify; intro H2; elim H2; simpl in |- *;
  elim (scalar_norm_add_stable t e); simpl in |- *; 
@@ -1456,7 +1621,7 @@ Qed.
 
 (* \paragraph{[O_CONTRADICTION]} *)
 
-Definition contradiction (t i j:nat) (l:hyps) :=
+Definition contradiction (t i j : nat) (l : list proposition) :=
   match nth_hyps i l with
   | LeqTerm (Tint Z0) b1 =>
       match nth_hyps j l with
@@ -1475,10 +1640,10 @@ Definition contradiction (t i j:nat) (l:hyps) :=
   end.
 
 Theorem contradiction_valid :
- forall t i j:nat, valid_hyps (contradiction t i j).
+ forall t i j : nat, valid_hyps (contradiction t i j).
 
-unfold valid_hyps, contradiction in |- *; intros t i j e l H;
- generalize (nth_valid _ i _ H); generalize (nth_valid _ j _ H);
+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; intros z; case z; auto; case (nth_hyps j l); 
  auto; intros t3 t4; case t3; auto; intros z'; case z'; 
@@ -1495,7 +1660,7 @@ Qed.
 
 (* \paragraph{[O_NEGATE_CONTRADICT]} *)
 
-Definition negate_contradict (i1 i2:nat) (h:hyps) :=
+Definition negate_contradict (i1 i2 : nat) (h : list proposition) :=
   match nth_hyps i1 h with
   | EqTerm (Tint Z0) b1 =>
       match nth_hyps i2 h with
@@ -1518,7 +1683,7 @@ Definition negate_contradict (i1 i2:nat) (h:hyps) :=
   | _ => h
   end.
 
-Definition negate_contradict_inv (t i1 i2:nat) (h:hyps) :=
+Definition negate_contradict_inv (t i1 i2 : nat) (h : list proposition) :=
   match nth_hyps i1 h with
   | EqTerm (Tint Z0) b1 =>
       match nth_hyps i2 h with
@@ -1541,12 +1706,11 @@ Definition negate_contradict_inv (t i1 i2:nat) (h:hyps) :=
   | _ => h
   end.
 
-
 Theorem negate_contradict_valid :
- forall i j:nat, valid_hyps (negate_contradict i j).
+ forall i j : nat, valid_hyps (negate_contradict i j).
 
-unfold valid_hyps, negate_contradict in |- *; intros i j e l H;
- generalize (nth_valid _ i _ H); generalize (nth_valid _ j _ H);
+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; case z; auto; case (nth_hyps j l); 
  auto; intros t3 t4; case t3; auto; intros z'; case z'; 
@@ -1559,11 +1723,11 @@ unfold valid_hyps, negate_contradict in |- *; intros i j e l H;
 Qed.
 
 Theorem negate_contradict_inv_valid :
- forall t i j:nat, valid_hyps (negate_contradict_inv t i j).
+ forall t i j : nat, valid_hyps (negate_contradict_inv t i j).
 
 
-unfold valid_hyps, negate_contradict_inv in |- *; intros t i j e l H;
- generalize (nth_valid _ i _ H); generalize (nth_valid _ j _ H);
+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; case z; auto; case (nth_hyps j l); 
  auto; intros t3 t4; case t3; auto; intros z'; case z'; 
@@ -1585,15 +1749,15 @@ unfold valid_hyps, negate_contradict_inv in |- *; intros t i j e l H;
 
 Qed.
 
-
-(* \subsubsection{Tactiques générant une nouvelle équation} *)
+(* \subsubsection{Tactiques générant une nouvelle équation} *)
 (* \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 
- généralisations des théorèmes utilisés par OMEGA. *)
+ 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 
+ généralisations des théorèmes utilisés par OMEGA. *)
 
-Definition sum (k1 k2:Z) (trace:list t_fusion) (prop1 prop2:proposition) :=
+Definition sum (k1 k2 : Z) (trace : list t_fusion)
+  (prop1 prop2 : proposition) :=
   match prop1 with
   | EqTerm (Tint Z0) b1 =>
       match prop2 with
@@ -1646,36 +1810,36 @@ Definition sum (k1 k2:Z) (trace:list t_fusion) (prop1 prop2:proposition) :=
   end.
 
 Theorem sum1 :
- forall a b c d:Z, 0%Z = a -> 0%Z = b -> 0%Z = (a * c + b * d)%Z.
+ forall a b c d : Z, 0%Z = a -> 0%Z = b -> 0%Z = (a * c + b * d)%Z.
 
 intros; elim H; elim H0; simpl in |- *; auto.
 Qed.
   
 Theorem sum2 :
- forall a b c d:Z,
-   (0 <= d)%Z -> 0%Z = a -> (0 <= b)%Z -> (0 <= a * c + b * d)%Z.
+ forall a b c d : Z,
+ (0 <= d)%Z -> 0%Z = a -> (0 <= b)%Z -> (0 <= a * c + b * d)%Z.
 
 intros; elim H0; simpl in |- *; generalize H H1; case b; case d;
  unfold Zle in |- *; simpl in |- *; auto.  
 Qed.
 
 Theorem sum3 :
- forall a b c d:Z,
-   (0 <= c)%Z ->
-   (0 <= d)%Z -> (0 <= a)%Z -> (0 <= b)%Z -> (0 <= a * c + b * d)%Z.
+ forall a b c d : Z,
+ (0 <= c)%Z ->
+ (0 <= d)%Z -> (0 <= a)%Z -> (0 <= b)%Z -> (0 <= a * c + b * d)%Z.
 
 intros a b c d; case a; case b; case c; case d; unfold Zle in |- *;
  simpl in |- *; auto. 
 Qed.
 
-Theorem sum4 : forall k:Z, (k ?= 0)%Z = Datatypes.Gt -> (0 <= k)%Z.
+Theorem sum4 : forall k : Z, (k ?= 0)%Z = Datatypes.Gt -> (0 <= k)%Z.
 
 intro; case k; unfold Zle in |- *; simpl in |- *; auto; intros; discriminate.  
 Qed.
 
 Theorem sum5 :
- forall a b c d:Z,
-   c <> 0%Z -> 0%Z <> a -> 0%Z = b -> 0%Z <> (a * c + b * d)%Z.
+ forall a b c d : Z,
+ c <> 0%Z -> 0%Z <> a -> 0%Z = b -> 0%Z <> (a * c + b * d)%Z.
 
 intros a b c d H1 H2 H3; elim H3; simpl in |- *; rewrite Zplus_comm;
  simpl in |- *; generalize H1 H2; case a; case c; simpl in |- *; 
@@ -1683,11 +1847,12 @@ intros a b c d H1 H2 H3; elim H3; simpl in |- *; rewrite Zplus_comm;
 Qed.
 
 
-Theorem sum_valid : forall (k1 k2:Z) (t:list t_fusion), valid2 (sum k1 k2 t).
+Theorem sum_valid :
+ forall (k1 k2 : Z) (t : list t_fusion), valid2 (sum k1 k2 t).
 
-unfold valid2 in |- *; intros k1 k2 t e p1 p2; unfold sum in |- *; Simplify;
- simpl in |- *; auto; try elim (fusion_stable t); simpl in |- *; 
- intros;
+unfold valid2 in |- *; intros k1 k2 t ep e p1 p2; unfold sum in |- *;
+ Simplify; simpl in |- *; auto; try elim (fusion_stable t); 
+ simpl in |- *; intros;
  [ apply sum1; assumption
  | apply sum2; try assumption; apply sum4; assumption
  | rewrite Zplus_comm; apply sum2; try assumption; apply sum4; assumption
@@ -1698,9 +1863,10 @@ unfold valid2 in |- *; intros k1 k2 t e p1 p2; unfold sum in |- *; Simplify;
 Qed.
 
 (* \paragraph{[O_EXACT_DIVIDE]}
-   c'est une oper1 valide mais on préfère une substitution a ce point la *)
+   c'est une oper1 valide mais on préfère une substitution a ce point la *)
 
-Definition exact_divide (k:Z) (body:term) (t:nat) (prop:proposition) :=
+Definition exact_divide (k : Z) (body : term) (t : nat)
+  (prop : proposition) :=
   match prop with
   | EqTerm (Tint Z0) b =>
       match eq_term (scalar_norm t (Tmult body (Tint k))) b with
@@ -1715,10 +1881,10 @@ Definition exact_divide (k:Z) (body:term) (t:nat) (prop:proposition) :=
   end.
 
 Theorem exact_divide_valid :
- forall (k:Z) (t:term) (n:nat), valid1 (exact_divide k t n).
+ forall (k : Z) (t : term) (n : nat), valid1 (exact_divide k t n).
 
 
-unfold valid1, exact_divide in |- *; intros k1 k2 t e p1; Simplify;
+unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; Simplify;
  simpl in |- *; auto; elim_eq_term (scalar_norm t (Tmult k2 (Tint k1))) t1;
  simpl in |- *; auto; elim_eq_Z k1 0%Z; simpl in |- *; 
  auto; intros H1 H2; elim H2; elim scalar_norm_stable; 
@@ -1734,11 +1900,11 @@ Qed.
 
 
 (* \paragraph{[O_DIV_APPROX]}
-  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. *)
+  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:Z) (body:term) 
-  (t:nat) (prop:proposition) :=
+Definition divide_and_approx (k1 k2 : Z) (body : term) 
+  (t : nat) (prop : proposition) :=
   match prop with
   | LeqTerm (Tint Z0) b =>
       match
@@ -1760,10 +1926,11 @@ Definition divide_and_approx (k1 k2:Z) (body:term)
   end.
 
 Theorem divide_and_approx_valid :
- forall (k1 k2:Z) (body:term) (t:nat),
-   valid1 (divide_and_approx k1 k2 body t).
+ forall (k1 k2 : Z) (body : term) (t : nat),
+ valid1 (divide_and_approx k1 k2 body t).
 
-unfold valid1, divide_and_approx in |- *; intros k1 k2 body t e p1; Simplify;
+unfold valid1, divide_and_approx in |- *; intros k1 k2 body t ep e p1;
+ Simplify;
  elim_eq_term (scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) t1;
  Simplify; auto; intro E; elim E; simpl in |- *;
  elim (scalar_norm_add_stable t e); simpl in |- *; 
@@ -1772,7 +1939,7 @@ Qed.
 
 (* \paragraph{[MERGE_EQ]} *)
 
-Definition merge_eq (t:nat) (prop1 prop2:proposition) :=
+Definition merge_eq (t : nat) (prop1 prop2 : proposition) :=
   match prop1 with
   | LeqTerm (Tint Z0) b1 =>
       match prop2 with
@@ -1786,9 +1953,9 @@ Definition merge_eq (t:nat) (prop1 prop2:proposition) :=
   | _ => TrueTerm
   end.
 
-Theorem merge_eq_valid : forall n:nat, valid2 (merge_eq n).
+Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n).
 
-unfold valid2, merge_eq in |- *; intros n e p1 p2; Simplify; simpl in |- *;
+unfold valid2, merge_eq in |- *; intros n ep e p1 p2; Simplify; simpl in |- *;
  auto; elim (scalar_norm_stable n e); simpl in |- *; 
  intros; symmetry  in |- *; apply OMEGA8 with (2 := H0);
  [ assumption | elim Zopp_eq_mult_neg_1; trivial ].
@@ -1798,23 +1965,23 @@ Qed.
 
 (* \paragraph{[O_CONSTANT_NUL]} *)
 
-Definition constant_nul (i:nat) (h:hyps) :=
+Definition constant_nul (i : nat) (h : list proposition) :=
   match nth_hyps i h with
   | NeqTerm (Tint Z0) (Tint Z0) => absurd
   | _ => h
   end.
 
-Theorem constant_nul_valid : forall i:nat, valid_hyps (constant_nul i).
+Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i).
 
 unfold valid_hyps, constant_nul in |- *; intros;
- generalize (nth_valid e i lp); Simplify; simpl in |- *; 
+ generalize (nth_valid ep e i lp); Simplify; simpl in |- *;
  unfold Zne in |- *; intro H1; absurd (0%Z = 0%Z); 
  auto.
 Qed.
 
 (* \paragraph{[O_STATE]} *)
 
-Definition state (m:Z) (s:step) (prop1 prop2:proposition) :=
+Definition state (m : Z) (s : step) (prop1 prop2 : proposition) :=
   match prop1 with
   | EqTerm (Tint Z0) b1 =>
       match prop2 with
@@ -1826,9 +1993,9 @@ Definition state (m:Z) (s:step) (prop1 prop2:proposition) :=
   | _ => TrueTerm
   end.
 
-Theorem state_valid : forall (m:Z) (s:step), valid2 (state m s).
+Theorem state_valid : forall (m : Z) (s : step), valid2 (state m s).
 
-unfold valid2 in |- *; intros m s e p1 p2; unfold state in |- *; Simplify;
+unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify;
  simpl in |- *; auto; elim (rewrite_stable s e); simpl in |- *; 
  intros H1 H2; elim H1;
  rewrite (Zplus_comm (- interp_term e t5) (interp_term e t3)); 
@@ -1836,12 +2003,13 @@ unfold valid2 in |- *; intros m s e p1 p2; unfold state in |- *; Simplify;
 
 Qed.
 
-(* \subsubsection{Tactiques générant plusieurs but}
+(* \subsubsection{Tactiques générant plusieurs but}
    \paragraph{[O_SPLIT_INEQ]} 
-   La seule pour le moment (tant que la normalisation n'est pas réfléchie). *)
+   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) 
-  (l:hyps) :=
+Definition split_ineq (i t : nat)
+  (f1 f2 : list proposition -> list (list proposition))
+  (l : list proposition) :=
   match nth_hyps i l with
   | NeqTerm (Tint Z0) b1 =>
       f1 (LeqTerm (Tint 0) (add_norm t (Tplus b1 (Tint (-1)))) :: l) ++
@@ -1853,12 +2021,12 @@ Definition split_ineq (i t:nat) (f1 f2:hyps -> lhyps)
   end.
 
 Theorem split_ineq_valid :
- forall (i t:nat) (f1 f2:hyps -> lhyps),
-   valid_list_hyps f1 ->
-   valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2).
+ forall (i t : nat) (f1 f2 : list proposition -> list (list proposition)),
+ valid_list_hyps f1 ->
+ valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2).
 
-unfold valid_list_hyps, split_ineq in |- *; intros i t f1 f2 H1 H2 e lp H;
- generalize (nth_valid _ i _ H); case (nth_hyps i lp); 
+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 |- *; 
  auto; intros z; case z; simpl in |- *; auto; intro H3; 
  apply append_valid; elim (OMEGA19 (interp_term e t2));
@@ -1872,112 +2040,91 @@ Qed.
 
 
 (* \subsection{La fonction de rejeu de la trace} *)
-Inductive t_omega : Set :=
-  | O_CONSTANT_NOT_NUL : 
-      (* n = 0 n!= 0 *)
-      nat -> t_omega
-  | O_CONSTANT_NEG :
-      nat -> t_omega
-      (* division et approximation d'une équation *)
-  | O_DIV_APPROX :
-      Z ->
-      Z ->
-      term ->
-      nat ->
-      t_omega ->
-      nat -> t_omega
-      (* pas de solution car pas de division exacte (fin) *)
-  | O_NOT_EXACT_DIVIDE :
-      Z -> Z -> term -> nat -> nat -> t_omega
-                               (* division exacte *)
-  | O_EXACT_DIVIDE : Z -> term -> nat -> t_omega -> nat -> t_omega
-  | O_SUM : Z -> nat -> Z -> nat -> list t_fusion -> t_omega -> t_omega
-  | O_CONTRADICTION : nat -> nat -> nat -> t_omega
-  | O_MERGE_EQ : nat -> nat -> nat -> t_omega -> t_omega
-  | O_SPLIT_INEQ : nat -> nat -> t_omega -> t_omega -> t_omega
-  | O_CONSTANT_NUL : nat -> t_omega
-  | O_NEGATE_CONTRADICT : nat -> nat -> t_omega
-  | O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega
-  | O_STATE : Z -> step -> nat -> nat -> t_omega -> t_omega.
-
-Notation singleton := (fun a:hyps => a :: nil).
 
-Fixpoint execute_omega (t:t_omega) (l:hyps) {struct t} : lhyps :=
+Fixpoint execute_omega (t : t_omega) (l : list proposition) {struct t} :
+ list (list proposition) :=
   match t with
-  | O_CONSTANT_NOT_NUL n => singleton (constant_not_nul n l)
-  | O_CONSTANT_NEG n => singleton (constant_neg n l)
+  | O_CONSTANT_NOT_NUL n =>
+      (fun a : list proposition => a :: nil) (constant_not_nul n l)
+  | O_CONSTANT_NEG n =>
+      (fun a : list proposition => a :: nil) (constant_neg n l)
   | O_DIV_APPROX k1 k2 body t cont n =>
       execute_omega cont (apply_oper_1 n (divide_and_approx k1 k2 body t) l)
   | O_NOT_EXACT_DIVIDE k1 k2 body t i =>
-      singleton (not_exact_divide k1 k2 body t i l)
+      (fun a : list proposition => a :: nil)
+        (not_exact_divide k1 k2 body t i l)
   | O_EXACT_DIVIDE k body t cont n =>
       execute_omega cont (apply_oper_1 n (exact_divide k body t) l)
   | O_SUM k1 i1 k2 i2 t cont =>
       execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2 t) l)
-  | O_CONTRADICTION t i j => singleton (contradiction t i j l)
+  | O_CONTRADICTION t i j =>
+      (fun a : list proposition => a :: nil) (contradiction t i j l)
   | O_MERGE_EQ t i1 i2 cont =>
       execute_omega cont (apply_oper_2 i1 i2 (merge_eq t) l)
   | O_SPLIT_INEQ t i cont1 cont2 =>
       split_ineq i t (execute_omega cont1) (execute_omega cont2) l
-  | O_CONSTANT_NUL i => singleton (constant_nul i l)
-  | O_NEGATE_CONTRADICT i j => singleton (negate_contradict i j l)
+  | O_CONSTANT_NUL i =>
+      (fun a : list proposition => a :: nil) (constant_nul i l)
+  | O_NEGATE_CONTRADICT i j =>
+      (fun a : list proposition => a :: nil) (negate_contradict i j l)
   | O_NEGATE_CONTRADICT_INV t i j =>
-      singleton (negate_contradict_inv t i j l)
+      (fun a : list proposition => a :: nil) (negate_contradict_inv t i j l)
   | O_STATE m s i1 i2 cont =>
       execute_omega cont (apply_oper_2 i1 i2 (state m s) l)
   end.
 
-Theorem omega_valid : forall t:t_omega, valid_list_hyps (execute_omega t).
+Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t).
 
 simple induction t; simpl in |- *;
  [ unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
-    apply (constant_not_nul_valid n e lp H)
+    apply (constant_not_nul_valid n ep e lp H)
  | unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
-    apply (constant_neg_valid n e lp H)
+    apply (constant_neg_valid n ep e lp H)
  | unfold valid_list_hyps, valid_hyps in |- *;
-    intros k1 k2 body n t' Ht' m e lp H; apply Ht';
+    intros k1 k2 body n t' Ht' m ep e lp H; apply Ht';
     apply
      (apply_oper_1_valid m (divide_and_approx k1 k2 body n)
-        (divide_and_approx_valid k1 k2 body n) e lp H)
+        (divide_and_approx_valid k1 k2 body n) ep e lp H)
  | unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
-    apply (not_exact_divide_valid z z0 t0 n n0 e lp H)
+    apply (not_exact_divide_valid z z0 t0 n n0 ep e lp H)
  | unfold valid_list_hyps, valid_hyps in |- *;
-    intros k body n t' Ht' m e lp H; apply Ht';
+    intros k body n t' Ht' m ep e lp H; apply Ht';
     apply
      (apply_oper_1_valid m (exact_divide k body n)
-        (exact_divide_valid k body n) e lp H)
+        (exact_divide_valid k body n) ep e lp H)
  | unfold valid_list_hyps, valid_hyps in |- *;
-    intros k1 i1 k2 i2 trace t' Ht' e lp H; apply Ht';
+    intros k1 i1 k2 i2 trace t' Ht' ep e lp H; apply Ht';
     apply
-     (apply_oper_2_valid i1 i2 (sum k1 k2 trace) (sum_valid k1 k2 trace) e lp
-        H)
+     (apply_oper_2_valid i1 i2 (sum k1 k2 trace) (sum_valid k1 k2 trace) ep e
+        lp H)
  | unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
-    apply (contradiction_valid n n0 n1 e lp H)
+    apply (contradiction_valid n n0 n1 ep e lp H)
  | unfold valid_list_hyps, valid_hyps in |- *;
-    intros trace i1 i2 t' Ht' e lp H; apply Ht';
+    intros trace i1 i2 t' Ht' ep e lp H; apply Ht';
     apply
-     (apply_oper_2_valid i1 i2 (merge_eq trace) (merge_eq_valid trace) e lp H)
+     (apply_oper_2_valid i1 i2 (merge_eq trace) (merge_eq_valid trace) ep e
+        lp H)
  | intros t' i k1 H1 k2 H2; unfold valid_list_hyps in |- *; simpl in |- *;
-    intros e lp H;
+    intros ep e lp H;
     apply
-     (split_ineq_valid i t' (execute_omega k1) (execute_omega k2) H1 H2 e lp
-        H)
- | unfold valid_list_hyps in |- *; simpl in |- *; intros i e lp H; left;
-    apply (constant_nul_valid i e lp H)
- | unfold valid_list_hyps in |- *; simpl in |- *; intros i j e lp H; left;
-    apply (negate_contradict_valid i j e lp H)
- | unfold valid_list_hyps in |- *; simpl in |- *; intros n i j e lp H; left;
-    apply (negate_contradict_inv_valid n i j e lp H)
- | unfold valid_list_hyps, valid_hyps in |- *; intros m s i1 i2 t' Ht' e lp H;
-    apply Ht';
-    apply (apply_oper_2_valid i1 i2 (state m s) (state_valid m s) e lp H) ].
+     (split_ineq_valid i t' (execute_omega k1) (execute_omega k2) H1 H2 ep e
+        lp H)
+ | unfold valid_list_hyps in |- *; simpl in |- *; intros i ep e lp H; left;
+    apply (constant_nul_valid i ep e lp H)
+ | unfold valid_list_hyps in |- *; simpl in |- *; intros i j ep e lp H; left;
+    apply (negate_contradict_valid i j ep e lp H)
+ | unfold valid_list_hyps in |- *; simpl in |- *; intros n i j ep e lp H;
+    left; apply (negate_contradict_inv_valid n i j ep e lp H)
+ | unfold valid_list_hyps, valid_hyps in |- *;
+    intros m s i1 i2 t' Ht' ep e lp H; apply Ht';
+    apply (apply_oper_2_valid i1 i2 (state m s) (state_valid m s) ep e lp H) ].
 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) :=
+Definition move_right (s : step) (p : proposition) :=
   match p with
   | EqTerm t1 t2 => EqTerm (Tint 0) (rewrite s (Tplus t1 (Topp t2)))
   | LeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (Tplus t2 (Topp t1)))
@@ -1990,15 +2137,15 @@ Definition move_right (s:step) (p:proposition) :=
   | p => p
   end.
 
-Theorem Zne_left_2 : forall x y:Z, Zne x y -> Zne 0 (x + - y).
+Theorem Zne_left_2 : forall x y : Z, Zne x y -> Zne 0 (x + - y).
 unfold Zne, not in |- *; intros x y H1 H2; apply H1;
  apply (Zplus_reg_l (- y)); rewrite Zplus_comm; elim H2; 
  rewrite Zplus_opp_l; trivial.
 Qed.
 
-Theorem move_right_valid : forall s:step, valid1 (move_right s).
+Theorem move_right_valid : forall s : step, valid1 (move_right s).
 
-unfold valid1, move_right in |- *; intros s e p; Simplify; simpl in |- *;
+unfold valid1, move_right in |- *; intros s ep e p; Simplify; simpl in |- *;
  elim (rewrite_stable s e); simpl in |- *;
  [ symmetry  in |- *; apply Zegal_left; assumption
  | intro; apply Zle_left; assumption
@@ -2008,56 +2155,633 @@ unfold valid1, move_right in |- *; intros s e p; Simplify; simpl in |- *;
  | intro; apply Zne_left_2; assumption ].
 Qed.
 
-Definition do_normalize (i:nat) (s:step) := apply_oper_1 i (move_right s).
+Definition do_normalize (i : nat) (s : step) := apply_oper_1 i (move_right s).
 
 Theorem do_normalize_valid :
- forall (i:nat) (s:step), valid_hyps (do_normalize i s).
+ forall (i : nat) (s : step), valid_hyps (do_normalize i s).
 
 intros; unfold do_normalize in |- *; apply apply_oper_1_valid;
  apply move_right_valid.
 Qed.
 
-Fixpoint do_normalize_list (l:list step) (i:nat) (h:hyps) {struct l} :
- hyps :=
+Fixpoint do_normalize_list (l : list step) (i : nat) 
+ (h : list proposition) {struct l} : list proposition :=
   match l with
   | s :: l' => do_normalize_list l' (S i) (do_normalize i s h)
   | nil => h
   end.
 
 Theorem do_normalize_list_valid :
- forall (l:list step) (i:nat), valid_hyps (do_normalize_list l i).
+ forall (l : list step) (i : nat), valid_hyps (do_normalize_list l i).
 
 simple induction l; simpl in |- *; unfold valid_hyps in |- *;
  [ auto
- | intros a l' Hl' i e lp H; unfold valid_hyps in Hl'; apply Hl';
-    apply (do_normalize_valid i a e lp); assumption ].
+ | intros a l' Hl' i ep e lp H; unfold valid_hyps in Hl'; apply Hl';
+    apply (do_normalize_valid i a ep e lp); assumption ].
 Qed.
 
 Theorem normalize_goal :
- forall (s:list step) (env:list Z) (l:hyps),
-   interp_goal env (do_normalize_list s 0 l) -> interp_goal env l.
+ forall (s : list step) (ep : PropList) (env : list Z) (l : list proposition),
+ (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+  interp_goal_concl envp env FalseTerm l) ep env (do_normalize_list s 0 l) ->
+ (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+  interp_goal_concl envp env FalseTerm l) ep env l.
 
 intros; apply valid_goal with (2 := H); apply do_normalize_list_valid.
 Qed.
 
-(* \subsubsection{Exécution de la trace} *)
+(* \subsubsection{Exécution de la trace} *)
 
 Theorem execute_goal :
- forall (t:t_omega) (env:list Z) (l:hyps),
-   interp_list_goal env (execute_omega t l) -> interp_goal env l.
+ forall (t : t_omega) (ep : PropList) (env : list Z) (l : list proposition),
+ interp_list_goal ep env (execute_omega t l) ->
+ (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+  interp_goal_concl envp env FalseTerm l) ep env l.
 
-intros; apply (goal_valid (execute_omega t) (omega_valid t) env l H).
+intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H).
 Qed.
 
 
 Theorem append_goal :
- forall (e:list Z) (l1 l2:lhyps),
-   interp_list_goal e l1 /\ interp_list_goal e l2 ->
-   interp_list_goal e (l1 ++ l2).
+ forall (ep : PropList) (e : list Z) (l1 l2 : list (list proposition)),
+ interp_list_goal ep e l1 /\ interp_list_goal ep e l2 ->
+ interp_list_goal ep e (l1 ++ l2).
 
-intros e; simple induction l1;
- [ simpl in |- *; intros l2 [H1 H2]; assumption
- | simpl in |- *; intros h1 t1 HR l2 [[H1 H2] H3]; split; auto ].
+intros ep e; simple induction l1;
+ [ simpl in |- *; intros l2 (H1, H2); assumption
+ | simpl in |- *; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ].
 
+Qed.
+
+Require Import Decidable.
+
+(* A simple decidability checker : if the proposition belongs to the
+   simple grammar describe below then it is decidable. Proof is by 
+   induction and uses well known theorem about arithmetic and propositional
+   calculus *)
+
+Fixpoint decidability (p : proposition) : bool :=
+  match p with
+  | EqTerm _ _ => true
+  | LeqTerm _ _ => true
+  | GeqTerm _ _ => true
+  | GtTerm _ _ => true
+  | LtTerm _ _ => true
+  | NeqTerm _ _ => true
+  | FalseTerm => true
+  | TrueTerm => true
+  | Tnot t => decidability t
+  | Tand t1 t2 => decidability t1 && decidability t2
+  | Timp t1 t2 => decidability t1 && decidability t2
+  | Tor t1 t2 => decidability t1 && decidability t2
+  | Tprop _ => false
+  end.
+
+Theorem decidable_correct :
+ forall (ep : PropList) (e : list Z) (p : proposition),
+ decidability p = true -> decidable (interp_proposition ep e p).
+
+simple induction p; simpl in |- *; intros;
+ [ apply dec_eq
+ | apply dec_Zle
+ | left; auto
+ | right; unfold not in |- *; auto
+ | apply dec_not; auto
+ | apply dec_Zge
+ | apply dec_Zgt
+ | apply dec_Zlt
+ | apply dec_Zne
+ | apply dec_or; elim andb_prop with (1 := H1); auto
+ | apply dec_and; elim andb_prop with (1 := H1); auto
+ | apply dec_imp; elim andb_prop with (1 := H1); auto
+ | discriminate H ].
+
+Qed.
+
+(* An interpretation function for a complete goal with an explicit
+   conclusion. We use an intermediate fixpoint. *)
+
+Fixpoint interp_full_goal (envp : PropList) (env : list Z) 
+ (c : proposition) (l : list proposition) {struct l} : Prop :=
+  match l with
+  | nil => interp_proposition envp env c
+  | p' :: l' =>
+      interp_proposition envp env p' -> interp_full_goal envp env c l'
+  end.
+
+Definition interp_full (ep : PropList) (e : list Z)
+  (lc : list proposition * proposition) : Prop :=
+  match lc with
+  | (l, c) => interp_full_goal ep e c l
+  end.
+
+(* Relates the interpretation of a complete goal with the interpretation
+   of its hypothesis and conclusion *)
+
+Theorem interp_full_false :
+ forall (ep : PropList) (e : list Z) (l : list proposition) (c : proposition),
+ (interp_hyps ep e l -> interp_proposition ep e c) -> interp_full ep e (l, c).
+
+simple induction l; unfold interp_full in |- *; simpl in |- *;
+ [ auto | intros a l1 H1 c H2 H3; apply H1; auto ].
+
+Qed.
+
+(* Push the conclusion in the list of hypothesis using a double negation
+   If the decidability cannot be "proven", then just forget about the 
+   conclusion (equivalent of replacing it with false) *)
+
+Definition to_contradict (lc : list proposition * proposition) :=
+  match lc with
+  | (l, c) => if decidability c then Tnot c :: l else l
+  end.
+
+(* The previous operation is valid in the sense that the new list of
+   hypothesis implies the original goal *)
+
+Theorem to_contradict_valid :
+ forall (ep : PropList) (e : list Z) (lc : list proposition * proposition),
+ (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+  interp_goal_concl envp env FalseTerm l) ep e (to_contradict lc) ->
+ interp_full ep e lc.
+
+intros ep e lc; case lc; intros l c; simpl in |- *;
+ pattern (decidability c) in |- *; apply bool_ind2;
+ [ simpl in |- *; intros H H1; apply interp_full_false; intros H2;
+    apply not_not;
+    [ apply decidable_correct; assumption
+    | unfold not at 1 in |- *; intro H3; apply hyps_to_goal with (2 := H2);
+       auto ]
+ | intros H1 H2; apply interp_full_false; intro H3;
+    elim hyps_to_goal with (1 := H2); assumption ].
+Qed.
+
+(* [map_cons x l] adds [x] at the head of each list in [l] (which is a list
+   of lists *)
+
+Fixpoint map_cons (A : Set) (x : A) (l : list (list A)) {struct l} :
+ list (list A) :=
+  match l with
+  | nil => nil
+  | l :: ll => (x :: l) :: map_cons A x ll
+  end.
+
+(* 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. 
+   Note that :
+	- we need a way to drive the analysis as some hypotheis may not
+          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 : list proposition) {struct nn} :
+ list (list proposition) :=
+  match nn with
+  | O => ll :: nil
+  | S n =>
+      match ll with
+      | nil => nil :: nil
+      | Tor p1 p2 :: l =>
+          destructure_hyps n (p1 :: l) ++ destructure_hyps n (p2 :: l)
+      | Tand p1 p2 :: l => destructure_hyps n (p1 :: p2 :: l)
+      | Timp p1 p2 :: l =>
+          if decidability p1
+          then
+           destructure_hyps n (Tnot p1 :: l) ++ destructure_hyps n (p2 :: l)
+          else map_cons _ (Timp p1 p2) (destructure_hyps n l)
+      | Tnot p :: l =>
+          match p with
+          | Tnot p1 =>
+              if decidability p1
+              then destructure_hyps n (p1 :: l)
+              else map_cons _ (Tnot (Tnot p1)) (destructure_hyps n l)
+          | Tor p1 p2 => destructure_hyps n (Tnot p1 :: Tnot p2 :: l)
+          | Tand p1 p2 =>
+              if decidability p1
+              then
+               destructure_hyps n (Tnot p1 :: l) ++
+               destructure_hyps n (Tnot p2 :: l)
+              else map_cons _ (Tnot p) (destructure_hyps n l)
+          | _ => map_cons _ (Tnot p) (destructure_hyps n l)
+          end
+      | x :: l => map_cons _ x (destructure_hyps n l)
+      end
+  end.
+
+Theorem map_cons_val :
+ forall (ep : PropList) (e : list Z) (p : proposition)
+   (l : list (list proposition)),
+ interp_proposition ep e p ->
+ interp_list_hyps ep e l -> interp_list_hyps ep e (map_cons _ p l).
+
+simple induction l; simpl in |- *; [ auto | intros; elim H1; intro H2; auto ].
+Qed.
+
+Hint Resolve map_cons_val append_valid decidable_correct.
+
+Theorem destructure_hyps_valid :
+ forall n : nat, valid_list_hyps (destructure_hyps n).
+
+simple induction n;
+ [ unfold valid_list_hyps in |- *; simpl in |- *; auto
+ | unfold valid_list_hyps at 2 in |- *; intros n1 H ep e lp; case lp;
+    [ simpl in |- *; auto
+    | intros p l; case p;
+       try
+        (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0;
+          auto);
+       [ intro p'; case p';
+          try
+           (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0;
+             auto);
+          [ simpl in |- *; intros p1 (H1, H2);
+             pattern (decidability p1) in |- *; apply bool_ind2; 
+             intro H3;
+             [ apply H; simpl in |- *; split;
+                [ apply not_not; auto | assumption ]
+             | auto ]
+          | 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_ind2; 
+             intro H3;
+             [ apply append_valid; elim not_and with (2 := H1);
+                [ intro; left; apply H; simpl in |- *; auto
+                | intro; right; apply H; simpl in |- *; auto
+                | auto ]
+             | auto ] ]
+       | simpl in |- *; intros p1 p2 (H1, H2); apply append_valid;
+          (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_ind2; 
+          intro H3;
+          [ apply append_valid; elim imp_simp with (2 := H1);
+             [ intro H4; left; simpl in |- *; apply H; simpl in |- *; auto
+             | intro H4; right; simpl in |- *; apply H; simpl in |- *; auto
+             | auto ]
+          | auto ] ] ] ].
+
+Qed.
+
+Definition prop_stable (f : proposition -> proposition) :=
+  forall (ep : PropList) (e : list Z) (p : proposition),
+  interp_proposition ep e p <-> interp_proposition ep e (f p).
+
+Definition p_apply_left (f : proposition -> proposition) 
+  (p : proposition) :=
+  match p with
+  | Timp x y => Timp (f x) y
+  | Tor x y => Tor (f x) y
+  | Tand x y => Tand (f x) y
+  | Tnot x => Tnot (f x)
+  | x => x
+  end.
+
+Theorem p_apply_left_stable :
+ forall f : proposition -> proposition,
+ prop_stable f -> prop_stable (p_apply_left f).
+
+unfold prop_stable in |- *; intros f H ep e p; split;
+ (case p; simpl in |- *; auto; intros p1; elim (H ep e p1); tauto).
+Qed.
+
+Definition p_apply_right (f : proposition -> proposition)
+  (p : proposition) :=
+  match p with
+  | Timp x y => Timp x (f y)
+  | Tor x y => Tor x (f y)
+  | Tand x y => Tand x (f y)
+  | Tnot x => Tnot (f x)
+  | x => x
+  end.
+
+Theorem p_apply_right_stable :
+ forall f : proposition -> proposition,
+ prop_stable f -> prop_stable (p_apply_right f).
+
+unfold prop_stable in |- *; intros f H ep e p; split;
+ (case p; simpl in |- *; auto;
+   [ intros p1; elim (H ep e p1); tauto
+   | intros p1 p2; elim (H ep e p2); tauto
+   | intros p1 p2; elim (H ep e p2); tauto
+   | intros p1 p2; elim (H ep e p2); tauto ]).
+Qed.
+
+Definition p_invert (f : proposition -> proposition) 
+  (p : proposition) :=
+  match p with
+  | EqTerm x y => Tnot (f (NeqTerm x y))
+  | LeqTerm x y => Tnot (f (GtTerm x y))
+  | GeqTerm x y => Tnot (f (LtTerm x y))
+  | GtTerm x y => Tnot (f (LeqTerm x y))
+  | LtTerm x y => Tnot (f (GeqTerm x y))
+  | NeqTerm x y => Tnot (f (EqTerm x y))
+  | x => x
+  end.
+
+Theorem p_invert_stable :
+ forall f : proposition -> proposition,
+ prop_stable f -> prop_stable (p_invert f).
+
+unfold prop_stable in |- *; intros f H ep e p; split;
+ (case p; simpl in |- *; auto;
+   [ intros t1 t2; elim (H ep e (NeqTerm t1 t2)); simpl in |- *;
+      unfold Zne in |- *;
+      generalize (dec_eq (interp_term e t1) (interp_term e t2));
+      unfold decidable in |- *; tauto
+   | intros t1 t2; elim (H ep e (GtTerm t1 t2)); simpl in |- *;
+      unfold Zgt in |- *;
+      generalize (dec_Zgt (interp_term e t1) (interp_term e t2));
+      unfold decidable, Zgt, Zle in |- *; tauto
+   | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl in |- *;
+      unfold Zlt in |- *;
+      generalize (dec_Zlt (interp_term e t1) (interp_term e t2));
+      unfold decidable, Zge in |- *; tauto
+   | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl in |- *;
+      generalize (dec_Zgt (interp_term e t1) (interp_term e t2));
+      unfold Zle, Zgt in |- *; unfold decidable in |- *; 
+      tauto
+   | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl in |- *;
+      generalize (dec_Zlt (interp_term e t1) (interp_term e t2));
+      unfold Zge, Zlt in |- *; unfold decidable in |- *; 
+      tauto
+   | intros t1 t2; elim (H ep e (EqTerm t1 t2)); simpl in |- *;
+      generalize (dec_eq (interp_term e t1) (interp_term e t2));
+      unfold decidable, Zne in |- *; tauto ]).
+Qed.
+
+Theorem Zlt_left_inv : forall x y : Z, (0 <= y + -1 + - x)%Z -> (x < y)%Z.
+
+intros; apply Zsucc_lt_reg; apply Zle_lt_succ;
+ apply (fun a b : Z => Zplus_le_reg_r a b (-1 + - x)); 
+ rewrite Zplus_assoc; unfold Zsucc in |- *; rewrite (Zplus_assoc_reverse x);
+ rewrite (Zplus_assoc y); simpl in |- *; rewrite Zplus_0_r;
+ rewrite Zplus_opp_r; assumption.
+Qed.
+
+Theorem move_right_stable : forall s : step, prop_stable (move_right s).
+
+unfold move_right, prop_stable in |- *; intros s ep e p; split;
+ [ Simplify; simpl in |- *; elim (rewrite_stable s e); simpl in |- *;
+    [ symmetry  in |- *; apply Zegal_left; assumption
+    | intro; apply Zle_left; assumption
+    | intro; apply Zge_left; assumption
+    | intro; apply Zgt_left; assumption
+    | intro; apply Zlt_left; assumption
+    | intro; apply Zne_left_2; assumption ]
+ | case p; simpl in |- *; intros; auto; generalize H; elim (rewrite_stable s);
+    simpl in |- *; intro H1;
+    [ rewrite (Zplus_0_r_reverse (interp_term e t0)); rewrite H1;
+       rewrite Zplus_permute; rewrite Zplus_opp_r; 
+       rewrite Zplus_0_r; trivial
+    | apply (fun a b : Z => Zplus_le_reg_r a b (- interp_term e t));
+       rewrite Zplus_opp_r; assumption
+    | apply Zle_ge;
+       apply (fun a b : Z => Zplus_le_reg_r a b (- interp_term e t0));
+       rewrite Zplus_opp_r; assumption
+    | apply Zlt_gt; apply Zlt_left_inv; assumption
+    | apply Zlt_left_inv; assumption
+    | unfold Zne, not in |- *; unfold Zne in H1; intro H2; apply H1;
+       rewrite H2; rewrite Zplus_opp_r; trivial ] ].
+Qed.
+
+
+Fixpoint p_rewrite (s : p_step) : proposition -> proposition :=
+  match s with
+  | P_LEFT s => p_apply_left (p_rewrite s)
+  | P_RIGHT s => p_apply_right (p_rewrite s)
+  | P_STEP s => move_right s
+  | P_INVERT s => p_invert (move_right s)
+  | P_NOP => fun p : proposition => p
+  end.
+
+Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s).
+
+
+simple induction s; simpl in |- *;
+ [ intros; apply p_apply_left_stable; trivial
+ | intros; apply p_apply_right_stable; trivial
+ | intros; apply p_invert_stable; apply move_right_stable
+ | apply move_right_stable
+ | unfold prop_stable in |- *; simpl in |- *; intros; split; auto ].
+Qed.
+
+Fixpoint normalize_hyps (l : list h_step) (lh : list proposition) {struct l}
+ : list proposition :=
+  match l with
+  | nil => lh
+  | pair_step i s :: r => normalize_hyps r (apply_oper_1 i (p_rewrite s) lh)
+  end.
+
+Theorem normalize_hyps_valid :
+ forall l : list h_step, valid_hyps (normalize_hyps l).
+
+simple induction l; unfold valid_hyps in |- *; simpl in |- *;
+ [ auto
+ | intros n_s r; case n_s; intros n s H ep e lp H1; apply H;
+    apply apply_oper_1_valid;
+    [ unfold valid1 in |- *; intros ep1 e1 p1 H2;
+       elim (p_rewrite_stable s ep1 e1 p1); auto
+    | assumption ] ].
+Qed.
+
+Theorem normalize_hyps_goal :
+ forall (s : list h_step) (ep : PropList) (env : list Z)
+   (l : list proposition),
+ (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+  interp_goal_concl envp env FalseTerm l) ep env (normalize_hyps s l) ->
+ (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+  interp_goal_concl envp env FalseTerm l) ep env l.
+
+intros; apply valid_goal with (2 := H); apply normalize_hyps_valid.
+Qed.
+
+Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} :
+ proposition :=
+  match s with
+  | D_left :: l =>
+      match p with
+      | Tand x y => extract_hyp_pos l x
+      | _ => p
+      end
+  | D_right :: l =>
+      match p with
+      | Tand x y => extract_hyp_pos l y
+      | _ => p
+      end
+  | D_mono :: l => match p with
+                   | Tnot x => extract_hyp_neg l x
+                   | _ => p
+                   end
+  | _ => p
+  end
+ 
+ with extract_hyp_neg (s : list direction) (p : proposition) {struct s} :
+ proposition :=
+  match s with
+  | D_left :: l =>
+      match p with
+      | Tor x y => extract_hyp_neg l x
+      | Timp x y => if decidability x then extract_hyp_pos l x else Tnot p
+      | _ => Tnot p
+      end
+  | D_right :: l =>
+      match p with
+      | Tor x y => extract_hyp_neg l y
+      | Timp x y => extract_hyp_neg l y
+      | _ => Tnot p
+      end
+  | D_mono :: l =>
+      match p with
+      | Tnot x => if decidability x then extract_hyp_pos l x else Tnot p
+      | _ => Tnot p
+      end
+  | _ =>
+      match p with
+      | Tnot x => if decidability x then x else Tnot p
+      | _ => Tnot p
+      end
+  end.
+
+Definition co_valid1 (f : proposition -> proposition) :=
+  forall (ep : PropList) (e : list Z) (p1 : proposition),
+  interp_proposition ep e (Tnot p1) -> interp_proposition ep e (f p1).
+
+Theorem extract_valid :
+ forall s : list direction,
+ valid1 (extract_hyp_pos s) /\ co_valid1 (extract_hyp_neg s).
+
+unfold valid1, co_valid1 in |- *; simple induction s;
+ [ split;
+    [ simpl in |- *; auto
+    | intros ep e p1; case p1; simpl in |- *; auto; intro p;
+       pattern (decidability p) in |- *; apply bool_ind2;
+       [ intro H; generalize (decidable_correct ep e p H);
+          unfold decidable in |- *; tauto
+       | simpl in |- *; auto ] ]
+ | intros a s' (H1, H2); simpl in H2; split; intros ep e p; case a; auto;
+    case p; auto; simpl in |- *; intros;
+    (apply H1; tauto) ||
+      (apply H2; tauto) ||
+        (pattern (decidability p0) in |- *; apply bool_ind2;
+          [ intro H3; generalize (decidable_correct ep e p0 H3);
+             unfold decidable in |- *; intro H4; apply H1; 
+             tauto
+          | intro; tauto ]) ].
+
+Qed.
+
+Fixpoint decompose_solve (s : e_step) (h : list proposition) {struct s} :
+ list (list proposition) :=
+  match s with
+  | E_SPLIT i dl s1 s2 =>
+      match extract_hyp_pos dl (nth_hyps i h) with
+      | Tor x y => decompose_solve s1 (x :: h) ++ decompose_solve s2 (y :: h)
+      | Tnot (Tand x y) =>
+          if decidability x
+          then
+           decompose_solve s1 (Tnot x :: h) ++
+           decompose_solve s2 (Tnot y :: h)
+          else h :: nil
+      | _ => h :: nil
+      end
+  | E_EXTRACT i dl s1 =>
+      decompose_solve s1 (extract_hyp_pos dl (nth_hyps i h) :: h)
+  | E_SOLVE t => execute_omega t h
+  end.
 
+Theorem decompose_solve_valid :
+ forall s : e_step, valid_list_goal (decompose_solve s).
+
+intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s;
+ simpl in |- *; intros;
+ [ cut (interp_proposition ep e1 (extract_hyp_pos l (nth_hyps n lp)));
+    [ case (extract_hyp_pos l (nth_hyps n lp)); simpl in |- *; auto;
+       [ intro p; case p; simpl in |- *; auto; intros p1 p2 H2;
+          pattern (decidability p1) in |- *; apply bool_ind2;
+          [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4;
+             apply append_valid; elim H4; intro H5;
+             [ right; apply H0; simpl in |- *; tauto
+             | left; apply H; simpl in |- *; tauto ]
+          | 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 ] ]
+    | elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto ]
+ | intros; apply H; simpl in |- *; split;
+    [ elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto
+    | auto ]
+ | apply omega_valid with (1 := H) ].
+
+Qed.
+
+(* \subsection{La dernière étape qui élimine tous les séquents inutiles} *)
+
+Definition valid_lhyps
+  (f : list (list proposition) -> list (list proposition)) :=
+  forall (ep : PropList) (e : list Z) (lp : list (list proposition)),
+  interp_list_hyps ep e lp -> interp_list_hyps ep e (f lp).
+
+Fixpoint reduce_lhyps (lp : list (list proposition)) :
+ list (list proposition) :=
+  match lp with
+  | (FalseTerm :: nil) :: lp' => reduce_lhyps lp'
+  | x :: lp' => x :: reduce_lhyps lp'
+  | nil => nil (A:=list proposition)
+  end.
+
+Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps.
+
+unfold valid_lhyps in |- *; intros ep e lp; elim lp;
+ [ simpl in |- *; auto
+ | intros a l HR; elim a;
+    [ simpl in |- *; tauto
+    | intros a1 l1; case l1; case a1; simpl in |- *; try tauto ] ].
+Qed.
+
+Theorem do_reduce_lhyps :
+ forall (envp : PropList) (env : list Z) (l : list (list proposition)),
+ interp_list_goal envp env (reduce_lhyps l) -> interp_list_goal envp env l.
+
+intros envp env l H; apply list_goal_to_hyps; intro H1;
+ apply list_hyps_to_goal with (1 := H); apply reduce_lhyps_valid; 
+ assumption.
 Qed.
+
+Definition concl_to_hyp (p : proposition) :=
+  if decidability p then Tnot p else TrueTerm.
+
+Definition do_concl_to_hyp :
+  forall (envp : PropList) (env : list Z) (c : proposition)
+    (l : list proposition),
+  (fun (envp : PropList) (env : list Z) (l : list proposition) =>
+   interp_goal_concl envp env FalseTerm l) envp env (
+    concl_to_hyp c :: l) -> interp_goal_concl envp env c l.
+
+simpl in |- *; intros envp env c l; induction  l as [| a l Hrecl];
+ [ simpl in |- *; unfold concl_to_hyp in |- *;
+    pattern (decidability c) in |- *; apply bool_ind2;
+    [ intro H; generalize (decidable_correct envp env c H);
+       unfold decidable in |- *; simpl in |- *; tauto
+    | simpl in |- *; intros H1 H2; elim H2; trivial ]
+ | simpl in |- *; tauto ].
+Qed.
+
+Definition omega_tactic (t1 : e_step) (t2 : list h_step) 
+  (c : proposition) (l : list proposition) :=
+  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 : PropList) 
+   (env : list Z) (c : proposition) (l : list proposition),
+ interp_list_goal envp env (omega_tactic t1 t2 c l) ->
+ interp_goal_concl envp env c l.
+
+unfold omega_tactic in |- *; intros; apply do_concl_to_hyp;
+ apply (normalize_hyps_goal t2); apply (decompose_solve_valid t1);
+ apply do_reduce_lhyps; assumption.
+Qed.
\ No newline at end of file
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 28a969babc..b896614312 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -7,7 +7,7 @@
  *************************************************************************)
 
 let module_refl_name = "ReflOmegaCore"
-let module_refl_path = ["romega"; module_refl_name]
+let module_refl_path = ["Coq"; "romega"; module_refl_name]
 
 type result = 
    Kvar of string
@@ -17,19 +17,20 @@ type result =
 
 let destructurate t =
   let c, args = Term.decompose_app t in
-(*  let env = Global.env() in*)
+  let env = Global.env() in
   match Term.kind_of_term c, args with
     | Term.Const sp, args ->
 	Kapp (Names.string_of_id
 		(Nametab.id_of_global (Libnames.ConstRef sp)),
-              args)
+	      args)
     | Term.Construct csp , args ->
 	Kapp (Names.string_of_id
 		(Nametab.id_of_global (Libnames.ConstructRef csp)),
-	        args)
+	      args)
     | Term.Ind isp, args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.IndRef isp)),args)
+		(Nametab.id_of_global (Libnames.IndRef isp)),
+	      args)
     | Term.Var id,[] -> Kvar(Names.string_of_id id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
@@ -39,15 +40,14 @@ let destructurate t =
 exception Destruct
 
 let dest_const_apply t = 
-  let f,args = Term.decompose_app t in
+  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
     | _ -> raise Destruct
-  in
-  Nametab.id_of_global ref, args
+  in  Nametab.id_of_global ref, args
 
 let recognize_number t =
   let rec loop t =
@@ -62,26 +62,17 @@ let recognize_number t =
        "POS",[t] -> loop t | "NEG",[t] -> - (loop t) | "ZERO",[] -> 0
      | _ -> failwith "not a number";;
 
-let init_dir = ["Coq";"Init"]
-let arith_dir = ["Coq";"Arith"]
-let logic_dir = ["Coq";"Logic"]
-let zarith_dir = ["Coq";"ZArith"]
-let list_dir = ["Coq";"Lists"]
-let coq_modules = [
-  zarith_dir@["fast_integer"];
-  zarith_dir@["zarith_aux"];
-  zarith_dir@["auxiliary"];
-  init_dir@["Datatypes"];
-  init_dir@["Peano"];
-  init_dir@["Logic"];
-  arith_dir@["Compare_dec"];
-  arith_dir@["Peano_dec"];
-  arith_dir@["Minus"];
-  logic_dir@["Decidable"];
-  list_dir@["PolyList"]
-]
-
-let constant = Coqlib.gen_constant_in_modules "ROmega" coq_modules
+
+let logic_dir = ["Coq";"Logic";"Decidable"]
+
+let coq_modules =
+  Coqlib.init_modules @ [logic_dir] @ Coqlib.arith_modules @ Coqlib.zarith_base_modules
+    @ [["Coq"; "omega"; "OmegaLemmas"]]
+    @ [["Coq"; "Lists"; (if !Options.v7 then "PolyList" else "List")]]
+    @ [module_refl_path]
+
+
+let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules
 
 let coq_xH = lazy (constant "xH")
 let coq_xO = lazy (constant "xO")
@@ -90,119 +81,334 @@ let coq_ZERO = lazy (constant "ZERO")
 let coq_POS = lazy (constant "POS")
 let coq_NEG = lazy (constant "NEG")
 let coq_Z = lazy (constant "Z")
-let coq_relation = lazy (constant "relation")
+let coq_relation = lazy (constant  (if !Options.v7 then "relation" else "comparis
+on"))
 let coq_SUPERIEUR = lazy (constant "SUPERIEUR")
 let coq_INFEEIEUR = lazy (constant "INFERIEUR")
 let coq_EGAL = lazy (constant "EGAL")
 let coq_Zplus = lazy (constant "Zplus")
-let coq_Zmult = lazy (constant "Zmult")
+let coq_Zmult = lazy (constant  "Zmult")
 let coq_Zopp = lazy (constant "Zopp")
 
-(* auxiliaires zarith *)
 let coq_Zminus = lazy (constant "Zminus")
-let coq_Zs = lazy (constant "Zs")
+let coq_Zs = lazy (constant  "Zs")
 let coq_Zgt = lazy (constant "Zgt")
 let coq_Zle = lazy (constant "Zle")
-let coq_inject_nat = lazy (constant "inject_nat")
+let coq_inject_nat = lazy (constant  "inject_nat")
 
 (* Peano *)
 let coq_le = lazy(constant "le")
 let coq_gt = lazy(constant "gt")
 
-(* Datatypes *)
+(* Integers *)
 let coq_nat = lazy(constant "nat")
 let coq_S = lazy(constant "S")
 let coq_O = lazy(constant "O")
-
-(* Minus *)
 let coq_minus = lazy(constant "minus")
 
 (* Logic *)
-let coq_eq = lazy(constant "eq")
-let coq_refl_equal = lazy(constant "refl_equal")
+let coq_eq = lazy(constant  "eq")
+let coq_refl_equal = lazy(constant  "refl_equal")
 let coq_and = lazy(constant "and")
 let coq_not = lazy(constant "not")
 let coq_or = lazy(constant "or")
+let coq_true = lazy(constant "true")
+let coq_false = lazy(constant "false")
 let coq_ex = lazy(constant "ex")
+let coq_I = lazy(constant "I")
 
 (* Lists *)
 let coq_cons =  lazy (constant "cons")
 let coq_nil =  lazy (constant "nil")
 
-let romega_constant = Coqlib.gen_constant "ROmega" module_refl_path
-
-let coq_t_nat = lazy (romega_constant "Tint")
-let coq_t_plus = lazy (romega_constant "Tplus")
-let coq_t_mult = lazy (romega_constant "Tmult")
-let coq_t_opp = lazy (romega_constant "Topp")
-let coq_t_minus = lazy (romega_constant "Tminus")
-let coq_t_var = lazy (romega_constant "Tvar")
-let coq_t_equal = lazy (romega_constant "EqTerm")
-let coq_t_leq = lazy (romega_constant "LeqTerm")
-let coq_t_geq = lazy (romega_constant "GeqTerm")
-let coq_t_lt = lazy (romega_constant "LtTerm")
-let coq_t_gt = lazy (romega_constant "GtTerm")
-let coq_t_neq = lazy (romega_constant "NeqTerm")
-
-let coq_proposition = lazy (romega_constant "proposition")
-let coq_interp_sequent = lazy (romega_constant "interp_goal")
-let coq_normalize_sequent = lazy (romega_constant "normalize_goal")
-let coq_execute_sequent = lazy (romega_constant "execute_goal")
-let coq_sequent_to_hyps = lazy (romega_constant "goal_to_hyps")
+let coq_pcons = lazy (constant "Pcons")
+let coq_pnil = lazy (constant "Pnil")
+
+let coq_h_step = lazy (constant "h_step")
+let coq_pair_step = lazy (constant  "pair_step")
+let coq_p_left = lazy (constant  "P_LEFT")
+let coq_p_right = lazy (constant  "P_RIGHT")
+let coq_p_invert = lazy (constant  "P_INVERT")
+let coq_p_step = lazy (constant  "P_STEP")
+let coq_p_nop = lazy (constant  "P_NOP")
+
+
+let coq_t_int = lazy (constant  "Tint")
+let coq_t_plus = lazy (constant  "Tplus")
+let coq_t_mult = lazy (constant  "Tmult")
+let coq_t_opp = lazy (constant  "Topp")
+let coq_t_minus = lazy (constant  "Tminus")
+let coq_t_var = lazy (constant  "Tvar")
+
+let coq_p_eq = lazy (constant  "EqTerm")
+let coq_p_leq = lazy (constant  "LeqTerm")
+let coq_p_geq = lazy (constant  "GeqTerm")
+let coq_p_lt = lazy (constant  "LtTerm")
+let coq_p_gt = lazy (constant  "GtTerm")
+let coq_p_neq = lazy (constant  "NeqTerm")
+let coq_p_true = lazy (constant  "TrueTerm")
+let coq_p_false = lazy (constant  "FalseTerm")
+let coq_p_not = lazy (constant  "Tnot")
+let coq_p_or = lazy (constant  "Tor")
+let coq_p_and = lazy (constant  "Tand")
+let coq_p_imp = lazy (constant  "Timp")
+let coq_p_prop = lazy (constant  "Tprop")
+
+let coq_proposition = lazy (constant  "proposition")
+let coq_interp_sequent = lazy (constant  "interp_goal_concl")
+let coq_normalize_sequent = lazy (constant  "normalize_goal")
+let coq_execute_sequent = lazy (constant  "execute_goal")
+let coq_do_concl_to_hyp =  lazy (constant  "do_concl_to_hyp")
+let coq_sequent_to_hyps = lazy (constant  "goal_to_hyps")
+let coq_normalize_hyps_goal =
+  lazy (constant  "normalize_hyps_goal")
 
 (* Constructors for shuffle tactic *)
-let coq_t_fusion =  lazy (romega_constant "t_fusion")
-let coq_f_equal =  lazy (romega_constant "F_equal")
-let coq_f_cancel =  lazy (romega_constant "F_cancel")
-let coq_f_left =  lazy (romega_constant "F_left")
-let coq_f_right =  lazy (romega_constant "F_right")
+let coq_t_fusion =  lazy (constant  "t_fusion")
+let coq_f_equal =  lazy (constant  "F_equal")
+let coq_f_cancel =  lazy (constant  "F_cancel")
+let coq_f_left =  lazy (constant  "F_left")
+let coq_f_right =  lazy (constant  "F_right")
 
 (* Constructors for reordering tactics *)
-let coq_step = lazy (romega_constant "step")
-let coq_c_do_both = lazy (romega_constant "C_DO_BOTH")
-let coq_c_do_left = lazy (romega_constant "C_LEFT")
-let coq_c_do_right = lazy (romega_constant "C_RIGHT")
-let coq_c_do_seq = lazy (romega_constant "C_SEQ")
-let coq_c_nop = lazy (romega_constant "C_NOP")
-let coq_c_opp_plus = lazy (romega_constant "C_OPP_PLUS")
-let coq_c_opp_opp = lazy (romega_constant "C_OPP_OPP")
-let coq_c_opp_mult_r = lazy (romega_constant "C_OPP_MULT_R")
-let coq_c_opp_one = lazy (romega_constant "C_OPP_ONE")
-let coq_c_reduce = lazy (romega_constant "C_REDUCE")
-let coq_c_mult_plus_distr = lazy (romega_constant "C_MULT_PLUS_DISTR")
-let coq_c_opp_left = lazy (romega_constant "C_MULT_OPP_LEFT")
-let coq_c_mult_assoc_r = lazy (romega_constant "C_MULT_ASSOC_R")
-let coq_c_plus_assoc_r = lazy (romega_constant "C_PLUS_ASSOC_R")
-let coq_c_plus_assoc_l = lazy (romega_constant "C_PLUS_ASSOC_L")
-let coq_c_plus_permute = lazy (romega_constant "C_PLUS_PERMUTE")
-let coq_c_plus_sym = lazy (romega_constant "C_PLUS_SYM")
-let coq_c_red0 = lazy (romega_constant "C_RED0")
-let coq_c_red1 = lazy (romega_constant "C_RED1")
-let coq_c_red2 = lazy (romega_constant "C_RED2")
-let coq_c_red3 = lazy (romega_constant "C_RED3")
-let coq_c_red4 = lazy (romega_constant "C_RED4")
-let coq_c_red5 = lazy (romega_constant "C_RED5")
-let coq_c_red6 = lazy (romega_constant "C_RED6")
-let coq_c_mult_opp_left = lazy (romega_constant "C_MULT_OPP_LEFT")
+let coq_step = lazy (constant  "step")
+let coq_c_do_both = lazy (constant  "C_DO_BOTH")
+let coq_c_do_left = lazy (constant  "C_LEFT")
+let coq_c_do_right = lazy (constant  "C_RIGHT")
+let coq_c_do_seq = lazy (constant  "C_SEQ")
+let coq_c_nop = lazy (constant  "C_NOP")
+let coq_c_opp_plus = lazy (constant  "C_OPP_PLUS")
+let coq_c_opp_opp = lazy (constant  "C_OPP_OPP")
+let coq_c_opp_mult_r = lazy (constant  "C_OPP_MULT_R")
+let coq_c_opp_one = lazy (constant  "C_OPP_ONE")
+let coq_c_reduce = lazy (constant  "C_REDUCE")
+let coq_c_mult_plus_distr = lazy (constant  "C_MULT_PLUS_DISTR")
+let coq_c_opp_left = lazy (constant  "C_MULT_OPP_LEFT")
+let coq_c_mult_assoc_r = lazy (constant  "C_MULT_ASSOC_R")
+let coq_c_plus_assoc_r = lazy (constant  "C_PLUS_ASSOC_R")
+let coq_c_plus_assoc_l = lazy (constant  "C_PLUS_ASSOC_L")
+let coq_c_plus_permute = lazy (constant  "C_PLUS_PERMUTE")
+let coq_c_plus_sym = lazy (constant  "C_PLUS_SYM")
+let coq_c_red0 = lazy (constant  "C_RED0")
+let coq_c_red1 = lazy (constant  "C_RED1")
+let coq_c_red2 = lazy (constant  "C_RED2")
+let coq_c_red3 = lazy (constant  "C_RED3")
+let coq_c_red4 = lazy (constant  "C_RED4")
+let coq_c_red5 = lazy (constant  "C_RED5")
+let coq_c_red6 = lazy (constant  "C_RED6")
+let coq_c_mult_opp_left = lazy (constant  "C_MULT_OPP_LEFT")
 let coq_c_mult_assoc_reduced = 
-  lazy (romega_constant "C_MULT_ASSOC_REDUCED")
-let coq_c_minus = lazy (romega_constant "C_MINUS")
-let coq_c_mult_sym = lazy (romega_constant "C_MULT_SYM")
-
-let coq_s_constant_not_nul = lazy (romega_constant "O_CONSTANT_NOT_NUL")
-let coq_s_constant_neg = lazy (romega_constant "O_CONSTANT_NEG")
-let coq_s_div_approx = lazy (romega_constant "O_DIV_APPROX")
-let coq_s_not_exact_divide = lazy (romega_constant "O_NOT_EXACT_DIVIDE")
-let coq_s_exact_divide = lazy (romega_constant "O_EXACT_DIVIDE")
-let coq_s_sum = lazy (romega_constant "O_SUM")
-let coq_s_state = lazy (romega_constant "O_STATE")
-let coq_s_contradiction = lazy (romega_constant "O_CONTRADICTION")
-let coq_s_merge_eq = lazy (romega_constant "O_MERGE_EQ")
-let coq_s_split_ineq =lazy (romega_constant "O_SPLIT_INEQ")
-let coq_s_constant_nul =lazy (romega_constant "O_CONSTANT_NUL")
-let coq_s_negate_contradict =lazy (romega_constant "O_NEGATE_CONTRADICT")
-let coq_s_negate_contradict_inv =lazy (romega_constant "O_NEGATE_CONTRADICT_INV")
+  lazy (constant  "C_MULT_ASSOC_REDUCED")
+let coq_c_minus = lazy (constant  "C_MINUS")
+let coq_c_mult_sym = lazy (constant  "C_MULT_SYM")
+
+let coq_s_constant_not_nul = lazy (constant  "O_CONSTANT_NOT_NUL")
+let coq_s_constant_neg = lazy (constant  "O_CONSTANT_NEG")
+let coq_s_div_approx = lazy (constant  "O_DIV_APPROX")
+let coq_s_not_exact_divide = lazy (constant  "O_NOT_EXACT_DIVIDE")
+let coq_s_exact_divide = lazy (constant  "O_EXACT_DIVIDE")
+let coq_s_sum = lazy (constant  "O_SUM")
+let coq_s_state = lazy (constant  "O_STATE")
+let coq_s_contradiction = lazy (constant  "O_CONTRADICTION")
+let coq_s_merge_eq = lazy (constant  "O_MERGE_EQ")
+let coq_s_split_ineq =lazy (constant  "O_SPLIT_INEQ")
+let coq_s_constant_nul =lazy (constant  "O_CONSTANT_NUL")
+let coq_s_negate_contradict =lazy (constant  "O_NEGATE_CONTRADICT")
+let coq_s_negate_contradict_inv =lazy (constant  "O_NEGATE_CONTRADICT_INV")
+
+(* construction for the [extract_hyp] tactic *)
+let coq_direction = lazy  (constant  "direction")
+let coq_d_left = lazy  (constant  "D_left")
+let coq_d_right = lazy  (constant  "D_right")
+let coq_d_mono = lazy  (constant  "D_mono")
+
+let coq_e_split = lazy  (constant  "E_SPLIT")
+let coq_e_extract = lazy  (constant  "E_EXTRACT")
+let coq_e_solve = lazy  (constant  "E_SOLVE")
+
+let coq_decompose_solve_valid = 
+  lazy (constant   "decompose_solve_valid")
+let coq_do_reduce_lhyps = lazy (constant   "do_reduce_lhyps")
+let coq_do_omega = lazy (constant  "do_omega")
+
+(**
+let constant dir s =
+   try
+     Libnames.constr_of_reference 
+       (Nametab.absolute_reference
+	  (Libnames.make_path
+             (Names.make_dirpath (List.map Names.id_of_string (List.rev dir)))
+             (Names.id_of_string s)))
+   with e -> print_endline (String.concat "." dir); print_endline s;
+             raise e
+
+let path_fast_integer = ["Coq"; "ZArith"; "fast_integer"]
+let path_zarith_aux = ["Coq"; "ZArith"; "zarith_aux"]
+let path_logic = ["Coq"; "Init";"Logic"]
+let path_datatypes = ["Coq"; "Init";"Datatypes"]
+let path_peano = ["Coq"; "Init"; "Peano"]
+let path_list = ["Coq"; "Lists"; "PolyList"]
+
+let coq_xH = lazy (constant path_fast_integer "xH")
+let coq_xO = lazy (constant path_fast_integer "xO")
+let coq_xI = lazy (constant path_fast_integer "xI")
+let coq_ZERO = lazy (constant path_fast_integer "ZERO")
+let coq_POS = lazy (constant path_fast_integer "POS")
+let coq_NEG = lazy (constant path_fast_integer "NEG")
+let coq_Z = lazy (constant path_fast_integer "Z")
+let coq_relation = lazy (constant path_fast_integer "relation")
+let coq_SUPERIEUR = lazy (constant path_fast_integer "SUPERIEUR")
+let coq_INFEEIEUR = lazy (constant path_fast_integer "INFERIEUR")
+let coq_EGAL = lazy (constant path_fast_integer "EGAL")
+let coq_Zplus = lazy (constant path_fast_integer "Zplus")
+let coq_Zmult = lazy (constant path_fast_integer "Zmult")
+let coq_Zopp = lazy (constant path_fast_integer "Zopp")
+
+(* auxiliaires zarith *)
+let coq_Zminus = lazy (constant path_zarith_aux "Zminus")
+let coq_Zs = lazy (constant path_zarith_aux "Zs")
+let coq_Zgt = lazy (constant path_zarith_aux "Zgt")
+let coq_Zle = lazy (constant path_zarith_aux "Zle")
+let coq_inject_nat = lazy (constant path_zarith_aux "inject_nat")
+
+(* Peano *)
+let coq_le = lazy(constant path_peano "le")
+let coq_gt = lazy(constant path_peano "gt")
+
+(* Integers *)
+let coq_nat = lazy(constant path_datatypes "nat")
+let coq_S = lazy(constant path_datatypes "S")
+let coq_O = lazy(constant path_datatypes "O")
+
+(* Minus *)
+let coq_minus = lazy(constant ["Arith"; "Minus"] "minus")
 
+(* Logic *)
+let coq_eq = lazy(constant path_logic "eq")
+let coq_refl_equal = lazy(constant path_logic "refl_equal")
+let coq_and = lazy(constant path_logic "and")
+let coq_not = lazy(constant path_logic "not")
+let coq_or = lazy(constant path_logic "or")
+let coq_true = lazy(constant path_logic "true")
+let coq_false = lazy(constant path_logic "false")
+let coq_ex = lazy(constant path_logic "ex")
+let coq_I = lazy(constant path_logic "I")
+
+(* Lists *)
+let coq_cons =  lazy (constant path_list  "cons")
+let coq_nil =  lazy (constant path_list "nil")
+
+let coq_pcons = lazy (constant module_refl_path "Pcons")
+let coq_pnil = lazy (constant module_refl_path "Pnil")
+
+let coq_h_step = lazy (constant module_refl_path "h_step")
+let coq_pair_step = lazy (constant module_refl_path "pair_step")
+let coq_p_left = lazy (constant module_refl_path "P_LEFT")
+let coq_p_right = lazy (constant module_refl_path "P_RIGHT")
+let coq_p_invert = lazy (constant module_refl_path "P_INVERT")
+let coq_p_step = lazy (constant module_refl_path "P_STEP")
+let coq_p_nop = lazy (constant module_refl_path "P_NOP")
+
+
+let coq_t_int = lazy (constant module_refl_path "Tint")
+let coq_t_plus = lazy (constant module_refl_path "Tplus")
+let coq_t_mult = lazy (constant module_refl_path "Tmult")
+let coq_t_opp = lazy (constant module_refl_path "Topp")
+let coq_t_minus = lazy (constant module_refl_path "Tminus")
+let coq_t_var = lazy (constant module_refl_path "Tvar")
+
+let coq_p_eq = lazy (constant module_refl_path "EqTerm")
+let coq_p_leq = lazy (constant module_refl_path "LeqTerm")
+let coq_p_geq = lazy (constant module_refl_path "GeqTerm")
+let coq_p_lt = lazy (constant module_refl_path "LtTerm")
+let coq_p_gt = lazy (constant module_refl_path "GtTerm")
+let coq_p_neq = lazy (constant module_refl_path "NeqTerm")
+let coq_p_true = lazy (constant module_refl_path "TrueTerm")
+let coq_p_false = lazy (constant module_refl_path "FalseTerm")
+let coq_p_not = lazy (constant module_refl_path "Tnot")
+let coq_p_or = lazy (constant module_refl_path "Tor")
+let coq_p_and = lazy (constant module_refl_path "Tand")
+let coq_p_imp = lazy (constant module_refl_path "Timp")
+let coq_p_prop = lazy (constant module_refl_path "Tprop")
+
+let coq_proposition = lazy (constant module_refl_path "proposition")
+let coq_interp_sequent = lazy (constant module_refl_path "interp_goal_concl")
+let coq_normalize_sequent = lazy (constant module_refl_path "normalize_goal")
+let coq_execute_sequent = lazy (constant module_refl_path "execute_goal")
+let coq_do_concl_to_hyp =  lazy (constant module_refl_path "do_concl_to_hyp")
+let coq_sequent_to_hyps = lazy (constant module_refl_path "goal_to_hyps")
+let coq_normalize_hyps_goal =
+  lazy (constant module_refl_path "normalize_hyps_goal")
+
+(* Constructors for shuffle tactic *)
+let coq_t_fusion =  lazy (constant module_refl_path "t_fusion")
+let coq_f_equal =  lazy (constant module_refl_path "F_equal")
+let coq_f_cancel =  lazy (constant module_refl_path "F_cancel")
+let coq_f_left =  lazy (constant module_refl_path "F_left")
+let coq_f_right =  lazy (constant module_refl_path "F_right")
+
+(* Constructors for reordering tactics *)
+let coq_step = lazy (constant module_refl_path "step")
+let coq_c_do_both = lazy (constant module_refl_path "C_DO_BOTH")
+let coq_c_do_left = lazy (constant module_refl_path "C_LEFT")
+let coq_c_do_right = lazy (constant module_refl_path "C_RIGHT")
+let coq_c_do_seq = lazy (constant module_refl_path "C_SEQ")
+let coq_c_nop = lazy (constant module_refl_path "C_NOP")
+let coq_c_opp_plus = lazy (constant module_refl_path "C_OPP_PLUS")
+let coq_c_opp_opp = lazy (constant module_refl_path "C_OPP_OPP")
+let coq_c_opp_mult_r = lazy (constant module_refl_path "C_OPP_MULT_R")
+let coq_c_opp_one = lazy (constant module_refl_path "C_OPP_ONE")
+let coq_c_reduce = lazy (constant module_refl_path "C_REDUCE")
+let coq_c_mult_plus_distr = lazy (constant module_refl_path "C_MULT_PLUS_DISTR")
+let coq_c_opp_left = lazy (constant module_refl_path "C_MULT_OPP_LEFT")
+let coq_c_mult_assoc_r = lazy (constant module_refl_path "C_MULT_ASSOC_R")
+let coq_c_plus_assoc_r = lazy (constant module_refl_path "C_PLUS_ASSOC_R")
+let coq_c_plus_assoc_l = lazy (constant module_refl_path "C_PLUS_ASSOC_L")
+let coq_c_plus_permute = lazy (constant module_refl_path "C_PLUS_PERMUTE")
+let coq_c_plus_sym = lazy (constant module_refl_path "C_PLUS_SYM")
+let coq_c_red0 = lazy (constant module_refl_path "C_RED0")
+let coq_c_red1 = lazy (constant module_refl_path "C_RED1")
+let coq_c_red2 = lazy (constant module_refl_path "C_RED2")
+let coq_c_red3 = lazy (constant module_refl_path "C_RED3")
+let coq_c_red4 = lazy (constant module_refl_path "C_RED4")
+let coq_c_red5 = lazy (constant module_refl_path "C_RED5")
+let coq_c_red6 = lazy (constant module_refl_path "C_RED6")
+let coq_c_mult_opp_left = lazy (constant module_refl_path "C_MULT_OPP_LEFT")
+let coq_c_mult_assoc_reduced = 
+  lazy (constant module_refl_path "C_MULT_ASSOC_REDUCED")
+let coq_c_minus = lazy (constant module_refl_path "C_MINUS")
+let coq_c_mult_sym = lazy (constant module_refl_path "C_MULT_SYM")
+
+let coq_s_constant_not_nul = lazy (constant module_refl_path "O_CONSTANT_NOT_NUL")
+let coq_s_constant_neg = lazy (constant module_refl_path "O_CONSTANT_NEG")
+let coq_s_div_approx = lazy (constant module_refl_path "O_DIV_APPROX")
+let coq_s_not_exact_divide = lazy (constant module_refl_path "O_NOT_EXACT_DIVIDE")
+let coq_s_exact_divide = lazy (constant module_refl_path "O_EXACT_DIVIDE")
+let coq_s_sum = lazy (constant module_refl_path "O_SUM")
+let coq_s_state = lazy (constant module_refl_path "O_STATE")
+let coq_s_contradiction = lazy (constant module_refl_path "O_CONTRADICTION")
+let coq_s_merge_eq = lazy (constant module_refl_path "O_MERGE_EQ")
+let coq_s_split_ineq =lazy (constant module_refl_path "O_SPLIT_INEQ")
+let coq_s_constant_nul =lazy (constant module_refl_path "O_CONSTANT_NUL")
+let coq_s_negate_contradict =lazy (constant module_refl_path "O_NEGATE_CONTRADICT")
+let coq_s_negate_contradict_inv =lazy (constant module_refl_path "O_NEGATE_CONTRADICT_INV")
+
+(* construction for the [extract_hyp] tactic *)
+let coq_direction = lazy  (constant module_refl_path "direction")
+let coq_d_left = lazy  (constant module_refl_path "D_left")
+let coq_d_right = lazy  (constant module_refl_path "D_right")
+let coq_d_mono = lazy  (constant module_refl_path "D_mono")
+
+let coq_e_split = lazy  (constant module_refl_path "E_SPLIT")
+let coq_e_extract = lazy  (constant module_refl_path "E_EXTRACT")
+let coq_e_solve = lazy  (constant module_refl_path "E_SOLVE")
+
+let coq_decompose_solve_valid = 
+  lazy (constant  module_refl_path "decompose_solve_valid")
+let coq_do_reduce_lhyps = lazy (constant  module_refl_path "do_reduce_lhyps")
+let coq_do_omega = lazy (constant module_refl_path "do_omega")
+
+*)
 (* \subsection{Construction d'expressions} *)
 
 
@@ -270,5 +476,14 @@ let mk_list typ l =
 	Term.mkApp (Lazy.force coq_cons, [|typ; step; loop l |]) in
   loop l
 
+let mk_plist l =
+  let rec loop = function
+    | [] ->
+	(Lazy.force coq_pnil)
+    | (step :: l) -> 
+	Term.mkApp (Lazy.force coq_pcons, [| step; loop l |]) in
+  loop l
+
+
 let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l
 
diff --git a/contrib/romega/g_romega.ml4 b/contrib/romega/g_romega.ml4
index b5203dcb72..386f7f2877 100644
--- a/contrib/romega/g_romega.ml4
+++ b/contrib/romega/g_romega.ml4
@@ -8,10 +8,8 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
-
 open Refl_omega
 
 TACTIC EXTEND ROmega
-  [ "ROmega" ] -> [ omega_solver ]
+  [ "ROmega" ] -> [ total_reflexive_omega_tactic ]
 END
diff --git a/contrib/romega/omega2.ml b/contrib/romega/omega2.ml
new file mode 100644
index 0000000000..913b7132e9
--- /dev/null
+++ b/contrib/romega/omega2.ml
@@ -0,0 +1,675 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(**************************************************************************)
+(*                                                                        *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
+(*                                                                        *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(*                                                                        *)
+(* 13/10/2002 : modified to cope with an external numbering of equations  *)
+(*   and hypothesis. Its use for Omega is not more complex and it makes   *)
+(*   things much simpler for the reflexive version where we should limit  *)
+(*   the number of source of numbering.                                   *)
+(**************************************************************************)
+
+open Names
+
+let flat_map f =
+ let rec flat_map_f = function
+   | [] -> [] 
+   | x :: l -> f x @ flat_map_f l
+ in 
+ flat_map_f
+
+let pp i = print_int i; print_newline (); flush stdout
+
+let debug = ref false
+
+let filter = List.partition
+
+let push v l = l := v :: !l
+
+let rec pgcd x y = if y = 0 then x else pgcd y (x mod y)
+
+let pgcd_l = function
+  | [] -> failwith "pgcd_l"
+  | x :: l -> List.fold_left pgcd x l
+
+let floor_div a b =
+  match a >=0 , b > 0 with
+    | true,true -> a / b
+    | false,false -> a / b
+    | true, false -> (a-1) / b - 1
+    | false,true  -> (a+1) / b - 1
+
+type coeff = {c: int ; v: int}
+
+type linear = coeff list
+
+type eqn_kind = EQUA | INEQ | DISE
+
+type afine = { 
+  (* a number uniquely identifying the equation *)
+  id: int ; 
+  (* a boolean true for an eq, false for an ineq (Sigma a_i x_i >= 0) *)
+  kind: eqn_kind; 
+  (* the variables and their coefficient *)
+  body: coeff list; 
+  (* a constant *)
+  constant: int }
+
+type state_action = {
+  st_new_eq : afine;
+  st_def    :  afine;
+  st_orig   : afine;
+  st_coef   : int;
+  st_var    : int }
+
+type action =
+  | DIVIDE_AND_APPROX of afine * afine * int * int
+  | NOT_EXACT_DIVIDE of afine * int
+  | FORGET_C of int
+  | EXACT_DIVIDE of afine * int
+  | SUM of int * (int * afine) * (int * afine)
+  | STATE of state_action 
+  | HYP of afine
+  | FORGET   of int * int
+  | FORGET_I of int * int
+  | CONTRADICTION of afine * afine
+  | NEGATE_CONTRADICT of afine * afine * bool
+  | MERGE_EQ of int * afine * int 
+  | CONSTANT_NOT_NUL of int * int
+  | CONSTANT_NUL of int
+  | CONSTANT_NEG of int * int
+  | SPLIT_INEQ of afine * (int * action list) * (int * action list)
+  | WEAKEN of int * int
+
+exception UNSOLVABLE
+
+exception NO_CONTRADICTION
+
+let display_eq print_var (l,e) =
+  let _ = 
+    List.fold_left 
+      (fun not_first f ->
+	 print_string 
+	   (if f.c < 0 then "- " else if not_first then "+ " else "");
+	 let c = abs f.c in
+	 if c = 1 then 
+	   Printf.printf "%s " (print_var f.v)
+	 else 
+	   Printf.printf "%d %s " c (print_var f.v); 
+	 true)
+      false l
+  in
+  if e > 0 then 
+    Printf.printf "+ %d " e 
+  else if e < 0 then 
+    Printf.printf "- %d " (abs e)
+
+let rec trace_length l =
+  let action_length accu = function
+    | SPLIT_INEQ (_,(_,l1),(_,l2)) ->
+	accu + 1 + trace_length l1 + trace_length l2
+    | _ -> accu + 1 in
+  List.fold_left action_length 0 l
+
+let operator_of_eq = function 
+  | EQUA -> "=" | DISE -> "!=" | INEQ -> ">="
+
+let kind_of = function
+  | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation"
+
+let display_system print_var l = 
+  List.iter 
+    (fun { kind=b; body=e; constant=c; id=id} -> 
+       print_int id; print_string ": ";
+       display_eq print_var (e,c); print_string (operator_of_eq b);
+       print_string "0\n") 
+    l;
+  print_string "------------------------\n\n"
+
+let display_inequations print_var l = 
+  List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l;
+  print_string "------------------------\n\n"
+
+let rec display_action print_var = function
+  | act :: l -> begin match act with
+      | DIVIDE_AND_APPROX (e1,e2,k,d) ->
+          Printf.printf 
+            "Inequation E%d is divided by %d and the constant coefficient is \
+            rounded by substracting %d.\n" e1.id k d
+      | NOT_EXACT_DIVIDE (e,k) ->
+          Printf.printf
+            "Constant in equation E%d is not divisible by the pgcd \
+            %d of its other coefficients.\n" e.id k
+      | EXACT_DIVIDE (e,k) ->
+          Printf.printf
+            "Equation E%d is divided by the pgcd \
+            %d of its coefficients.\n" e.id k
+      | WEAKEN (e,k) ->
+          Printf.printf 
+            "To ensure a solution in the dark shadow \
+            the equation E%d is weakened by %d.\n" e k
+      | SUM (e,(c1,e1),(c2,e2)) -> 
+          Printf.printf
+            "We state %s E%d = %d %s E%d + %d %s E%d.\n" 
+            (kind_of e1.kind) e c1 (kind_of e1.kind) e1.id c2 
+            (kind_of e2.kind) e2.id
+      | STATE { st_new_eq = e; st_coef = x} ->
+          Printf.printf "We define a new equation %d :" e.id; 
+          display_eq print_var (e.body,e.constant); 
+          print_string (operator_of_eq e.kind); print_string " 0\n"
+      | HYP e ->   
+          Printf.printf "We define %d :" e.id; 
+          display_eq print_var (e.body,e.constant); 
+          print_string (operator_of_eq e.kind); print_string " 0\n"
+      | FORGET_C e ->  Printf.printf "E%d is trivially satisfiable.\n" e
+      | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
+      | FORGET_I (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
+      | MERGE_EQ (e,e1,e2) ->
+         Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e
+      | CONTRADICTION (e1,e2) -> 
+          Printf.printf
+            "equations E%d and E%d implie a contradiction on their \
+            constant factors.\n" e1.id e2.id
+      | NEGATE_CONTRADICT(e1,e2,b) ->
+          Printf.printf
+            "Eqations E%d and E%d state that their body is at the same time
+            equal and different\n" e1.id e2.id
+      | CONSTANT_NOT_NUL (e,k) -> 
+          Printf.printf "equation E%d states %d=0.\n" e k
+      | CONSTANT_NEG(e,k) -> 
+          Printf.printf "equation E%d states %d >= 0.\n" e k
+      | CONSTANT_NUL e ->
+          Printf.printf "inequation E%d states 0 != 0.\n" e
+      | SPLIT_INEQ (e,(e1,l1),(e2,l2)) -> 
+          Printf.printf "equation E%d is split in E%d and E%d\n\n" e.id e1 e2;
+          display_action print_var l1;
+          print_newline ();
+          display_action print_var l2;
+          print_newline ()
+    end; display_action print_var l
+  | [] -> 
+      flush stdout
+
+(*""*)
+let default_print_var v = Printf.sprintf "XX%d" v
+
+let add_event, history, clear_history =
+  let accu = ref [] in
+  (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu),
+  (fun () -> !accu),
+  (fun () -> accu := [])
+
+let nf_linear = Sort.list (fun x y -> x.v > y.v)
+
+let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x))
+
+let map_eq_linear f = 
+  let rec loop = function
+    | x :: l -> let c = f x.c in if c=0 then loop l else {v=x.v; c=c} :: loop l
+    | [] -> [] 
+  in
+  loop
+
+let map_eq_afine f e = 
+  { id = e.id; kind = e.kind; body = map_eq_linear f e.body; 
+    constant = f e.constant }
+
+let negate_eq = map_eq_afine (fun x -> -x)
+
+let rec sum p0 p1 = match (p0,p1) with 
+  | ([], l) -> l | (l, []) -> l
+  | (((x1::l1) as l1'), ((x2::l2) as l2')) -> 
+      if x1.v = x2.v then
+	let c = x1.c + x2.c in
+	if c = 0 then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2
+      else if x1.v > x2.v then 
+	x1 :: sum l1 l2'
+      else 
+	x2 :: sum l1' l2
+
+let sum_afine new_eq_id eq1 eq2 = 
+  { kind = eq1.kind; id = new_eq_id ();
+    body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant }
+
+exception FACTOR1
+
+let rec chop_factor_1 = function
+  | x :: l -> 
+      if abs x.c = 1 then x,l else let (c',l') = chop_factor_1 l in (c',x::l')
+  | [] -> raise FACTOR1
+
+exception CHOPVAR
+
+let rec chop_var v = function
+  | f :: l -> if f.v = v then f,l else let (f',l') = chop_var v l in (f',f::l')
+  | [] -> raise CHOPVAR
+
+let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) =
+  if e = [] then begin 
+    match eq_flag with
+      | EQUA ->
+          if x =0 then [] else begin
+            add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE
+         end
+      | DISE ->
+          if x <> 0 then [] else begin
+            add_event (CONSTANT_NUL id); raise UNSOLVABLE
+          end
+      | INEQ ->
+          if x >= 0 then [] else begin
+            add_event (CONSTANT_NEG(id,x)); raise UNSOLVABLE
+          end
+  end else
+    let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in
+    if eq_flag=EQUA & x mod gcd <> 0 then begin
+      add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE
+    end else if eq_flag=DISE & x mod gcd <> 0 then begin
+      add_event (FORGET_C eq.id); []
+    end else if gcd <> 1 then begin
+      let c = floor_div x gcd in
+      let d = x - c * gcd in
+      let new_eq = {id=id; kind=eq_flag; constant=c; 
+                    body=map_eq_linear (fun c -> c / gcd) e} in
+      add_event (if eq_flag=EQUA or eq_flag = DISE then EXACT_DIVIDE(eq,gcd)
+                 else DIVIDE_AND_APPROX(eq,new_eq,gcd,d));
+      [new_eq]
+    end else [eq]
+
+let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2
+                        ({body=e1; constant=c1} as eq1) =
+  try
+    let (f,_) = chop_var v e1 in 
+    let coeff = if c_unite=1 then -f.c else if c_unite= -1 then f.c 
+                else failwith "eliminate_with_in" in
+    let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in
+    add_event (SUM (res.id,(1,eq1),(coeff,eq2))); res
+  with CHOPVAR -> eq1
+
+let omega_mod a b = a - b * floor_div (2 * a + b) (2 * b)
+let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = 
+  let e = original.body in
+  let sigma = new_var_id () in
+  let smallest,var =
+    try
+      List.fold_left (fun (v,p) c ->  if v > (abs c.c) then abs c.c,c.v else (v,p))
+              (abs (List.hd e).c, (List.hd e).v) (List.tl e)
+    with Failure "tl" -> display_system print_var [original] ; failwith "TL" in
+  let m = smallest + 1 in
+  let new_eq =
+    { constant = omega_mod original.constant m;
+      body = {c= -m;v=sigma} :: 
+             map_eq_linear (fun a -> omega_mod a m) original.body;
+      id = new_eq_id (); kind = EQUA } in
+  let definition =
+    { constant = - floor_div (2 * original.constant + m) (2 * m);
+      body = map_eq_linear (fun a -> - floor_div (2 * a + m) (2 * m))
+                             original.body;
+      id = new_eq_id (); kind = EQUA } in
+  add_event (STATE {st_new_eq = new_eq; st_def = definition;
+		    st_orig =original; st_coef = m; st_var = sigma});
+  let new_eq = List.hd (normalize new_eq) in
+  let eliminated_var, def = chop_var var new_eq.body in
+  let other_equations = 
+    flat_map (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e))
+             l1 in
+  let inequations = 
+    flat_map (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e))
+             l2 in
+  let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in
+  let mod_original = map_eq_afine (fun c -> c / m) original' in
+  add_event (EXACT_DIVIDE (original',m));
+  List.hd (normalize mod_original),other_equations,inequations
+
+let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) = 
+  if !debug then display_system print_var (e::other);
+  try
+    let v,def = chop_factor_1 e.body in
+    (flat_map (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other,
+     flat_map (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs)
+  with FACTOR1 -> 
+    eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs)
+
+let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) =
+  let rec fst_eq_1 = function
+     (eq::l) -> 
+        if List.exists (fun x -> abs x.c = 1) eq.body then eq,l
+        else let (eq',l') = fst_eq_1 l in (eq',eq::l')
+   | [] -> raise Not_found in
+  match sys_eq with
+     [] -> if !debug then display_system print_var sys_ineq; sys_ineq
+   | (e1::rest) -> 
+       let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in
+       if eq.body = [] then 
+         if eq.constant = 0 then begin
+           add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq)
+         end else begin
+           add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE
+         end
+       else
+	 banerjee new_ids 
+	   (eliminate_one_equation new_ids (eq,other,sys_ineq))
+
+type kind = INVERTED | NORMAL
+
+let redundancy_elimination new_eq_id system =
+  let normal = function
+     ({body=f::_} as e) when f.c < 0 ->  negate_eq e, INVERTED
+   | e -> e,NORMAL in
+  let table = Hashtbl.create 7 in
+  List.iter
+    (fun e -> 
+       let ({body=ne} as nx) ,kind = normal e in
+       if ne = [] then
+         if nx.constant < 0 then begin
+           add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE
+         end else add_event (FORGET_C nx.id)
+       else
+       try 
+         let (optnormal,optinvert) = Hashtbl.find table ne in
+         let final =
+           if kind = NORMAL then begin
+             match optnormal with 
+                Some v -> 
+                  let kept =
+                    if v.constant < nx.constant 
+                    then begin add_event (FORGET (v.id,nx.id));v end
+                    else begin add_event (FORGET (nx.id,v.id));nx end in
+                  (Some(kept),optinvert)
+              | None -> Some nx,optinvert
+           end else begin
+             match optinvert with 
+                Some v ->
+                  let kept =
+                    if v.constant > nx.constant 
+                    then begin add_event (FORGET_I (v.id,nx.id));v end
+                    else begin add_event (FORGET_I (nx.id,v.id));nx end in
+                  (optnormal,Some(if v.constant > nx.constant then v else nx))
+              | None -> optnormal,Some nx
+           end in
+         begin match final with
+            (Some high, Some low) -> 
+              if high.constant < low.constant then begin
+                add_event(CONTRADICTION (high,negate_eq low));
+                raise UNSOLVABLE
+              end
+          | _ -> () end;
+         Hashtbl.remove table ne;
+         Hashtbl.add table ne final
+       with Not_found ->
+         Hashtbl.add table ne 
+           (if kind = NORMAL then (Some nx,None) else (None,Some nx)))
+    system;
+  let accu_eq = ref [] in
+  let accu_ineq = ref [] in
+  Hashtbl.iter
+    (fun p0 p1 -> match (p0,p1) with 
+       | (e, (Some x, Some y)) when x.constant = y.constant -> 
+           let id=new_eq_id () in
+           add_event (MERGE_EQ(id,x,y.id));
+           push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq
+       | (e, (optnorm,optinvert)) ->
+           begin match optnorm with 
+               Some x -> push x accu_ineq | _ -> () end;
+           begin match optinvert with 
+               Some x -> push (negate_eq x) accu_ineq | _ -> () end)
+    table;
+  !accu_eq,!accu_ineq
+
+exception SOLVED_SYSTEM
+
+let select_variable system =
+  let table = Hashtbl.create 7 in
+  let push v c= 
+    try let r = Hashtbl.find table v in r := max !r (abs c)
+    with Not_found -> Hashtbl.add table v (ref (abs c)) in
+  List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system;
+  let vmin,cmin = ref (-1), ref 0 in
+  let var_cpt = ref 0 in
+  Hashtbl.iter
+    (fun v ({contents =  c}) ->
+       incr var_cpt;
+       if c < !cmin or !vmin = (-1) then begin vmin := v; cmin := c end)
+    table;
+  if !var_cpt < 1 then raise SOLVED_SYSTEM;
+  !vmin
+
+let classify v system =
+  List.fold_left 
+    (fun (not_occ,below,over) eq ->
+       try let f,eq' = chop_var v eq.body in
+       if f.c >= 0 then (not_occ,((f.c,eq) :: below),over)
+       else (not_occ,below,((-f.c,eq) :: over))
+       with CHOPVAR -> (eq::not_occ,below,over))
+    ([],[],[]) system
+
+let product new_eq_id dark_shadow low high =
+  List.fold_left
+    (fun accu (a,eq1) ->
+       List.fold_left
+         (fun accu (b,eq2) ->
+            let eq = 
+              sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1)
+                (map_eq_afine (fun c -> c * a) eq2) in
+            add_event(SUM(eq.id,(b,eq1),(a,eq2)));
+            match normalize eq with
+	      | [eq] ->
+                  let final_eq =
+                    if dark_shadow then 
+                      let delta = (a - 1) * (b - 1) in
+                      add_event(WEAKEN(eq.id,delta));
+                      {id = eq.id; kind=INEQ; body = eq.body; 
+                       constant = eq.constant - delta} 
+                    else eq
+                  in final_eq :: accu
+              | (e::_) -> failwith "Product dardk"
+              | [] -> accu)
+         accu high)
+    [] low
+
+let fourier_motzkin (_,new_eq_id,print_var) dark_shadow system =
+  let v = select_variable system in
+  let (ineq_out, ineq_low,ineq_high) = classify v system in
+  let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in
+  if !debug then display_system print_var expanded; expanded
+
+let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system =
+  if List.exists (fun e -> e.kind = DISE) system then 
+    failwith "disequation in simplify";
+  clear_history ();
+  List.iter (fun e -> add_event (HYP e)) system;
+  let system = flat_map normalize system in
+  let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in
+  let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in
+  let system = (eqs @ simp_eq,simp_ineq) in
+  let rec loop1a system =
+    let sys_ineq = banerjee new_ids system in 
+    loop1b sys_ineq 
+  and loop1b sys_ineq =
+    let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in
+    if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq) 
+  in
+  let rec loop2 system =
+    try
+      let expanded = fourier_motzkin new_ids dark_shadow system in
+      loop2 (loop1b expanded)
+    with SOLVED_SYSTEM ->
+      if !debug then display_system print_var system; system 
+  in
+  loop2 (loop1a system)
+
+let rec depend relie_on accu = function
+  | act :: l -> 
+      begin match act with
+	| DIVIDE_AND_APPROX (e,_,_,_) ->
+            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            else depend relie_on accu l
+	| EXACT_DIVIDE (e,_) ->
+            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            else depend relie_on accu l
+	| WEAKEN (e,_) ->
+            if List.mem e relie_on then depend relie_on (act::accu) l
+            else depend relie_on accu l
+	| SUM (e,(_,e1),(_,e2)) -> 
+            if List.mem e relie_on then 
+	      depend (e1.id::e2.id::relie_on) (act::accu) l
+            else 
+	      depend relie_on accu l
+	| STATE {st_new_eq=e} ->
+            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            else depend relie_on accu l
+	| HYP e ->   
+            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            else depend relie_on accu l
+	| FORGET_C _ -> depend relie_on accu l
+	| FORGET _ -> depend relie_on accu l
+	| FORGET_I _ -> depend relie_on accu l
+	| MERGE_EQ (e,e1,e2) ->
+            if List.mem e relie_on then 
+	      depend (e1.id::e2::relie_on) (act::accu) l
+            else 
+	      depend relie_on accu l
+	| NOT_EXACT_DIVIDE (e,_) -> depend (e.id::relie_on) (act::accu) l
+	| CONTRADICTION (e1,e2) -> 
+	    depend (e1.id::e2.id::relie_on) (act::accu) l
+	| CONSTANT_NOT_NUL (e,_) -> depend (e::relie_on) (act::accu) l
+	| CONSTANT_NEG (e,_) -> depend (e::relie_on) (act::accu) l
+	| CONSTANT_NUL e -> depend (e::relie_on) (act::accu) l
+	| NEGATE_CONTRADICT (e1,e2,_) -> 
+            depend (e1.id::e2.id::relie_on) (act::accu) l
+	| SPLIT_INEQ _ -> failwith "depend"
+      end
+  | [] -> relie_on, accu
+
+(*
+let depend relie_on accu trace = 
+  Printf.printf "Longueur de la trace initiale : %d\n" 
+    (trace_length trace + trace_length accu);
+  let rel',trace' = depend relie_on accu trace in
+  Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace');
+  rel',trace'
+*)
+
+let solve (new_eq_id,new_eq_var,print_var) system =
+  try let _ = simplify new_eq_id false system in failwith "no contradiction"
+  with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ())))
+      
+let negation (eqs,ineqs) =
+  let diseq,_ = filter (fun e -> e.kind = DISE) ineqs in
+  let normal = function
+    | ({body=f::_} as e) when f.c < 0 ->  negate_eq e, INVERTED
+    | e -> e,NORMAL in
+  let table = Hashtbl.create 7 in
+  List.iter (fun e -> 
+               let {body=ne;constant=c} ,kind = normal e in
+               Hashtbl.add table (ne,c) (kind,e)) diseq;
+  List.iter (fun e ->
+               if e.kind <> EQUA then pp 9999;
+               let {body=ne;constant=c},kind = normal e in
+               try 
+		 let (kind',e') = Hashtbl.find table (ne,c) in
+		 add_event (NEGATE_CONTRADICT (e,e',kind=kind'));
+		 raise UNSOLVABLE
+               with Not_found -> ()) eqs
+
+exception FULL_SOLUTION of action list * int list
+
+let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
+  clear_history ();
+  List.iter (fun e -> add_event (HYP e)) system;
+  (* Initial simplification phase *)
+  let rec loop1a system =
+    negation system;
+    let sys_ineq = banerjee new_ids system in 
+    loop1b sys_ineq 
+  and loop1b sys_ineq =
+    let dise,ine = filter (fun e -> e.kind = DISE) sys_ineq in
+    let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
+    if simp_eq = [] then dise @ simp_ineq
+    else loop1a (simp_eq,dise @ simp_ineq) 
+  in
+  let rec loop2 system =
+    try
+      let expanded = fourier_motzkin new_ids false system in
+      loop2 (loop1b expanded)
+    with SOLVED_SYSTEM -> if !debug then display_system print_var system; system 
+  in
+  let rec explode_diseq = function 
+    | (de::diseq,ineqs,expl_map) ->
+	let id1 = new_eq_id () 
+	and id2 = new_eq_id () in
+	let e1 = 
+	  {id = id1; kind=INEQ; body = de.body; constant = de.constant - 1} in
+	let e2 = 
+	  {id = id2; kind=INEQ; body = map_eq_linear (fun x -> -x) de.body; 
+           constant = - de.constant - 1} in
+	let new_sys =
+          List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys)) 
+	    ineqs @ 
+          List.map (fun (what,sys) -> ((de.id,id2,false)::what,e2::sys)) 
+	    ineqs 
+	in
+	explode_diseq (diseq,new_sys,(de.id,(de,id1,id2))::expl_map)
+    | ([],ineqs,expl_map) -> ineqs,expl_map 
+  in
+  try 
+    let system = flat_map normalize system in
+    let eqs,ineqs = filter (fun e -> e.kind=EQUA) system in
+    let dise,ine = filter (fun e -> e.kind = DISE) ineqs in
+    let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
+    let system = (eqs @ simp_eq,simp_ineq @ dise) in
+    let system' = loop1a system in
+    let diseq,ineq = filter (fun e -> e.kind = DISE) system' in
+    let first_segment = history () in
+    let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in
+    let all_solutions =
+      List.map
+        (fun (decomp,sys) -> 
+           clear_history ();
+           try let _ = loop2 sys in raise NO_CONTRADICTION
+           with UNSOLVABLE -> 
+             let relie_on,path = depend [] [] (history ()) in
+             let dc,_ = filter (fun (_,id,_) -> List.mem id relie_on) decomp in
+             let red = List.map (fun (x,_,_) -> x) dc in
+             (red,relie_on,decomp,path))
+        sys_exploded 
+    in
+    let max_count sys = 
+      let tbl = Hashtbl.create 7 in
+      let augment x = 
+        try incr (Hashtbl.find tbl x) 
+	with Not_found -> Hashtbl.add tbl x (ref 1) in
+      let eq = ref (-1) and c = ref 0 in
+      List.iter (function 
+		   | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on))
+                   | (l,_,_,_) -> List.iter augment l) sys;
+      Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl;
+      !eq 
+    in
+    let rec solve systems = 
+      try 
+	let id = max_count systems in 
+        let rec sign = function 
+	  | ((id',_,b)::l) -> if id=id' then b else sign l 
+          | [] -> failwith "solve" in
+        let s1,s2 = filter (fun (_,_,decomp,_) -> sign decomp) systems in
+        let s1' = 
+	  List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in
+        let s2' = 
+	  List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in
+        let (r1,relie1) = solve s1' 
+	and (r2,relie2) = solve s2' in
+	let (eq,id1,id2) = List.assoc id explode_map in
+	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2
+      with FULL_SOLUTION (x0,x1) -> (x0,x1) 
+    in
+    let act,relie_on = solve all_solutions in
+    snd(depend relie_on act first_segment)
+  with UNSOLVABLE -> snd (depend [] [] (history ()))
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 75bc2d1b0f..86784186fd 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -9,205 +9,510 @@
 open Const_omega
 
 
-(* \section{Utilitaires} *)
+(* \section{Useful functions and flags} *)
+(* Especially useful debugging functions *)
+let debug = ref false
 
-let debug = ref false 
+let show_goal gl =
+  if !debug then Pp.ppnl (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl
 
+let pp i = print_int i; print_newline (); flush stdout
+
+(* More readable than the prefix notation *)
 let (>>) = Tacticals.tclTHEN
 
-let index t = 
+(* [list_index t l = i] \eqv $nth l i = t \wedge \forall j < i nth l j != t$ *)
+
+let list_index t = 
   let rec loop i = function
     | (u::l) -> if u = t then i else loop (i+1) l
     | [] -> raise Not_found in
   loop 0
 
+(* [list_uniq l = filter_i (x i -> nth l (i-1) != x) l] *)
+let list_uniq l  = 
+  let rec uniq = function
+      x :: ((y :: _) as l) when x = y -> uniq l
+    | x :: l -> x :: uniq l
+    | [] -> [] in
+  uniq (List.sort compare l)
+
+(* $\forall x. mem x  (list\_union l1 l2) \eqv x \in \{l1\} \cup \{l2\}$ *)
+let list_union l1 l2 =
+  let rec loop buf = function
+      x :: r -> if List.mem x l2 then loop buf r else loop (x :: buf) r
+    | [] -> buf in
+  loop l2 l1
+
+(* $\forall x. 
+      mem \;\; x \;\; (list\_intersect\;\; l1\;\;l2) \eqv x \in \{l1\} 
+       \cap \{l2\}$ *)
+let list_intersect l1 l2 =
+  let rec loop buf = function
+      x :: r -> if List.mem x l2 then loop (x::buf) r else loop buf r
+    | [] -> buf in
+  loop [] l1
+
+(* cartesian product. Elements are lists and are concatenated.
+   $cartesian [x_1 ... x_n] [y_1 ... y_p] = [x_1 @ y_1, x_2 @ y_1 ... x_n @ y_1 , x_1 @ y_2 ... x_n @ y_p]$ *)
+
+let rec cartesien l1 l2 =
+  let rec loop = function
+      (x2 :: r2) -> List.map (fun x1 -> x1 @ x2) l1 @ loop r2
+    | [] -> [] in
+  loop l2
+
+(* remove element e from list l *)
+let list_remove e l =
+  let rec loop = function
+      x :: l -> if x = e then loop l else x :: loop l
+    | [] -> [] in
+  loop l
+
+(* equivalent of the map function but no element is added when the function
+   raises an exception (and the computation silently continues) *)
+let map_exc f = 
+  let rec loop = function 
+    (x::l) -> 
+      begin match try Some (f x) with exc -> None with
+        Some v -> v :: loop l | None -> loop l
+      end
+    | [] -> [] in
+  loop 
+
 let mkApp = Term.mkApp
 
-(* \section{Formules réifiables} *)
+(* \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 
+  connector) *)
+type direction = Left of int | Right of int
+
+(* Step to find a proposition (operators are at most binary). A list is
+   a path *)
+type occ_step = O_left | O_right | O_mono
+type occ_path = occ_step list
+
+(* chemin identifiant une proposition sous forme du nom de l'hypothèse et
+   d'une liste de pas à partir de la racine de l'hypothèse *)
+type occurence = {o_hyp : Names.identifier; o_path : occ_path}
+
+(* \subsection{refiable formulas} *)
 type oformula =
+    (* integer *)
+  | Oint of int
+    (* recognized binary and unary operations *)
   | Oplus of oformula * oformula
+  | Omult of oformula * oformula
   | Ominus of oformula * oformula
-  | Oinv of  oformula
-  | Otimes of oformula * oformula
-  | Oatom of  int
-  | Oz of int
+  | Oopp of  oformula
+    (* an atome in the environment *)
+  | Oatom of int
+    (* weird expression that cannot be translated *)
   | Oufo of oformula
 
-let rec oprint = function 
-  | Oplus(t1,t2) -> 
-      print_string "("; oprint t1; print_string "+"; 
-      oprint t2; print_string ")"
-  | Ominus(t1,t2) -> 
-      print_string "("; oprint t1; print_string "-"; 
-      oprint t2; print_string ")"
-  | Oinv t -> print_string "~"; oprint t
-  | Otimes (t1,t2) -> 
-      print_string "("; oprint t1; print_string "*"; 
-      oprint t2; print_string ")"
-  | Oatom i ->print_string "V";  print_int i
-  | Oz i -> print_int i
-  | Oufo f -> print_string "?"
-
-(* \section{Tables} *)
-
-let get_hyp env_hyp id = 
-  try index id env_hyp 
-  with Not_found -> failwith ("get_hyp " ^ string_of_int id)
-
-let tag_equation,tag_of_equation, clear_tags  =
-  let l = ref ([]:(int * Names.identifier) list) in
-  (fun id h -> l := (h,id):: !l),
-  (fun h -> try List.assoc h !l with Not_found-> failwith "tag_hypothesis"),
-  (fun () -> l := [])
-
-let add_atom t env =
-  try index t env, env
-  with Not_found ->  List.length env, (env@[t])
-
-let get_atom v env = 
-  try List.nth v env with _ -> failwith "get_atom"
-
-(* compilation des environnements *)
-
-let intern_id, intern_id_force, unintern_id, clear_intern =
-  let c = ref 0 in
-  let l = ref [] in
-  (fun t -> 
-     try List.assoc t !l 
-     with Not_found -> incr c; let v = !c in l := (t,v)::!l; v),
-  (fun t v -> l := (t,v) :: !l),
-  (fun i ->
-    let rec loop = function 
-	[] -> failwith "unintern" 
-      | ((t,j)::l) -> if i = j then t else loop l in
-    loop !l),
-  (fun () -> c := 0; l := [])
+(* 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 
+ * quantifications sont externes au langage) *)
+type oproposition = 
+    Pequa of Term.constr * oequation
+  | Ptrue 
+  | Pfalse
+  | Pnot of oproposition
+  | Por of int * oproposition * oproposition
+  | Pand of int * oproposition * oproposition
+  | Pimp of int * oproposition * oproposition
+  | Pprop of Term.constr
+
+(* Les équations ou proposiitions atomiques utiles du calcul *)
+and oequation = {
+    e_comp: comparaison;		(* comparaison *)
+    e_left: oformula;			(* formule brute gauche *)
+    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é 
+					   après normalisation *)
+    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: Omega2.afine		(* la fonction normalisée *)
+  } 
+
+(* \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
+  reified goals)
+  \item translation functions linking the decision procedure and the Coq proof
+  \end{itemize} *)
+
+type environment = {
+  (* La liste des termes non reifies constituant l'environnement global *)
+  mutable terms : Term.constr list;
+  (* La meme chose pour les propositions *)
+  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 
+   * la tactique Omega après dénombrement des variables utiles *)
+  real_indices : (int,int) Hashtbl.t;
+  mutable cnt_connectors : int;
+  equations : (int,oequation) Hashtbl.t;
+  constructors : (int, occurence) Hashtbl.t
+}
+
+(* \subsection{Solution tree}
+   Définition d'une solution trouvée par Omega sous la forme d'un identifiant,
+   d'un ensemble d'équation dont dépend la solution et d'une trace *)
+type solution = {
+  s_index : int;
+  s_equa_deps : int list;
+  s_trace : Omega2.action list }
+
+(* Arbre de solution résolvant complètement un ensemble de systèmes *)
+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
+       (typ. disjonction). Le premier argument
+       est l'identifiant du connecteur *)
+  | Tree of int * solution_tree * 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 = 
+    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 *)  
+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; 
+  real_indices = Hashtbl.create 7;
+  equations = Hashtbl.create 7;
+  constructors = Hashtbl.create 7;
+}
+
+(* Génération d'un nom d'équation *)
+let new_eq_id env =
+   env.cnt_connectors <- env.cnt_connectors + 1; 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 
+
+(* Affichage de l'environnement de réification (termes et propositions) *)
+let print_env_reification env = 
+  let rec loop c i = function
+      [] -> Printf.printf "===============================\n\n"
+    | t :: l -> 
+	Printf.printf "(%c%02d) : " c i;
+	Pp.ppnl (Printer.prterm t);
+	Pp.flush_all ();
+	loop c (i+1) l in
+  Printf.printf "PROPOSITIONS :\n\n"; loop 'P' 0 env.props;
+  Printf.printf "TERMES :\n\n"; loop 'V' 0 env.terms
+
+
+(* \subsection{Gestion des environnements de variable pour Omega} *)
+(* generation d'identifiant d'equation pour Omega *)
+let new_omega_id = let cpt = ref 0 in function () -> incr cpt; !cpt
+(* Affichage des variables d'un système *)
+let display_omega_id i = Printf.sprintf "O%d" i
+(* Recherche la variable codant un terme pour Omega et crée la variable dans
+   l'environnement si il n'existe pas. Cas ou la variable dans Omega représente
+   le terme d'un monome (le plus souvent un atome) *)
+
+let intern_omega env t =
+  begin try List.assoc t env.om_vars
+  with Not_found -> 
+    let v = new_omega_id () in 
+    env.om_vars <- (t,v) :: env.om_vars; v
+  end
 
-(* Le poids d'un terme : fondamental pour classer les variables *)
+(* Ajout forcé d'un lien entre un terme et une variable Omega. Cas ou la
+   variable est crée par Omega et ou il faut la lier après coup a un atome
+   réifié introduit de force *)
+let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars
 
-let rec weight = function
-  | Oatom _ as c -> intern_id c
-  | Oz _ -> -1
-  | Oinv c -> weight c
-  | Otimes(c,_) -> weight c
+(* Récupère le terme associé à une variable *)
+let unintern_omega env id =
+  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} 
+   Gestion des environnements de traduction entre termes des constructions
+   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. *)
+
+let add_reified_atom t env =
+  try list_index t env.terms
+  with Not_found ->
+    let i = List.length env.terms in
+    env.terms <- env.terms @ [t]; i
+
+let get_reified_atom env = 
+  try List.nth env.terms with _ -> failwith "get_reified_atom"
+
+(* \subsection{Gestion de l'environnement de proposition pour Omega} *)
+(* ajout d'une proposition *)
+let add_prop env t =
+  try list_index t env.props
+  with Not_found ->
+    let i = List.length env.props in  env.props <- env.props @ [t]; i
+
+(* accès a une proposition *)
+let get_prop v env = try List.nth v env with _ -> failwith "get_prop"
+
+(* \subsection{Gestion du nommage des équations} *)
+(* Ajout d'une equation dans l'environnement de reification *)
+let add_equation env e =
+  let id = e.e_omega.Omega2.id in
+  try let _ = Hashtbl.find env.equations id in ()
+  with Not_found -> Hashtbl.add env.equations id e
+
+(* accès a une equation *)
+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 
+  | Oint n -> Printf.fprintf ch "%d" 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 
+  | 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 
+	  Eq -> "=" | Leq -> "=<" | Geq -> ">="
+	| Gt -> ">" | Lt -> "<" | Neq -> "!=" in
+      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  
+  | Pprop c -> Printf.fprintf ch "Prop"
+
+let rec weight env = function
+  | Oint _ -> -1
+  | Oopp c -> weight env c
+  | Omult(c,_) -> weight env c
   | Oplus _ -> failwith "weight"
   | Ominus _ -> failwith "weight minus"
   | Oufo _ -> -1
+  | Oatom _ as c -> (intern_omega env c)
 
-(* \section{Passage entre oformules et 
-               représentation interne de Omega} *)
+(* \section{Passage entre oformules et représentation interne de Omega} *)
 
 (* \subsection{Oformula vers Omega} *)
 
-let compile name kind = 
+let omega_of_oformula env kind = 
   let rec loop accu = function
-    | Oplus(Otimes(v,Oz n),r) -> 
-	loop ({Omega.v=intern_id v; Omega.c=n} :: accu) r
-    | Oz n ->
-	let id = Omega.new_id () in
-	tag_equation name id;
-	{Omega.kind = kind; Omega.body = List.rev accu; 
-	 Omega.constant = n; Omega.id = id}
-    | t -> print_string "CO"; oprint t; failwith "compile_equation" in
+    | Oplus(Omult(v,Oint n),r) -> 
+	loop ({Omega2.v=intern_omega env v; Omega2.c=n} :: accu) r
+    | Oint n ->
+	let id = new_omega_id () in
+	(*i tag_equation name id; i*)
+	{Omega2.kind = kind; Omega2.body = List.rev accu; 
+	 Omega2.constant = n; Omega2.id = id}
+    | t -> print_string "CO"; oprint stdout t; failwith "compile_equation" in
   loop []
 
 (* \subsection{Omega vers Oformula} *)
 
-let rec decompile af = 
+let reified_of_atom env i =
+  try Hashtbl.find env.real_indices 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
+
+let rec oformula_of_omega env af = 
   let rec loop = function
-    | ({Omega.v=v; Omega.c=n}::r) -> Oplus(Otimes(unintern_id v,Oz n),loop r) 
-    | [] -> Oz af.Omega.constant in
-  loop af.Omega.body
+    | ({Omega2.v=v; Omega2.c=n}::r) ->
+	Oplus(Omult(unintern_omega env v,Oint n),loop r)
+    | [] -> Oint af.Omega2.constant in
+  loop af.Omega2.body
+
+let app f v = mkApp(Lazy.force f,v)
 
 (* \subsection{Oformula vers COQ reel} *)
 
 let rec coq_of_formula env t =
   let rec loop = function
-  | Oplus (t1,t2) -> mkApp(Lazy.force coq_Zplus, [| loop t1; loop t2 |])
-  | Oinv t -> mkApp(Lazy.force coq_Zopp, [| loop t |])
-  | Otimes(t1,t2) -> mkApp(Lazy.force coq_Zmult, [| loop t1; loop t2 |])
-  | Oz v ->  mk_Z v
+  | Oplus (t1,t2) -> app coq_Zplus [| loop t1; loop t2 |]
+  | Oopp t -> app coq_Zopp [| loop t |]
+  | Omult(t1,t2) -> app coq_Zmult [| loop t1; loop t2 |]
+  | Oint v ->   mk_Z v
   | Oufo t -> loop t
-  | Oatom i -> get_atom env i
-  | Ominus(t1,t2) -> mkApp(Lazy.force coq_Zminus, [| loop t1; loop t2 |]) in
+  | Oatom var ->
+      (* attention ne traite pas les nouvelles variables si on ne les
+       * met pas dans env.term *)
+      get_reified_atom env var
+  | Ominus(t1,t2) -> app coq_Zminus [| loop t1; loop t2 |] in
   loop t
 
 (* \subsection{Oformula vers COQ reifié} *)
 
-let rec val_of_formula = function
+let rec reified_of_formula env = function
   | Oplus (t1,t2) ->
-      mkApp(Lazy.force coq_t_plus, [| val_of_formula t1; val_of_formula t2 |])
-  | Oinv t ->
-      mkApp(Lazy.force coq_t_opp, [| val_of_formula t |])
-  | Otimes(t1,t2) ->
-      mkApp(Lazy.force coq_t_mult, [| val_of_formula t1; val_of_formula t2 |])
-  | Oz v ->  mkApp (Lazy.force coq_t_nat, [| mk_Z v |])
-  | Oufo t -> val_of_formula t
-  | Oatom i -> mkApp(Lazy.force coq_t_var, [| mk_nat i |])
+      app coq_t_plus [| reified_of_formula env t1; reified_of_formula env t2 |]
+  | Oopp t ->
+      app coq_t_opp [| reified_of_formula env t |]
+  | Omult(t1,t2) ->
+      app coq_t_mult [| reified_of_formula env t1; reified_of_formula env t2 |]
+  | Oint v ->  app coq_t_int [| mk_Z v |]
+  | Oufo t -> reified_of_formula env t
+  | Oatom i -> app coq_t_var [| mk_nat (reified_of_atom env i) |]
   | Ominus(t1,t2) ->
-      mkApp(Lazy.force coq_t_minus, [| val_of_formula t1; val_of_formula t2 |])
+      app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |]
+
+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 }) -> 
+      app coq_p_eq [| reified_of_formula env t1; reified_of_formula env 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 }) -> 
+      app coq_p_geq [| reified_of_formula env t1; reified_of_formula env 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 }) ->  
+      app coq_p_lt [| reified_of_formula env t1; reified_of_formula env 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 -> 
+      app coq_p_not [| reified_of_proposition env t |]
+  | Por (_,t1,t2) -> 
+      app coq_p_or
+	[| reified_of_proposition env t1; reified_of_proposition env t2 |]
+  | Pand(_,t1,t2) -> 
+      app coq_p_and
+	[| reified_of_proposition env t1; reified_of_proposition env 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 
+  with e -> pprint stderr f; raise e end
 
 (* \subsection{Omega vers COQ réifié} *)
 
-let val_of body constant = 
+let reified_of_omega env body constant = 
   let coeff_constant = 
-    mkApp(Lazy.force coq_t_nat, [| mk_Z constant |]) in
-  let mk_coeff {Omega.c=c; Omega.v=v} t =
-    let coef = mkApp(Lazy.force coq_t_mult,
-		     [|val_of_formula (unintern_id v );
-		       mkApp(Lazy.force coq_t_nat, [| mk_Z c |]) |]) in
-    mkApp(Lazy.force coq_t_plus, [|coef; t |]) in
+    app coq_t_int [| mk_Z constant |] in
+  let mk_coeff {Omega2.c=c; Omega2.v=v} t =
+    let coef = 
+      app coq_t_mult 
+	[| reified_of_formula env (unintern_omega env v); 
+	   app coq_t_int [| mk_Z 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 -> 
+    Omega2.display_eq display_omega_id (body,c); raise e 
+  end
+
 (* \section{Opérations sur les équations}
 Ces fonctions préparent les traces utilisées par la tactique réfléchie
 pour faire des opérations de normalisation sur les équations.  *)
 
+(* \subsection{Extractions des variables d'une équation} *)
+(* Extraction des variables d'une équation *)
+
+let rec vars_of_formula = function
+  | Oint _ -> []
+  | Oplus (e1,e2)  -> (vars_of_formula e1) @ (vars_of_formula e2)
+  | Omult (e1,e2)  -> (vars_of_formula e1) @ (vars_of_formula e2)
+  | Ominus (e1,e2) -> (vars_of_formula e1) @ (vars_of_formula e2)
+  | Oopp e -> (vars_of_formula e)
+  | Oatom i -> [i]
+  | Oufo _ -> []
+
+let vars_of_equations l =
+  let rec loop = function
+      e :: l -> vars_of_formula e.e_left @ vars_of_formula e.e_right @ loop l
+    | [] -> [] in
+  list_uniq (List.sort compare (loop l))
+
 (* \subsection{Multiplication par un scalaire} *)
+
 let rec scalar n = function
    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], 
      Oplus(t1',t2')
- | Oinv t ->
-     do_list [Lazy.force coq_c_mult_opp_left], Otimes(t,Oz(-n))
- | Otimes(t1,Oz x) -> 
-     do_list [Lazy.force coq_c_mult_assoc_reduced], Otimes(t1,Oz (n*x))
- | Otimes(t1,t2) -> 
+ | Oopp t ->
+     do_list [Lazy.force coq_c_mult_opp_left], Omult(t,Oint(-n))
+ | Omult(t1,Oint x) -> 
+     do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x))
+ | Omult(t1,t2) -> 
      Util.error "Omega: Can't solve a goal with non-linear products"
- | (Oatom _ as t) -> do_list [], Otimes(t,Oz n)
- | Oz i -> do_list [Lazy.force coq_c_reduce],Oz(n*i)
- | (Oufo _ as t)-> do_list [], Oufo (Otimes(t,Oz n))
+ | (Oatom _ as t) -> do_list [], Omult(t,Oint n)
+ | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i)
+ | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n))
  | Ominus _ -> failwith "scalar minus"
 
 (* \subsection{Propagation de l'inversion} *)
+
 let rec negate = function
    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')
- | Oinv t ->
+ | Oopp t ->
      do_list [Lazy.force coq_c_opp_opp], t
- | Otimes(t1,Oz x) -> 
-     do_list [Lazy.force coq_c_opp_mult_r], Otimes(t1,Oz (-x))
- | Otimes(t1,t2) -> 
+ | Omult(t1,Oint x) -> 
+     do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (-x))
+ | 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], Otimes(t,Oz(-1))
- | Oz i -> do_list [Lazy.force coq_c_reduce] ,Oz(-i)
- | Oufo c -> do_list [], Oufo (Oinv c)
+     do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(-1))
+ | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(-i)
+ | Oufo c -> do_list [], Oufo (Oopp c)
  | Ominus _ -> failwith "negate minus"
 
 let rec norm l = (List.length l)
 
 (* \subsection{Mélange (fusion) de deux équations} *)
-
+(* \subsubsection{Version avec coefficients} *)
 let rec shuffle_path k1 e1 k2 e2 =
   let rec loop = function
-      (({Omega.c=c1;Omega.v=v1}::l1) as l1'),
-      (({Omega.c=c2;Omega.v=v2}::l2) as l2') ->
+      (({Omega2.c=c1;Omega2.v=v1}::l1) as l1'),
+      (({Omega2.c=c2;Omega2.v=v2}::l2) as l2') ->
 	if v1 = v2 then
           if k1*c1 + k2 * c2 = 0 then (
             Lazy.force coq_f_cancel :: loop (l1,l2))
@@ -217,106 +522,109 @@ 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))
-    | ({Omega.c=c1;Omega.v=v1}::l1), [] -> 
+    | ({Omega2.c=c1;Omega2.v=v1}::l1), [] -> 
 	  Lazy.force coq_f_left :: loop(l1,[])
-    | [],({Omega.c=c2;Omega.v=v2}::l2) -> 
+    | [],({Omega2.c=c2;Omega2.v=v2}::l2) -> 
 	  Lazy.force coq_f_right :: loop([],l2)
     | [],[] -> flush stdout; [] in
   mk_shuffle_list (loop (e1,e2))
 
-let rec shuffle (t1,t2) = 
+(* \subsubsection{Version sans coefficients} *)
+let rec shuffle env (t1,t2) = 
   match t1,t2 with
     Oplus(l1,r1), Oplus(l2,r2) ->
-      if weight l1 > weight l2 then 
-	let l_action,t' = shuffle (r1,t2) in
+      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 
-	let l_action,t' = shuffle (t1,r2) in
+	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 -> 
-      if weight l1 > weight t2 then
-        let (l_action,t') = shuffle  (r1,t2) in
+      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_sym], Oplus(t2,t1)
   | t1,Oplus(l2,r2) -> 
-      if weight l2 > weight t1 then
-        let (l_action,t') = shuffle (t1,r2) in
+      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')
       else do_list [],Oplus(t1,t2)
-  | Oz t1,Oz t2 ->
-      do_list [Lazy.force coq_c_reduce], Oz(t1+t2)
+  | Oint t1,Oint t2 ->
+      do_list [Lazy.force coq_c_reduce], Oint(t1+t2)
   | t1,t2 ->
-      if weight t1 < weight t2 then
+      if weight env t1 < weight env t2 then
 	do_list [Lazy.force coq_c_plus_sym], Oplus(t2,t1)
       else do_list [],Oplus(t1,t2)
 
 (* \subsection{Fusion avec réduction} *)
+
 let shrink_pair f1 f2 =
   begin match f1,f2 with
      Oatom v,Oatom _ -> 
-       Lazy.force coq_c_red1, Otimes(Oatom v,Oz 2)
-   | Oatom v, Otimes(_,c2) -> 
-       Lazy.force coq_c_red2, Otimes(Oatom v,Oplus(c2,Oz 1))
-   | Otimes (v1,c1),Oatom v -> 
-       Lazy.force coq_c_red3, Otimes(Oatom v,Oplus(c1,Oz 1))
-   | Otimes (Oatom v,c1),Otimes (v2,c2) ->
-       Lazy.force coq_c_red4, Otimes(Oatom v,Oplus(c1,c2))
+       Lazy.force coq_c_red1, Omult(Oatom v,Oint 2)
+   | Oatom v, Omult(_,c2) -> 
+       Lazy.force coq_c_red2, Omult(Oatom v,Oplus(c2,Oint 1))
+   | Omult (v1,c1),Oatom v -> 
+       Lazy.force coq_c_red3, Omult(Oatom v,Oplus(c1,Oint 1))
+   | Omult (Oatom v,c1),Omult (v2,c2) ->
+       Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2))
    | t1,t2 -> 
-       oprint t1; print_newline (); oprint t2; print_newline (); 
+       oprint stdout t1; print_newline (); oprint stdout t2; print_newline (); 
        flush Pervasives.stdout; Util.error "shrink.1"
   end
 
 (* \subsection{Calcul d'une sous formule constante} *)
+
 let reduce_factor = function
    Oatom v ->
-     let r = Otimes(Oatom v,Oz 1) in
+     let r = Omult(Oatom v,Oint 1) in
        [Lazy.force coq_c_red0],r
-  | Otimes(Oatom v,Oz n) as f -> [],f
-  | Otimes(Oatom v,c) ->
+  | Omult(Oatom v,Oint n) as f -> [],f
+  | Omult(Oatom v,c) ->
       let rec compute = function
-          Oz n -> n
+          Oint n -> n
 	| Oplus(t1,t2) -> compute t1 + compute t2 
 	| _ -> Util.error "condense.1" in
-	[Lazy.force coq_c_reduce], Otimes(Oatom v,Oz(compute c))
+	[Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c))
   | t -> Util.error "reduce_factor.1"
 
 (* \subsection{Réordonancement} *)
 
-let rec condense = function
+let rec condense env = function
     Oplus(f1,(Oplus(f2,r) as t)) ->
-      if weight f1 = weight f2 then begin
+      if weight env f1 = weight env f2 then begin
 	let shrink_tac,t = shrink_pair f1 f2 in
 	let assoc_tac = Lazy.force coq_c_plus_assoc_l in
-	let tac_list,t' = condense (Oplus(t,r)) in
+	let tac_list,t' = condense env (Oplus(t,r)) in
 	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 t in 
+	let tac',t' = condense env t in 
 	[do_both (do_list tac) (do_list tac')], Oplus(f,t') 
       end
-  | (Oplus(f1,Oz n) as t) -> 
+  | (Oplus(f1,Oint n) as t) -> 
       let tac,f1' = reduce_factor f1 in 
-      [do_left (do_list tac)],Oplus(f1',Oz n)
+      [do_left (do_list tac)],Oplus(f1',Oint n)
   | Oplus(f1,f2) -> 
-      if weight f1 = weight f2 then begin
+      if weight env f1 = weight env f2 then begin
 	let tac_shrink,t = shrink_pair f1 f2 in
-	let tac,t' = condense t 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 f2 in 
+	let tac',t' = condense env f2 in 
 	[do_both (do_list tac) (do_list tac')],Oplus(f,t') 
       end
-  | (Oz _ as t)-> [],t
+  | (Oint _ as t)-> [],t
   | t -> 
       let tac,t' = reduce_factor t in
-      let final = Oplus(t',Oz 0) in
+      let final = Oplus(t',Oint 0) in
       tac @ [Lazy.force coq_c_red6], final
 
 (* \subsection{Elimination des zéros} *)
 
 let rec clear_zero = function
-   Oplus(Otimes(Oatom v,Oz 0),r) ->
+   Oplus(Omult(Oatom v,Oint 0),r) ->
      let tac',t = clear_zero r in
      Lazy.force coq_c_red5 :: tac',t
   | Oplus(f,r) -> 
@@ -324,519 +632,673 @@ let rec clear_zero = function
       (if tac = [] then [] else [do_right (do_list tac)]),Oplus(f,t)
   | t -> [],t;;
 
-(* \section{Transformation des hypothèses} *)
+(* \subsection{Transformation des hypothèses} *)
 
-let rec reduce = function
+let rec reduce env = function
     Oplus(t1,t2) ->
-      let t1', trace1 = reduce t1 in
-      let t2', trace2 = reduce t2 in
-      let trace3,t' = shuffle (t1',t2') in
+      let t1', trace1 = reduce env t1 in
+      let t2', trace2 = reduce env t2 in
+      let trace3,t' = shuffle env (t1',t2') in
       t', do_list [do_both trace1 trace2; trace3]
   | Ominus(t1,t2) ->
-      let t,trace = reduce (Oplus(t1, Oinv t2)) in
+      let t,trace = reduce env (Oplus(t1, Oopp t2)) in
       t, do_list [Lazy.force coq_c_minus; trace]
-  | Otimes(t1,t2) as t ->
-      let t1', trace1 = reduce t1 in
-      let t2', trace2 = reduce t2 in
+  | Omult(t1,t2) as t ->
+      let t1', trace1 = reduce env t1 in
+      let t2', trace2 = reduce env t2 in
       begin match t1',t2' with
-      | (_, Oz n) ->
+      | (_, Oint n) ->
 	  let tac,t' = scalar n t1' in
 	  t', do_list [do_both trace1 trace2; tac]
-      | (Oz n,_) ->
+      | (Oint n,_) ->
 	  let tac,t' = scalar n t2' in
 	  t', do_list [do_both trace1 trace2; Lazy.force coq_c_mult_sym; tac]
       | _ -> Oufo t, Lazy.force coq_c_nop
       end
-  | Oinv t ->
-      let t',trace = reduce  t in
+  | Oopp t ->
+      let t',trace = reduce env  t in
       let trace',t'' = negate t' in
       t'', do_list [do_left trace; trace']
-  | (Oz _ | Oatom _ | Oufo _) as t -> t, Lazy.force coq_c_nop
+  | (Oint _ | Oatom _ | Oufo _) as t -> t, Lazy.force coq_c_nop
+
+let normalize_linear_term env t =
+  let t1,trace1 = reduce env t in
+  let trace2,t2 = condense env t1 in
+  let trace3,t3 = clear_zero t2 in
+  do_list [trace1; do_list trace2; do_list trace3], t3
 
-let rec ocompile 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 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; 
+      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
+    | Eq  -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.EQUA
+    | Neq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.DISE
+    | Leq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oopp o1)) Omega2.INEQ
+    | Geq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.INEQ
+    | Lt  ->
+        mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o2,Oint (-1)),Oopp o1))
+	  Omega2.INEQ
+    | Gt ->
+        mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o1,Oint (-1)),Oopp o2)) 
+	  Omega2.INEQ
+  with e when Logic.catchable_exception e -> raise e
+
+(* \section{Compilation des hypothèses} *)
+
+let rec oformula_of_constr env t =
   try match destructurate t with
-  | Kapp("Zplus",[t1;t2]) ->
-      let t1',env1 = ocompile env  t1 in
-      let t2',env2 = ocompile env1 t2 in
-      (Oplus (t1',t2'), env2)
-  | Kapp("Zminus",[t1;t2]) ->
-      let t1',env1 = ocompile env  t1 in
-      let t2',env2 = ocompile env1 t2 in
-      (Ominus (t1',t2'), env2)
-  | Kapp("Zmult",[t1;t2]) ->
-      let t1',env1 = ocompile env t1 in
-      let t2',env2 = ocompile env1 t2 in
-      (Otimes (t1',t2'), env2)
-  | Kapp("Zs",[t]) ->  
-      let t',env = ocompile env  t in
-       (Oplus (t',Oz(1)), env)
+  | Kapp("Zplus",[t1;t2]) -> binop env (fun x y -> Oplus(x,y)) t1 t2
+  | Kapp("Zminus",[t1;t2]) ->binop env (fun x y -> Ominus(x,y)) t1 t2
+  | Kapp("Zmult",[t1;t2]) ->binop env (fun x y -> Omult(x,y)) t1 t2
   | Kapp(("POS"|"NEG"|"ZERO"),_) -> 
-      begin try (Oz(recognize_number t),env) 
-      with _ -> 
-	let v,env' = add_atom t env in Oatom v, env'
-      end
-  | Kvar s ->
-      let v,env' = add_atom t env in Oatom v, env'
-  | Kapp("Zopp",[t]) ->
-      let t',env1 = ocompile env t in Oinv t', env1
+      begin try Oint(recognize_number t)
+      with _ -> Oatom (add_reified_atom t env) end
   | _ -> 
-      let v,env' = add_atom t env in Oatom(v), env'
+      Oatom (add_reified_atom t env)
   with e when Logic.catchable_exception e ->
-    let v,env' = add_atom t env in Oatom(v), env'
-
-(*i  | Kapp("Zs",[t1]) ->
-    | Kapp("inject_nat",[t']) -> i*)
-
-let normalize_equation t =
-  let t1,trace1 = reduce t in
-  let trace2,t2 = condense t1 in
-  let trace3,t3 = clear_zero t2 in
-  do_list [trace1; do_list trace2; do_list trace3], t3
+    Oatom (add_reified_atom t env)
+
+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) 
+             add_to_depends neg1 gl c t1 t2 =
+  let i = new_eq_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' = 
+    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
+  (* On numérote le connecteur dans l'environnement. *)
+  c i t1' t2'
+
+and mk_equation env ctxt c connector t1 t2 =
+  let t1' = oformula_of_constr env t1 in
+  let t2' = oformula_of_constr env t2 in
+  (* On ajoute l'equation dans l'environnement. *)
+  let omega = normalize_equation env ctxt (connector,t1',t2') in
+  add_equation env omega;
+  Pequa (c,omega)
+
+and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = 
+  try match destructurate c with
+    | Kapp("eq",[typ;t1;t2]) 
+      when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) ->
+         mk_equation env ctxt c Eq t1 t2
+    | Kapp("Zne",[t1;t2]) -> 
+	mk_equation env ctxt c Neq t1 t2
+    | Kapp("Zle",[t1;t2]) -> 
+	mk_equation env ctxt c Leq t1 t2
+    | Kapp("Zlt",[t1;t2]) -> 
+	mk_equation env ctxt c Lt t1 t2
+    | Kapp("Zge",[t1;t2]) -> 
+	mk_equation env ctxt c Geq t1 t2
+    | Kapp("Zgt",[t1;t2]) -> 
+	mk_equation env ctxt c Gt t1 t2
+    | Kapp("True",[]) -> Ptrue
+    | Kapp("False",[]) -> Pfalse
+    | Kapp("not",[t]) ->
+       let t' = 
+	 oproposition_of_constr 
+	   env (not negated, depends, origin,(O_mono::path)) gl t in 
+       Pnot t'
+    | Kapp("or",[t1;t2]) ->  
+	binprop env ctxt (not negated) negated gl (fun i x y -> Por(i,x,y)) t1 t2
+    | Kapp("and",[t1;t2]) ->
+	binprop env ctxt negated negated gl
+	  (fun i x y -> Pand(i,x,y)) t1 t2
+    | Kimp(t1,t2) ->
+	binprop env ctxt (not negated) (not negated) gl 
+	  (fun i x y -> Pimp(i,x,y)) t1 t2
+    | _ -> Pprop c
+  with e when Logic.catchable_exception e -> Pprop c
+
+(* Destructuration des hypothèses et de la conclusion *)
+
+let reify_gl env gl =
+  let concl = Tacmach.pf_concl gl in
+  let t_concl =
+    Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in
+  if !debug then begin
+    Printf.printf "CONCL: "; pprint stdout t_concl; Printf.printf "\n"
+  end;
+  let rec loop = function
+      (i,t) :: lhyps ->
+	let t' = oproposition_of_constr env (false,[],i,[]) gl t in
+	if !debug then begin
+	  Printf.printf "%s: " (Names.string_of_id i);
+	  pprint stdout t';
+	  Printf.printf "\n"
+	end;
+	(i,t') :: loop lhyps
+    | [] -> 
+	if !debug then print_env_reification env; 
+	[] in
+  let t_lhyps = loop (Tacmach.pf_hyps_types gl) in
+  (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 = 
+	destructurate_pos_hyp orig list_equations (i::list_depends) t1 in
+      let s2 = 
+	destructurate_pos_hyp orig list_equations (i::list_depends) t2 in
+      s1 @ s2
+  | Pand(i,t1,t2) -> 
+      let list_s1 =
+	destructurate_pos_hyp orig list_equations (list_depends) t1 in
+      let rec loop = function 
+	  le1 :: ll -> destructurate_pos_hyp orig le1 list_depends t2 @ loop ll
+	| [] -> [] in
+      loop list_s1
+  | Pimp(i,t1,t2) -> 
+      let s1 =
+	destructurate_neg_hyp orig list_equations (i::list_depends) t1 in
+      let s2 =
+	destructurate_pos_hyp orig list_equations (i::list_depends) t2 in
+      s1 @ s2
+
+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) -> 
+      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) -> 
+      let list_s1 =
+	destructurate_neg_hyp orig list_equations list_depends t1 in
+      let rec loop = function 
+	  le1 :: ll -> destructurate_neg_hyp orig le1 list_depends t2 @ loop ll
+	| [] -> [] in
+      loop list_s1
+  | Pimp(_,t1,t2) -> 
+      let list_s1 =
+	destructurate_pos_hyp orig list_equations list_depends t1 in
+      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 -> 
+	let l_syst1 = destructurate_pos_hyp i []  [] t in
+	let l_syst2 = loop l in
+	cartesien l_syst1 l_syst2
+    | [] -> [[]] in
+  loop syst
+
+(* \subsection{Affichage d'un système d'équation} *)
+
+(* Affichage des dépendances de système *)
+let display_depend = function
+    Left i -> Printf.printf " L%d" i 
+  | Right i -> Printf.printf " R%d" i
+
+let display_systems syst_list = 
+  let display_omega om_e = 
+    Printf.printf "%d : %a %s 0\n"
+      om_e.Omega2.id
+      (fun _ -> Omega2.display_eq display_omega_id) 
+      (om_e.Omega2.body, om_e.Omega2.constant)
+      (Omega2.operator_of_eq om_e.Omega2.kind) in
+
+  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:"; 
+    List.iter display_depend oformula_eq.e_depends;
+    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));
+    Printf.printf "\n  Origin: %s -- Negated : %s\n"
+      (Names.string_of_id oformula_eq.e_origin.o_hyp)
+      (if oformula_eq.e_negated then "yes" else "false") in
+
+  let display_system syst =
+    Printf.printf "=SYSTEME==================================\n";
+    List.iter display_equation syst in
+  List.iter display_system syst_list
+
+(* Extraction des prédicats utilisées dans une trace. Permet ensuite le
+   calcul des hypothèses *)
+
+let rec hyps_used_in_trace = function
+  | act :: l -> 
+      begin match act with
+	| Omega2.HYP e -> e.Omega2.id :: hyps_used_in_trace l
+	| Omega2.SPLIT_INEQ (_,(_,act1),(_,act2)) -> 
+	    hyps_used_in_trace act1 @ hyps_used_in_trace act2
+	| _ -> hyps_used_in_trace l
+      end
+  | [] -> []
+
+(* Extraction des variables déclarées dans une équation. Permet ensuite
+   de les déclarer dans l'environnement de la procédure réflexive et
+   éviter les créations de variable au vol *)
+
+let rec variable_stated_in_trace = function
+  | act :: l -> 
+      begin match act with
+	| Omega2.STATE action ->
+	    (*i nlle_equa: afine, def: afine, eq_orig: afine, i*)
+            (*i coef: int, var:int                            i*)
+	    action :: variable_stated_in_trace l
+	| Omega2.SPLIT_INEQ (_,(_,act1),(_,act2)) -> 
+	    variable_stated_in_trace act1 @ variable_stated_in_trace act2
+	| _ -> variable_stated_in_trace l
+      end
+  | [] -> []
+;;
 
-let destructure_omega gl (trace_norm, system, env) (id,c) = 
-  let mk_step t1 t2 f kind coq_t_oper =
-       let o1,env1 = ocompile env t1 in
-       let o2,env2 = ocompile env1 t2 in
-       let t = f o1 o2 in
-       let trace, oterm = normalize_equation t in
-       let equa = compile id kind oterm in
-       let tterm =
-	 mkApp (Lazy.force coq_t_oper,
-		[| val_of_formula o1; val_of_formula o2 |]) in
-       ((id,(trace,tterm)) :: trace_norm), (equa :: system), env2 in
+let add_stated_equations env tree = 
+  let rec loop = function
+      Tree(_,t1,t2) -> 
+	list_union (loop t1) (loop t2)
+    | Leaf s -> variable_stated_in_trace s.s_trace in
+  (* Il faut trier les variables par ordre d'introduction pour ne pas risquer
+     de définir dans le mauvais ordre *)
+  let stated_equations = 
+    List.sort (fun x y -> x.Omega2.st_var - y.Omega2.st_var) (loop tree) in
+  let add_env st = 
+    (* On retransforme la définition de v en formule reifiée *)
+    let v_def = oformula_of_omega env st.Omega2.st_def in
+    (* 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
+    (* Le terme qu'il va falloir introduire *)
+    let term_to_generalize = app coq_refl_equal [|Lazy.force coq_Z; coq_v|] in
+    (* sa représentation sous forme d'équation mais non réifié car on n'a pas
+     * 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.Omega2.st_var; 
+    (v, term_to_generalize,term_to_reify,st.Omega2.st_def.Omega2.id) in
+ List.map add_env stated_equations
+
+(* Calcule la liste des éclatements à réaliser sur les hypothèses 
+   nécessaires pour extraire une liste d'équations donnée *)
+
+let rec get_eclatement env = function
+    i :: r -> 
+      let l = try (get_equation env i).e_depends with Not_found -> [] in
+      list_union l (get_eclatement env r)
+  | [] -> []
+
+let select_smaller l = 
+  let comp (_,x) (_,y) = 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) -> 
+	if List.mem x required then select l
+	else if List.mem (barre x) required then raise Exit 
+	else x :: select l
+    | [] -> [] in
+  map_exc (function (sol,splits) -> (sol,select splits)) systems
+
+let rec equas_of_solution_tree = function
+    Tree(_,t1,t2) -> 
+      list_union (equas_of_solution_tree t1) (equas_of_solution_tree t2)
+  | Leaf s -> s.s_equa_deps
+
+
+let really_useful_prop l_equa c =
+  let rec real_of = function
+      Pequa(t,_) -> t
+    | Ptrue ->  app  coq_true [||]
+    | Pfalse -> app  coq_false [||]
+    | Pnot t1 -> app coq_not [|real_of t1|]
+    | Por(_,t1,t2) -> app coq_or [|real_of t1; real_of t2|]
+    | Pand(_,t1,t2) -> app coq_and [|real_of t1; real_of t2|]
+    (* 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 
+      Pequa(_,e) ->
+	if List.mem e.e_omega.Omega2.id l_equa then Some c else None
+    | Ptrue -> None
+    | Pfalse -> None
+    | 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 = 
+    begin match loop t1, loop t2 with
+      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'))
+    end in
+  match loop c with
+    None -> Pprop (real_of c)
+  | Some t -> t
+
+let rec display_solution_tree ch = function
+    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 
+	display_solution_tree t1 display_solution_tree t2
+
+let rec solve_with_constraints all_solutions path = 
+  let rec build_tree sol buf = function
+      [] -> Leaf sol
+    | (Left i :: remainder) -> 
+	Tree(i,
+	     build_tree sol (Left i :: buf) remainder, 
+	     solve_with_constraints all_solutions (List.rev(Right i :: buf)))
+    | (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" 
+	(List.length weighted) (List.length all_solutions);
+      List.iter display_depend path; raise e in
+  build_tree winner_sol (List.rev path) winner_deps 
+
+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)
+    | _ -> None in
+  let rec loop_id i = function
+      CCHyp{o_hyp=id';o_path=p'} :: l when id = id' ->
+	begin match loop_path (p',p) with
+	  Some r -> i,r
+	| None -> loop_id (i+1) l
+	end
+    | _ :: l -> loop_id (i+1) l
+    | [] -> failwith "find_path" in
+  loop_id 0 env
+
+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)
 
-  try match destructurate c with
-    | Kapp("eq",[typ;t1;t2]) when destructurate (Tacmach.pf_nf gl typ) = 
-	                          Kapp("Z",[]) ->
-         mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oinv o2)) Omega.EQUA coq_t_equal
-    | Kapp("Zne",[t1;t2]) ->
-        mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oinv o2)) Omega.DISE coq_t_neq
-    | Kapp("Zle",[t1;t2]) ->
-        mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oinv o1)) Omega.INEQ coq_t_leq
-    | Kapp("Zlt",[t1;t2]) ->
-        mk_step t1 t2 
-	  (fun o1 o2 -> Oplus (Oplus(o2,Oz (-1)),Oinv o1)) Omega.INEQ coq_t_lt
-    | Kapp("Zge",[t1;t2]) ->
-        mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oinv o2)) Omega.INEQ coq_t_geq
-    | Kapp("Zgt",[t1;t2]) ->
-        mk_step t1 t2 
-	  (fun o1 o2 -> Oplus (Oplus(o1,Oz (-1)),Oinv o2)) Omega.INEQ coq_t_gt
-    | _ -> trace_norm, system, env
-  with e when Logic.catchable_exception e -> trace_norm, system, env
 
 (* \section{Rejouer l'historique} *)
 
-let replay_history env_hyp =
+let get_hyp env_hyp i =
+  try list_index (CCEqua i) env_hyp
+  with Not_found -> failwith (Printf.sprintf "get_hyp %d" i)
+
+let replay_history env env_hyp =
   let rec loop env_hyp t =
     match t with
-      | Omega.CONTRADICTION (e1,e2) :: l -> 
-	  let trace = mk_nat (List.length e1.Omega.body) in
+      | Omega2.CONTRADICTION (e1,e2) :: l -> 
+	  let trace = mk_nat (List.length e1.Omega2.body) in
 	  mkApp (Lazy.force coq_s_contradiction,
-		 [| trace ; mk_nat (get_hyp env_hyp e1.Omega.id); 
-		    mk_nat (get_hyp env_hyp e2.Omega.id) |])
-      | Omega.DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
+		 [| trace ; mk_nat (get_hyp env_hyp e1.Omega2.id); 
+		    mk_nat (get_hyp env_hyp e2.Omega2.id) |])
+      | Omega2.DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
 	  mkApp (Lazy.force coq_s_div_approx,
-		 [| mk_Z k; mk_Z d; val_of e2.Omega.body e2.Omega.constant;
-		    mk_nat (List.length e2.Omega.body); 
-		    loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega.id) |])
-      | Omega.NOT_EXACT_DIVIDE (e1,k) :: l ->
-	  let e2_constant = Omega.floor_div e1.Omega.constant k in
-	  let d = e1.Omega.constant - e2_constant * k in
-	  let e2_body = Omega.map_eq_linear (fun c -> c / k) e1.Omega.body in
+		 [| mk_Z k; mk_Z d; 
+		    reified_of_omega env e2.Omega2.body e2.Omega2.constant;
+		    mk_nat (List.length e2.Omega2.body); 
+		    loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega2.id) |])
+      | Omega2.NOT_EXACT_DIVIDE (e1,k) :: l ->
+	  let e2_constant = Omega2.floor_div e1.Omega2.constant k in
+	  let d = e1.Omega2.constant - e2_constant * k in
+	  let e2_body = Omega2.map_eq_linear (fun c -> c / k) e1.Omega2.body in
           mkApp (Lazy.force coq_s_not_exact_divide,
-		 [|mk_Z k; mk_Z d; val_of e2_body e2_constant; 
+		 [|mk_Z k; mk_Z d; 
+		   reified_of_omega env e2_body e2_constant; 
 		   mk_nat (List.length e2_body); 
-		   mk_nat (get_hyp env_hyp e1.Omega.id)|])
-      | Omega.EXACT_DIVIDE (e1,k) :: l ->
-	  let e2_body =  Omega.map_eq_linear (fun c -> c / k) e1.Omega.body in
-	  let e2_constant = Omega.floor_div e1.Omega.constant k in
+		   mk_nat (get_hyp env_hyp e1.Omega2.id)|])
+      | Omega2.EXACT_DIVIDE (e1,k) :: l ->
+	  let e2_body =  
+	    Omega2.map_eq_linear (fun c -> c / k) e1.Omega2.body in
+	  let e2_constant = Omega2.floor_div e1.Omega2.constant k in
           mkApp (Lazy.force coq_s_exact_divide,
-		 [|mk_Z k; val_of e2_body e2_constant; 
+		 [|mk_Z 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.Omega.id)|])
-      | (Omega.MERGE_EQ(e3,e1,e2)) :: l ->
-	  let n1 = get_hyp env_hyp e1.Omega.id and n2 = get_hyp env_hyp e2 in
+		   loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega2.id)|])
+      | (Omega2.MERGE_EQ(e3,e1,e2)) :: l ->
+	  let n1 = get_hyp env_hyp e1.Omega2.id and n2 = get_hyp env_hyp e2 in
           mkApp (Lazy.force coq_s_merge_eq,
-		 [| mk_nat (List.length e1.Omega.body);
+		 [| mk_nat (List.length e1.Omega2.body);
 		    mk_nat n1; mk_nat n2;
-		    loop (e3:: env_hyp) l |])
-      | Omega.SUM(e3,(k1,e1),(k2,e2)) :: l ->
-	  let n1 = get_hyp env_hyp e1.Omega.id 
-	  and n2 = get_hyp env_hyp e2.Omega.id in
-	  let trace = shuffle_path k1 e1.Omega.body k2 e2.Omega.body in
+		    loop (CCEqua e3:: env_hyp) l |])
+      | Omega2.SUM(e3,(k1,e1),(k2,e2)) :: l ->
+	  let n1 = get_hyp env_hyp e1.Omega2.id 
+	  and n2 = get_hyp env_hyp e2.Omega2.id in
+	  let trace = shuffle_path k1 e1.Omega2.body k2 e2.Omega2.body in
           mkApp (Lazy.force coq_s_sum,
 		 [| mk_Z k1; mk_nat n1; mk_Z k2;
-		    mk_nat n2; trace; (loop (e3 :: env_hyp) l) |])
-      | Omega.CONSTANT_NOT_NUL(e,k) :: l -> 
+		    mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |])
+      | Omega2.CONSTANT_NOT_NUL(e,k) :: l -> 
           mkApp (Lazy.force coq_s_constant_not_nul,
 		 [|  mk_nat (get_hyp env_hyp e) |])
-      | Omega.CONSTANT_NEG(e,k) :: l ->
+      | Omega2.CONSTANT_NEG(e,k) :: l ->
           mkApp (Lazy.force coq_s_constant_neg,
 		 [|  mk_nat (get_hyp env_hyp e) |])
-      | Omega.STATE (new_eq,def,orig,m,sigma) :: l ->
-	  let n1 = get_hyp env_hyp orig.Omega.id 
-	  and n2 = get_hyp env_hyp def.Omega.id in
-	  let v = unintern_id sigma in
-	  let o_def = decompile def in
-	  let o_orig = decompile orig in
+      | Omega2.STATE {Omega2.st_new_eq=new_eq; Omega2.st_def =def; 
+		      Omega2.st_orig=orig; Omega2.st_coef=m;
+                      Omega2.st_var=sigma } :: l ->
+	  let n1 = get_hyp env_hyp orig.Omega2.id 
+	  and n2 = get_hyp env_hyp def.Omega2.id in
+	  let v = unintern_omega env sigma in
+	  let o_def = oformula_of_omega env def in
+	  let o_orig = oformula_of_omega env orig in
 	  let body =
-	     Oplus (o_orig,Otimes (Oplus (Oinv v,o_def), Oz m)) in
-	  let trace,_ = normalize_equation body in
+	     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,
 		 [| mk_Z m; trace; mk_nat n1; mk_nat n2; 
-		    loop (new_eq.Omega.id :: env_hyp) l |])
-      |	Omega.HYP _ :: l -> loop env_hyp l
-      |	Omega.CONSTANT_NUL e :: l ->
+		    loop (CCEqua new_eq.Omega2.id :: env_hyp) l |])
+      |	Omega2.HYP _ :: l -> loop env_hyp l
+      |	Omega2.CONSTANT_NUL e :: l ->
 	  mkApp (Lazy.force coq_s_constant_nul, 
 		 [|  mk_nat (get_hyp env_hyp e) |])
-      |	Omega.NEGATE_CONTRADICT(e1,e2,b) :: l ->
-	  if b then
+      |	Omega2.NEGATE_CONTRADICT(e1,e2,b) :: l ->
 	  mkApp (Lazy.force coq_s_negate_contradict, 
-		 [|  mk_nat (get_hyp env_hyp e1.Omega.id);
-		     mk_nat (get_hyp env_hyp e2.Omega.id) |])
-	  else
-	    mkApp (Lazy.force coq_s_negate_contradict_inv, 
-		   [|  mk_nat (List.length e1.Omega.body);
-                       mk_nat (get_hyp env_hyp e1.Omega.id);
-                       mk_nat (get_hyp env_hyp e2.Omega.id) |])
-
-      | Omega.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
-	  let i =  get_hyp env_hyp e.Omega.id in
-	  let r1 = loop (e1 :: env_hyp) l1 in
-	  let r2 = loop (e2 :: env_hyp) l2 in
+		 [|  mk_nat (get_hyp env_hyp e1.Omega2.id);
+		     mk_nat (get_hyp env_hyp e2.Omega2.id) |])
+      | Omega2.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
+	  let i =  get_hyp env_hyp e.Omega2.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, 
-                  [| mk_nat (List.length e.Omega.body); mk_nat i; r1 ; r2 |])
-      |	(Omega.FORGET_C _ | Omega.FORGET _ | Omega.FORGET_I _) :: l ->
+                  [| mk_nat (List.length e.Omega2.body); mk_nat i; r1 ; r2 |])
+      |	(Omega2.FORGET_C _ | Omega2.FORGET _ | Omega2.FORGET_I _) :: l ->
 	  loop env_hyp l
-      | (Omega.WEAKEN  _ ) :: l -> failwith "not_treated"
+      | (Omega2.WEAKEN  _ ) :: l -> failwith "not_treated"
       |	[] -> failwith "no contradiction"
   in loop env_hyp
 
-let show_goal gl =
-  if !debug then Pp.ppnl (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl
-
-(* Cette fonction prépare le rejeu puis l'appelle :
-   \begin{itemize}
-   \item elle isole les hypothèses utiles et les mets dans 
-   le but réifié
-   \item elle prépare l'introduction de nouvelles variables pour le test
-    de Banerjee (opération STATE) 
-   \end{itemize}
-*)
-
-let prepare_and_play env tac_hyps trace_solution =   
-  let rec loop ((l_tac_norm, l_terms, l_id, l_e) as result) = function
-    Omega.HYP e :: l ->
-      let id = tag_of_equation e.Omega.id in
-      let (tac_norm,term) = 
-	try List.assoc id tac_hyps
-        with Not_found -> failwith "what eqn" in
-      loop (tac_norm :: l_tac_norm,term :: l_terms,
-	    Term.mkVar id :: l_id, e.Omega.id :: l_e ) l
-  |  Omega.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
-      loop (loop result l1) l2
-  | _ :: l -> loop result l
-  | [] -> result in
-  let l_tac_norms, l_terms,l_generalized, l_e = 
-    loop ([],[],[],[]) trace_solution in
-
-  let rec loop ((env,l_tac_norm, l_terms,l_gener, l_e) as result) = function
-    Omega.STATE (new_eq,def,orig,m,sigma) :: l ->
-      let o_def = decompile def in
-      let coq_def = coq_of_formula env o_def in
-      let v,env' = add_atom coq_def env in
-      intern_id_force (Oatom v) sigma;
-      let term_to_generalize =
-	mkApp(Lazy.force coq_refl_equal,[|Lazy.force coq_Z; coq_def|]) in
-      let reified_term =
-	 mkApp (Lazy.force coq_t_equal,	
-		[| val_of_formula o_def; val_of_formula (Oatom v) |]) in
-      loop (env', Lazy.force coq_c_nop :: l_tac_norm,
-	    reified_term :: l_terms ,term_to_generalize :: l_gener, 
-	    def.Omega.id :: l_e)  l
-  | Omega.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
-      loop (loop result l1) l2
-  | _ :: l -> loop result l
-  | [] -> result in
-  let env, l_tac_norms, l_terms,l_generalized, l_e = 
-    loop (env, l_tac_norms, l_terms,l_generalized, l_e) trace_solution in
-
-  (* Attention Generalize ajoute les buts dans l'ordre inverse *)
-  let l_reified_terms = mk_list (Lazy.force coq_proposition) l_terms in
-  let l_reified_tac_norms = mk_list (Lazy.force coq_step) l_tac_norms in
-  let env_reified = mk_list (Lazy.force coq_Z) env in
+let rec decompose_tree env ctxt = function
+   Tree(i,left,right) ->
+     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 
+       [| mk_nat index;
+	  mk_direction_list path;
+	  decompose_tree env (left_hyp::ctxt) left;
+	  decompose_tree env (right_hyp::ctxt) right |]
+  | Leaf s ->
+      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) -> 
+      let equation =
+        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 
+	   (CCEqua equation.e_omega.Omega2.id :: ctxt) l in
+      app coq_e_extract [|mk_nat index;
+			  mk_direction_list full_path;
+			  cont |]
+
+(* \section{La fonction principale} *)
+ (* Cette fonction construit la
+trace pour la procédure de décision réflexive.  A partir des résultats
+de l'extraction des systèmes, elle lance la résolution par Omega, puis
+l'extraction d'un ensemble minimal de solutions permettant la
+résolution globale du système et enfin construit la trace qui permet
+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 index = !num in
+    let system = List.map (fun eq -> eq.e_omega) list_eq in
+    let trace = 
+      Omega2.simplify_strong 
+	((fun () -> new_eq_id env),new_omega_id,display_omega_id) 
+	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
+    if !debug then begin
+      Printf.printf "SYSTEME %d\n" index;
+      Omega2.display_action display_omega_id trace;
+      print_string "\n  Depend :";
+      List.iter (fun i -> Printf.printf " %d" i) vars;
+      print_string "\n  Split points :";
+      List.iter display_depend splits;
+      Printf.printf "\n------------------------------------\n"
+    end;
+    incr num;
+    {s_index = index; s_trace = trace; s_equa_deps = vars}, splits  in
+  if !debug then Printf.printf "\n====================================\n";
+  let all_solutions = List.map solve_system systems_list in
+  let solution_tree = solve_with_constraints all_solutions [] in
+  if !debug then  begin
+    display_solution_tree stdout solution_tree;
+    print_newline()
+  end;
+  (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *)
+  let useful_equa_id = list_uniq (equas_of_solution_tree solution_tree) in
+  (* recupere explicitement ces equations *)
+  let equations = List.map (get_equation env) useful_equa_id in
+  let l_hyps' = list_uniq (List.map (fun e -> e.e_origin.o_hyp) equations) in
+  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 = vars_of_equations equations 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
+  let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in
+  let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in
+  (* L'environnement de base se construit en deux morceaux :
+     - les variables des équations utiles
+     - les nouvelles variables declarées durant les preuves *)
+  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 
+	  Hashtbl.add env.real_indices var i; t :: loop (i+1) l
+      |	[] -> [] in
+    loop 0 all_vars_env in
+  let env_terms_reified = mk_list (Lazy.force coq_Z) 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; 
+                                 reified_of_formula env r |])
+              to_introduce in
+  let reified_concl = 
+    match useful_hyps with
+      (Pnot p) :: _ ->
+	reified_of_proposition env (really_useful_prop useful_equa_id p)
+    | _ ->  reified_of_proposition env Pfalse in
+  let l_reified_terms =
+    (List.map
+      (fun p ->
+         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 = 
+    mk_list (Lazy.force coq_proposition)
+            (l_reified_stated @ l_reified_terms) in
   let reified = 
-    mkApp(Lazy.force coq_interp_sequent, [| env_reified; l_reified_terms |]) in
-  let reified_trace_solution = replay_history l_e trace_solution in
-  if !debug then begin
-    Pp.ppnl (Printer.prterm reified);
-    Pp.ppnl (Printer.prterm l_reified_tac_norms);
-    Pp.ppnl (Printer.prterm reified_trace_solution);
+    app coq_interp_sequent 
+       [| env_props_reified;env_terms_reified;reified_concl;reified_goal |] in
+  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
+    app coq_pair_step 
+        [| mk_nat (list_index e.e_origin.o_hyp l_hyps) ;
+	   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 = 
+    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 
+    (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
+  Tactics.change_in_concl None reified >> 
+  Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
+  show_goal >>
+  Tactics.normalise_in_concl >>
+  Tactics.apply (Lazy.force coq_I)
+
+let total_reflexive_omega_tactic gl = 
+  let env = new_environment () in
+  let reified_goal = reify_gl env gl in
+  let systems_list = destructurate_hyps reified_goal in
+  if !debug then begin 
+    display_systems systems_list
   end;
-  Tactics.generalize l_generalized >>
-  Tactics.change_in_concl None reified >>
-  Tacticals.tclTRY 
-    (Tactics.apply (mkApp (Lazy.force coq_normalize_sequent, 
-			   [|l_reified_tac_norms |]))) >>
-  Tacticals.tclTRY 
-    (Tactics.apply (mkApp (Lazy.force coq_execute_sequent, 
-			   [|reified_trace_solution |]))) >>
-  Tactics.normalise_in_concl >> Auto.auto 5 []
-  
-let coq_omega gl =
-  clear_tags (); clear_intern ();
-  let tactic_hyps, system, env = 
-    List.fold_left (destructure_omega gl) ([],[],[])
-      (Tacmach.pf_hyps_types gl) in
-  if !debug then begin Omega.display_system system;  print_newline () end;
-  begin try
-    let trace = Omega.simplify_strong system in 
-    if !debug then Omega.display_action trace;
-    prepare_and_play env tactic_hyps trace gl
-  with Omega.NO_CONTRADICTION -> Util.error "Omega can't solve this system"
-  end
+  resolution env reified_goal systems_list gl
+
+
+(*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
 
-(*
-let refl_omega = Tacmach.hide_atomic_tactic "StepOmega" coq_omega 
-*)
-
-(* \section{Encapsulation ROMEGA} *)
-
-(* Toute cette partie est héritée de [OMEGA]. Seule modification : l'appel
-   à [coq_omega] qui correspond à la version réflexive. Il suffirait de 
-   paramétrer le code par cette tactique.
-
-   \paragraph{Note :} cette partie aussi devrait être réfléchie.  *)
-
-open Reduction
-open Proof_type
-open Ast
-open Names
-open Term
-open Environ
-open Sign
-open Inductive
-open Tacticals
-open Tacmach
-open Tactics
-open Tacticals
-open Clenv
-open Logic
-open Omega
-
-let nat_inject gl = Coq_omega.nat_inject gl
-let elim_id id gl = simplest_elim (pf_global gl id) gl
-let resolve_id id gl = apply (pf_global gl id) gl
-let generalize_tac = Coq_omega.generalize_tac
-let coq_imp_simp = Coq_omega.coq_imp_simp
-let decidability = Coq_omega.decidability
-let coq_not_or = Coq_omega.coq_not_or
-let coq_not_and = Coq_omega.coq_not_and
-let coq_not_imp = Coq_omega.coq_not_imp
-let coq_not_not = Coq_omega.coq_not_not
-let coq_not_Zle = Coq_omega.coq_not_Zle
-let coq_not_Zge = Coq_omega.coq_not_Zge
-let coq_not_Zlt = Coq_omega.coq_not_Zlt
-let coq_not_Zgt = Coq_omega.coq_not_Zgt
-let coq_not_le = Coq_omega.coq_not_le
-let coq_not_ge = Coq_omega.coq_not_ge
-let coq_not_lt = Coq_omega.coq_not_lt
-let coq_not_gt = Coq_omega.coq_not_gt
-let coq_not_eq = Coq_omega.coq_not_eq
-let coq_not_Zeq = Coq_omega.coq_not_Zeq
-let coq_neq = Coq_omega.coq_neq
-let coq_Zne = Coq_omega.coq_Zne
-let coq_dec_not_not = Coq_omega.coq_dec_not_not
-let old_style_flag = Coq_omega.old_style_flag
-let unfold = Coq_omega.unfold
-let sp_not = Coq_omega.sp_not
-let all_time = Coq_omega.all_time
-let mkNewMeta = Coq_omega.mkNewMeta
-	  
-let destructure_hyps gl =
-  let rec loop evbd = function
-    | [] -> (tclTHEN nat_inject coq_omega)
-    | (i,body,t)::lit ->
-	begin try match destructurate t with
-          | Kapp(("Zle"|"Zge"|"Zgt"|"Zlt"|"Zne"),[t1;t2]) -> loop evbd lit
-          | Kapp("or",[t1;t2]) ->
-              (tclTHENS
-                (tclTHENSEQ [elim_id i; clear [i]; intros_using [i]])
-		[ loop evbd ((i,None,t1)::lit); 
-                  loop evbd ((i,None,t2)::lit) ])
-          | Kapp("and",[t1;t2]) ->
-              let i1 = id_of_string (string_of_id i ^ "_left") in
-              let i2 = id_of_string (string_of_id i ^ "_right") in
-              (tclTHENSEQ
-		 [elim_id i;
-                  clear [i];
-		  intros_using [i1;i2];
-		  loop (i1::i2::evbd) ((i1,None,t1)::(i2,None,t2)::lit)])
-          | Kimp(t1,t2) ->
-              if isprop (pf_type_of gl t1) & closed0 t2 then begin
-		(tclTHENSEQ
-                  [generalize_tac [mkApp (Lazy.force coq_imp_simp,
-                                          [| t1; t2; 
-					     decidability gl t1;
-					     mkVar i|])]; 
-		   clear [i];
-		   intros_using [i]; 
-		   loop evbd ((i,None,mk_or (mk_not t1) t2)::lit)])
-              end else loop evbd lit
-          | Kapp("not",[t]) -> 
-              begin match destructurate t with 
-		  Kapp("or",[t1;t2]) -> 
-                    (tclTHENSEQ
-		      [generalize_tac [mkApp (Lazy.force coq_not_or,
-                                              [| t1; t2; mkVar i |])];
-		       clear [i]; 
-		       intros_using [i]; 
-                       loop evbd 
-                         ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit)])
-		| Kapp("and",[t1;t2]) -> 
-                    (tclTHENSEQ
-		      [generalize_tac
-				[mkApp (Lazy.force coq_not_and, [| t1; t2;
-					   decidability gl t1;mkVar i|])];
-		       clear [i];
-		       intros_using [i];
-                       loop evbd ((i,None,mk_or (mk_not t1) (mk_not t2))::lit)])
-		| Kimp(t1,t2) ->
-                    (tclTHENSEQ
-		      [generalize_tac 
-				[mkApp (Lazy.force coq_not_imp, [| t1; t2; 
-					   decidability gl t1;mkVar i |])];
-		       clear [i];
-		       intros_using [i];
-                       loop evbd ((i,None,mk_and t1 (mk_not t2)) :: lit)])
-		| Kapp("not",[t]) ->
-                    (tclTHENSEQ
-                      [generalize_tac
-				[mkApp (Lazy.force coq_not_not, [| t;
-					    decidability gl t; mkVar i |])];
-		       clear [i]; 
-		       intros_using [i];
-                       loop evbd ((i,None,t)::lit)])
-		| Kapp("Zle", [t1;t2]) ->
-                    (tclTHENSEQ
-		      [generalize_tac [mkApp (Lazy.force coq_not_Zle,
-					      [| t1;t2;mkVar i|])];
-		       clear [i];
-		       intros_using [i];
-		       loop evbd lit])
-		| Kapp("Zge", [t1;t2]) ->
-                    (tclTHENSEQ
-		      [generalize_tac [mkApp (Lazy.force coq_not_Zge,
-					      [| t1;t2;mkVar i|])];
-		       clear [i];
-		       intros_using [i];
-		       loop evbd lit])
-		| Kapp("Zlt", [t1;t2]) ->
-                    (tclTHENSEQ
-		      [generalize_tac [mkApp (Lazy.force coq_not_Zlt,
-					      [| t1;t2;mkVar i|])];
-		       clear [i];
-		       intros_using [i];
-		       loop evbd lit])
-		| Kapp("Zgt", [t1;t2]) ->
-                    (tclTHENSEQ
-		      [generalize_tac [mkApp (Lazy.force coq_not_Zgt,
-					      [| t1;t2;mkVar i|])];
-		       clear [i];
-		       intros_using [i];
-		       loop evbd lit])
-		| Kapp("le", [t1;t2]) ->
-                    (tclTHENSEQ
-		      [generalize_tac [mkApp (Lazy.force coq_not_le,
-					      [| t1;t2;mkVar i|])];
-		       clear [i];
-		       intros_using [i];
-		       loop evbd lit])
-		| Kapp("ge", [t1;t2]) ->
-                    (tclTHENSEQ
-		      [generalize_tac [mkApp (Lazy.force coq_not_ge,
-					      [| t1;t2;mkVar i|])];
-		       clear [i];
-		       intros_using [i];
-		       loop evbd lit])
-		| Kapp("lt", [t1;t2]) ->
-                    (tclTHENSEQ
-		      [generalize_tac [mkApp (Lazy.force coq_not_lt,
-					      [| t1;t2;mkVar i|])];
-		       clear [i];
-		       intros_using [i];
-		       loop evbd lit])
-		| Kapp("gt", [t1;t2]) ->
-                    (tclTHENSEQ
-		      [generalize_tac [mkApp (Lazy.force coq_not_gt,
-					      [| t1;t2;mkVar i|])];
-		       clear [i];
-		       intros_using [i];
-		       loop evbd lit])
-		| Kapp("eq",[typ;t1;t2]) ->
-                    if !old_style_flag then begin 
-		      match destructurate (pf_nf gl typ) with
-			| Kapp("nat",_) -> 
-                            (tclTHENSEQ
-			      [simplest_elim 
-				(applist 
-				  (Lazy.force coq_not_eq,[t1;t2;mkVar i]));
-			        clear [i];
-			        intros_using [i];
-			        loop evbd lit])
-			| Kapp("Z",_) ->
-                            (tclTHENSEQ
-			      [simplest_elim 
-				(applist 
-				  (Lazy.force coq_not_Zeq,[t1;t2;mkVar i]));
-			       clear [i];
-			       intros_using [i];
-			       loop evbd lit])
-			| _ -> loop evbd lit
-                    end else begin 
-		      match destructurate (pf_nf gl typ) with
-			| Kapp("nat",_) -> 
-                            (tclTHEN 
-			       (convert_hyp_no_check
-                                  (i,body,
-				  (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
-			       (loop evbd lit))
-			| Kapp("Z",_) ->
-                            (tclTHEN 
-			       (convert_hyp_no_check
-                                  (i,body,
-				  (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
-			       (loop evbd lit))
-			| _ -> loop evbd lit
-                    end
-		| _ -> loop evbd lit
-              end 
-          | _ -> loop evbd lit 
-	with e when catchable_exception e -> loop evbd lit
-	end 
-  in
-  loop (pf_ids_of_hyps gl) (pf_hyps gl) gl
-
-let omega_solver gl =
-  Library.check_required_library ["Coq";"romega";"ROmega"];
-  let concl = pf_concl gl in
-  let rec loop t =
-    match destructurate t with
-      | Kapp("not",[t1;t2]) -> 
-          (tclTHENSEQ [unfold sp_not; intro; destructure_hyps])
-      | Kimp(a,b) -> (tclTHEN intro (loop b))
-      | Kapp("False",[]) -> destructure_hyps
-      | _ ->
-          (tclTHENSEQ
-	    [Tactics.refine 
-	      (mkApp (Lazy.force coq_dec_not_not,
-                      [| t; decidability gl t; mkNewMeta () |]));
-	     intro;
-	     destructure_hyps])
-  in
-  (loop concl) gl
-
-(*
-let omega = hide_atomic_tactic "ReflOmega" omega_solver
-*)