romega: no more normalization trace, replaced by some Coq-side computation

 This is a major change :

 - Generated proofs are quite shorter, since only the resolution trace remains.
 - No time penalty mesured (it even tends to be slightly faster this way).
 - Less infrastructure in ReflOmegaCore and refl_omega.
 - Warning: the normalization functions in ML and in Coq should be kept
   in sync, as well as the variable order.
 - Btw: get rid of ML constructor Oufo

4 files changed, 461 insertions, 1346 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index dad9909d2..8fa6905ba 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -16,6 +16,8 @@ Module Type Int.
 
   Parameter t : Set.
 
+  Bind Scope Int_scope with t.
+
   Parameter zero : t.
   Parameter one : t.
   Parameter plus : t -> t -> t.
@@ -177,7 +179,7 @@ Module IntProperties (I:Int).
  Lemma plus_reg_l : forall x y z, x+y = x+z -> y = z.
  Proof.
   intros.
-  rewrite (plus_0_r_reverse y), (plus_0_r_reverse z), <-(opp_def x).
+  rewrite <- (plus_0_r y), <- (plus_0_r z), <-(opp_def x).
   now rewrite plus_permute, plus_assoc, H, <- plus_assoc, plus_permute.
  Qed.
 
@@ -193,16 +195,23 @@ Module IntProperties (I:Int).
   apply mult_plus_distr_r.
  Qed.
 
- Lemma mult_0_l : forall x, 0*x = 0.
+ Lemma mult_0_l x : 0*x = 0.
  Proof.
-  intros.
-  generalize (mult_plus_distr_r 0 1 x).
-  rewrite plus_0_l, mult_1_l, plus_comm; intros.
+  assert (H := mult_plus_distr_r 0 1 x).
+  rewrite plus_0_l, mult_1_l, plus_comm in H.
   apply plus_reg_l with x.
-  rewrite <- H.
-  apply plus_0_r_reverse.
+  now rewrite <- H, plus_0_r.
+ Qed.
+
+ Lemma mult_0_r x : x*0 = 0.
+ Proof.
+   rewrite mult_comm. apply mult_0_l.
  Qed.
 
+ Lemma mult_1_r x : x*1 = x.
+ Proof.
+   rewrite mult_comm. apply mult_1_l.
+ Qed.
 
  (* More facts about opp *)
 
@@ -252,6 +261,13 @@ Module IntProperties (I:Int).
  Lemma egal_left : forall n m, n=m -> n+-m = 0.
  Proof. intros; subst; apply opp_def. Qed.
 
+ Lemma egal_left_iff n m : n = m <-> 0 = n + - m.
+ Proof.
+  split. intros. symmetry. now apply egal_left.
+  intros. apply plus_reg_l with (-m).
+  rewrite plus_comm, <- H. symmetry. apply plus_opp_l.
+ Qed.
+
  Lemma ne_left_2 : forall x y : int, x<>y -> 0<>(x + - y).
  Proof.
  intros; contradict H.
@@ -262,7 +278,7 @@ Module IntProperties (I:Int).
  (* Special lemmas for factorisation. *)
 
  Lemma red_factor0 : forall n, n = n*1.
- Proof. symmetry; rewrite mult_comm; apply mult_1_l. Qed.
+ Proof. symmetry; apply mult_1_r. Qed.
 
  Lemma red_factor1 : forall n, n+n = n*2.
  Proof.
@@ -273,7 +289,7 @@ Module IntProperties (I:Int).
  Lemma red_factor2 : forall n m, n + n*m = n * (1+m).
  Proof.
   intros; rewrite mult_plus_distr_l.
-  f_equal; now rewrite mult_comm, mult_1_l.
+  now rewrite mult_1_r.
  Qed.
 
  Lemma red_factor3 : forall n m, n*m + n = n*(1+m).
@@ -450,6 +466,11 @@ Module IntProperties (I:Int).
   generalize (lt_trans _ _ _ H C); intuition.
  Qed.
 
+ Lemma not_eq (a b:int) : ~ a <> b <-> a = b.
+ Proof.
+  destruct (eq_dec a b); intuition.
+ Qed.
+
  (* order and operations *)
 
  Lemma le_0_neg : forall n, 0 <= n <-> -n <= 0.
@@ -600,13 +621,15 @@ Module IntProperties (I:Int).
  apply lt_0_1.
  Qed.
 
- Lemma le_left : forall n m, n <= m -> 0 <= m + - n.
+ Lemma le_left n m : n <= m <-> 0 <= m + - n.
  Proof.
-  intros.
-  rewrite <- (opp_def m).
-  apply plus_le_compat.
-  apply le_refl.
-  apply opp_le_compat; auto.
+  split; intros.
+  - rewrite <- (opp_def m).
+    apply plus_le_compat.
+    apply le_refl.
+    apply opp_le_compat; auto.
+  - apply plus_le_reg_r with (-n).
+    now rewrite plus_opp_r.
  Qed.
 
  Lemma OMEGA2 : forall x y, 0 <= x -> 0 <= y -> 0 <= x + y.
@@ -662,7 +685,7 @@ Module IntProperties (I:Int).
 
  Lemma lt_left : forall n m, n < m -> 0 <= m + -(1) + - n.
  Proof.
- intros; apply le_left.
+ intros. rewrite <- le_left.
  now rewrite <- le_lt_int.
  Qed.
 
@@ -735,7 +758,7 @@ Module IntProperties (I:Int).
  rewrite le_lt_int.
  apply le_trans with (n+-(1)); [ now apply le_lt_int | ].
  apply plus_le_compat; [ | apply le_refl ].
- rewrite <- (mult_1_l n) at 1. rewrite mult_comm.
+ rewrite <- (mult_1_r n) at 1.
  apply mult_le_compat_l; auto using lt_le_weak.
  Qed.
 
@@ -798,6 +821,7 @@ Inductive term : Set :=
   | Topp : term -> term
   | Tvar : N -> term.
 
+Bind Scope romega_scope with term.
 Delimit Scope romega_scope with term.
 Arguments Tint _%I.
 Arguments Tplus (_ _)%term.
@@ -845,58 +869,6 @@ Notation singleton := (fun a : hyps => a :: nil).
 (* an absurd goal *)
 Definition absurd := FalseTerm :: nil.
 
-(* \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
-  | F_cancel : t_fusion
-  | F_left : t_fusion
-  | F_right : t_fusion.
-
-(* \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_COMM : 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_COMM : step.
-
 (* \subsubsection{Omega steps} *)
 (* The following inductive type describes steps as they can be found in
    the trace coming from the decision procedure Omega. *)
@@ -906,40 +878,19 @@ Inductive t_omega : Set :=
   | O_CONSTANT_NOT_NUL : nat -> t_omega
   | O_CONSTANT_NEG : nat -> t_omega
   (* division and approximation of an equation *)
-  | O_DIV_APPROX : int -> int -> term -> t_omega -> nat -> t_omega
+  | O_DIV_APPROX : nat -> int -> int -> term -> t_omega -> t_omega
   (* no solution because no exact division *)
-  | O_NOT_EXACT_DIVIDE : int -> int -> term -> nat -> t_omega
+  | O_NOT_EXACT_DIVIDE : nat -> int -> int -> term -> t_omega
   (* exact division *)
-  | O_EXACT_DIVIDE : int -> term -> t_omega -> nat -> t_omega
-  | O_SUM : int -> nat -> int -> nat -> list t_fusion -> t_omega -> t_omega
+  | O_EXACT_DIVIDE : nat -> int -> term -> t_omega -> t_omega
+  | O_SUM : int -> nat -> int -> nat -> t_omega -> t_omega
   | O_CONTRADICTION : nat -> nat -> t_omega
   | O_MERGE_EQ : nat -> nat -> t_omega -> t_omega
   | O_SPLIT_INEQ : 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 -> t_omega
-  | O_STATE : int -> step -> nat -> nat -> t_omega -> t_omega.
-
-(* \subsubsection{Rules for normalizing the hypothesis} *)
-(* These rules indicate how to normalize useful propositions
-   of each useful hypothesis before the decomposition of hypothesis.
-   Negation nodes could be traversed by either [P_LEFT] or [P_RIGHT].
-   The rules include the inversion phase for negation removal. *)
-
-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.
-
-(* List of normalizations to perform : if the type [p_step] had a constructor
-   that indicated visiting both left and right branches, we would be able to
-   restrict ourselves to the case of only one normalization by hypothesis.
-   And since all hypothesis are useful (otherwise they wouldn't be included),
-   we would be able to replace [h_step] by a simple list. *)
-
-Inductive h_step : Set :=
-    pair_step : nat -> p_step -> h_step.
+  | O_STATE : int -> nat -> nat -> t_omega -> t_omega.
 
 (* \subsubsection{Rules for decomposing the hypothesis} *)
 (* This type allows navigation in the logical constructors that
@@ -971,8 +922,6 @@ Inductive e_step : Set :=
 
 (* \subsubsection{Reified terms} *)
 
-Open Scope romega_scope.
-
 Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
   match t1, t2 with
   | Tint st1, Tint st2 => beq st1 st2
@@ -982,9 +931,7 @@ Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
   | (- st1), (- st2) => eq_term st1 st2
   | [st1], [st2] => N.eqb st1 st2
   | _, _ => false
-  end.
-
-Close Scope romega_scope.
+  end%term.
 
 Theorem eq_term_iff (t t' : term) :
  eq_term t t' = true <-> t = t'.
@@ -1258,93 +1205,6 @@ Proof.
        * 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
-   tactiques de conversion *)
-
-Definition apply_left (f : term -> term) (t : term) :=
-  match t with
-  | (x + y)%term => (f x + y)%term
-  | (x * y)%term => (f x * y)%term
-  | (- x)%term => (- f x)%term
-  | x => x
-  end.
-
-Definition apply_right (f : term -> term) (t : term) :=
-  match t with
-  | (x + y)%term => (x + f y)%term
-  | (x * y)%term => (x * f y)%term
-  | x => x
-  end.
-
-Definition apply_both (f g : term -> term) (t : term) :=
-  match t with
-  | (x + y)%term => (f x + g y)%term
-  | (x * y)%term => (f x * g y)%term
-  | x => x
-  end.
-
-(* 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).
-Proof.
- unfold term_stable; intros f H e t; case t; auto; simpl;
- intros; elim H; trivial.
-Qed.
-
-Theorem apply_right_stable :
- forall f : term -> term, term_stable f -> term_stable (apply_right f).
-Proof.
- unfold term_stable; intros f H e t; case t; auto; simpl;
- 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).
-Proof.
- unfold term_stable; intros f g H1 H2 e t; case t; auto; simpl;
- 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)).
-Proof.
- unfold term_stable; 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.
-
-   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.
-   \end{itemize}
-   Les motifs sur les cas sont très imparfaits et dans certains cas, il
-   semble que cela ne marche pas. On aimerait plutot un motif de la
-   forme [ Case (?1 :: T) of _ end ] permettant de s'assurer que l'on
-   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.
-
-   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é} *)
 
 Ltac loop t :=
@@ -1379,6 +1239,8 @@ Ltac loop t :=
       try (rewrite H in *; clear H); simpl; auto; Simplify
   | (if _ && _ then _ else _) => rewrite andb_if; Simplify
   | (if negb _ then _ else _) => rewrite negb_if; Simplify
+  | match N.compare ?X1 ?X2 with _ => _ end =>
+    destruct (N.compare_spec X1 X2); Simplify
   | match ?X1 with _ => _ end => destruct X1; auto; Simplify
   | _ => fail
   end
@@ -1388,401 +1250,12 @@ with Simplify := match goal with
   | _ => idtac
   end.
 
-Ltac prove_stable x th :=
-  match constr:(x) with
-  | ?X1 =>
-      unfold term_stable, X1; intros; Simplify; simpl;
-       apply th
-  end.
-
-(* \subsubsection{Les règles elle mêmes} *)
-Definition Tplus_assoc_l (t : term) :=
-  match t with
-  | (n + (m + p))%term => (n + m + p)%term
-  | _ => t
-  end.
-
-Theorem Tplus_assoc_l_stable : term_stable Tplus_assoc_l.
-Proof.
- prove_stable Tplus_assoc_l (ring.(Radd_assoc)).
-Qed.
-
-Definition Tplus_assoc_r (t : term) :=
-  match t with
-  | (n + m + p)%term => (n + (m + p))%term
-  | _ => t
-  end.
-
-Theorem Tplus_assoc_r_stable : term_stable Tplus_assoc_r.
-Proof.
- prove_stable Tplus_assoc_r plus_assoc_reverse.
-Qed.
-
-Definition Tmult_assoc_r (t : term) :=
-  match t with
-  | (n * m * p)%term => (n * (m * p))%term
-  | _ => t
-  end.
-
-Theorem Tmult_assoc_r_stable : term_stable Tmult_assoc_r.
-Proof.
- prove_stable Tmult_assoc_r mult_assoc_reverse.
-Qed.
-
-Definition Tplus_permute (t : term) :=
-  match t with
-  | (n + (m + p))%term => (m + (n + p))%term
-  | _ => t
-  end.
-
-Theorem Tplus_permute_stable : term_stable Tplus_permute.
-Proof.
- prove_stable Tplus_permute plus_permute.
-Qed.
-
-Definition Tplus_comm (t : term) :=
-  match t with
-  | (x + y)%term => (y + x)%term
-  | _ => t
-  end.
-
-Theorem Tplus_comm_stable : term_stable Tplus_comm.
-Proof.
- prove_stable Tplus_comm plus_comm.
-Qed.
-
-Definition Tmult_comm (t : term) :=
-  match t with
-  | (x * y)%term => (y * x)%term
-  | _ => t
-  end.
-
-Theorem Tmult_comm_stable : term_stable Tmult_comm.
-Proof.
- prove_stable Tmult_comm mult_comm.
-Qed.
-
-Definition T_OMEGA10 (t : term) :=
-  match t with
-  | ((v * Tint c1 + l1) * Tint k1 + (v' * Tint c2 + l2) * Tint k2)%term =>
-      if eq_term v v'
-      then (v * Tint (c1 * k1 + c2 * k2)%I + (l1 * Tint k1 + l2 * Tint k2))%term
-      else t
-  | _ => t
-  end.
-
-Theorem T_OMEGA10_stable : term_stable T_OMEGA10.
-Proof.
- prove_stable T_OMEGA10 OMEGA10.
-Qed.
-
-Definition T_OMEGA11 (t : term) :=
-  match t with
-  | ((v1 * Tint c1 + l1) * Tint k1 + l2)%term =>
-      (v1 * Tint (c1 * k1) + (l1 * Tint k1 + l2))%term
-  | _ => t
-  end.
-
-Theorem T_OMEGA11_stable : term_stable T_OMEGA11.
-Proof.
- prove_stable T_OMEGA11 OMEGA11.
-Qed.
-
-Definition T_OMEGA12 (t : term) :=
-  match t with
-  | (l1 + (v2 * Tint c2 + l2) * Tint k2)%term =>
-      (v2 * Tint (c2 * k2) + (l1 + l2 * Tint k2))%term
-  | _ => t
-  end.
-
-Theorem T_OMEGA12_stable : term_stable T_OMEGA12.
-Proof.
- prove_stable T_OMEGA12 OMEGA12.
-Qed.
-
-Definition Tred_factor5 (t : term) :=
-  match t with
-  | (x * Tint c + y)%term => if beq c 0 then y else t
-  | _ => t
-  end.
-
-Theorem Tred_factor5_stable : term_stable Tred_factor5.
-Proof.
- prove_stable Tred_factor5 red_factor5.
-Qed.
-
-Definition Topp_plus (t : term) :=
-  match t with
-  | (- (x + y))%term => (- x + - y)%term
-  | _ => t
-  end.
-
-Theorem Topp_plus_stable : term_stable Topp_plus.
-Proof.
- prove_stable Topp_plus opp_plus_distr.
-Qed.
-
-
-Definition Topp_opp (t : term) :=
-  match t with
-  | (- - x)%term => x
-  | _ => t
-  end.
-
-Theorem Topp_opp_stable : term_stable Topp_opp.
-Proof.
- prove_stable Topp_opp opp_involutive.
-Qed.
-
-Definition Topp_mult_r (t : term) :=
-  match t with
-  | (- (x * Tint k))%term => (x * Tint (- k))%term
-  | _ => t
-  end.
-
-Theorem Topp_mult_r_stable : term_stable Topp_mult_r.
-Proof.
- prove_stable Topp_mult_r opp_mult_distr_r.
-Qed.
-
-Definition Topp_one (t : term) :=
-  match t with
-  | (- x)%term => (x * Tint (-(1)))%term
-  | _ => t
-  end.
-
-Theorem Topp_one_stable : term_stable Topp_one.
-Proof.
- prove_stable Topp_one opp_eq_mult_neg_1.
-Qed.
-
-Definition Tmult_plus_distr (t : term) :=
-  match t with
-  | ((n + m) * p)%term => (n * p + m * p)%term
-  | _ => t
-  end.
-
-Theorem Tmult_plus_distr_stable : term_stable Tmult_plus_distr.
-Proof.
- prove_stable Tmult_plus_distr mult_plus_distr_r.
-Qed.
-
-Definition Tmult_opp_left (t : term) :=
-  match t with
-  | (- x * Tint y)%term => (x * Tint (- y))%term
-  | _ => t
-  end.
-
-Theorem Tmult_opp_left_stable : term_stable Tmult_opp_left.
-Proof.
- prove_stable Tmult_opp_left mult_opp_comm.
-Qed.
-
-Definition Tmult_assoc_reduced (t : term) :=
-  match t with
-  | (n * Tint m * Tint p)%term => (n * Tint (m * p))%term
-  | _ => t
-  end.
-
-Theorem Tmult_assoc_reduced_stable : term_stable Tmult_assoc_reduced.
-Proof.
- prove_stable Tmult_assoc_reduced mult_assoc_reverse.
-Qed.
-
-Definition Tred_factor0 (t : term) := (t * Tint 1)%term.
-
-Theorem Tred_factor0_stable : term_stable Tred_factor0.
-Proof.
- prove_stable Tred_factor0 red_factor0.
-Qed.
-
-Definition Tred_factor1 (t : term) :=
-  match t with
-  | (x + y)%term =>
-      if eq_term x y
-      then (x * Tint 2)%term
-      else t
-  | _ => t
-  end.
-
-Theorem Tred_factor1_stable : term_stable Tred_factor1.
-Proof.
- prove_stable Tred_factor1 red_factor1.
-Qed.
-
-Definition Tred_factor2 (t : term) :=
-  match t with
-  | (x + y * Tint k)%term =>
-      if eq_term x y
-      then (x * Tint (1 + k))%term
-      else t
-  | _ => t
-  end.
-
-Theorem Tred_factor2_stable : term_stable Tred_factor2.
-Proof.
- prove_stable Tred_factor2 red_factor2.
-Qed.
-
-Definition Tred_factor3 (t : term) :=
-  match t with
-  | (x * Tint k + y)%term =>
-      if eq_term x y
-      then (x * Tint (1 + k))%term
-      else t
-  | _ => t
-  end.
-
-Theorem Tred_factor3_stable : term_stable Tred_factor3.
-Proof.
- prove_stable Tred_factor3 red_factor3.
-Qed.
-
-
-Definition Tred_factor4 (t : term) :=
-  match t with
-  | (x * Tint k1 + y * Tint k2)%term =>
-      if eq_term x y
-      then (x * Tint (k1 + k2))%term
-      else t
-  | _ => t
-  end.
-
-Theorem Tred_factor4_stable : term_stable Tred_factor4.
-Proof.
- prove_stable Tred_factor4 red_factor4.
-Qed.
-
-Definition Tred_factor6 (t : term) := (t + Tint 0)%term.
-
-Theorem Tred_factor6_stable : term_stable Tred_factor6.
-Proof.
- prove_stable Tred_factor6 red_factor6.
-Qed.
-
-Definition Tminus_def (t : term) :=
-  match t with
-  | (x - y)%term => (x + - y)%term
-  | _ => t
-  end.
-
-Theorem Tminus_def_stable : term_stable Tminus_def.
-Proof.
- prove_stable Tminus_def minus_def.
-Qed.
-
-(* \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''.  *)
-
-Fixpoint reduce (t : term) : term :=
-  match t with
-  | (x + y)%term =>
-      match reduce x with
-      | Tint xi as xr =>
-          match reduce y with
-          | Tint yi => Tint (xi + yi)
-          | yr => (xr + yr)%term
-          end
-      | xr => (xr + reduce y)%term
-      end
-  | (x * y)%term =>
-      match reduce x with
-      | Tint xi as xr =>
-          match reduce y with
-          | Tint yi => Tint (xi * yi)
-          | yr => (xr * yr)%term
-          end
-      | xr => (xr * reduce y)%term
-      end
-  | (x - y)%term =>
-      match reduce x with
-      | Tint xi as xr =>
-          match reduce y with
-          | Tint yi => Tint (xi - yi)
-          | yr => (xr - yr)%term
-          end
-      | xr => (xr - reduce y)%term
-      end
-  | (- x)%term =>
-      match reduce x with
-      | Tint xi => Tint (- xi)
-      | xr => (- xr)%term
-      end
-  | _ => t
-  end.
-
-Theorem reduce_stable : term_stable reduce.
-Proof.
- red. intros e t; induction t; simpl; auto;
-  do 2 destruct reduce; simpl; f_equal; auto.
-Qed.
-
-(* \subsubsection{Fusions}
-    \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]. *)
-
-Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term :=
-  match trace with
-  | nil => reduce t
-  | step :: trace' =>
-      match step with
-      | F_equal => apply_right (fusion trace') (T_OMEGA10 t)
-      | F_cancel => fusion trace' (Tred_factor5 (T_OMEGA10 t))
-      | F_left => apply_right (fusion trace') (T_OMEGA11 t)
-      | F_right => apply_right (fusion trace') (T_OMEGA12 t)
-      end
-  end.
-
-Theorem fusion_stable : forall trace : list t_fusion, term_stable (fusion trace).
-Proof.
- simple induction trace; simpl.
- - exact reduce_stable.
- - intros stp l H; case stp.
-    + apply compose_term_stable.
-       * apply apply_right_stable; assumption.
-       * exact T_OMEGA10_stable.
-    + unfold term_stable; intros e t1; rewrite T_OMEGA10_stable;
-       rewrite Tred_factor5_stable; apply H.
-    + apply compose_term_stable.
-       * apply apply_right_stable; assumption.
-       * exact T_OMEGA11_stable.
-    + apply compose_term_stable.
-       * apply apply_right_stable; assumption.
-       * exact T_OMEGA12_stable.
-Qed.
-
-(* \paragraph{Fusion avec annihilation} *)
-(* Normalement le résultat est une constante *)
-
-Fixpoint fusion_cancel (t1 t2 : term) : term :=
-  match t1, t2 with
-  | (v1 * Tint x1 + l1)%term, (v2 * Tint x2 + l2)%term =>
-    if eq_term v1 v2 && beq x1 (-x2)
-    then fusion_cancel l1 l2
-    else (t1+t2)%term (* should not happen *)
-  | Tint x1, Tint x2 => Tint (x1+x2)
-  | _, _ => (t1+t2)%term (* should not happen *)
-  end.
-
-Theorem fusion_cancel_stable e t1 t2 :
- interp_term e (t1+t2)%term = interp_term e (fusion_cancel t1 t2).
-Proof.
- revert t2. induction t1; destruct t2; simpl; Simplify; auto.
- simpl in *.
- rewrite <- IHt1_2.
- apply OMEGA13.
-Qed.
-
 (* \subsubsection{Opérations affines sur une équation} *)
+
 (* \paragraph{Multiplication scalaire et somme d'une constante} *)
 
+(* invariant: k1<>0 *)
+
 Fixpoint scalar_norm_add (t : term) (k1 k2 : int) : term :=
   match t with
   | (v1 * Tint x1 + l1)%term =>
@@ -1800,6 +1273,7 @@ Proof.
 Qed.
 
 (* \paragraph{Multiplication scalaire} *)
+
 Definition scalar_norm (t : term) (k : int) := scalar_norm_add t k 0.
 
 Theorem scalar_norm_stable e t k :
@@ -1810,6 +1284,7 @@ Proof.
 Qed.
 
 (* \paragraph{Somme d'une constante} *)
+
 Fixpoint add_norm (t : term) (k : int) : term :=
   match t with
   | (m + l)%term => (m + add_norm l k)%term
@@ -1824,70 +1299,101 @@ Proof.
  rewrite <- IHt2. simpl. symmetry. apply plus_assoc.
 Qed.
 
-(* \subsection{La fonction de normalisation des termes (moteur de réécriture)} *)
+(* \subsubsection{Fusions}
+    \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. *)
+(* Invariant : k1 and k2 non-null *)
+
+Fixpoint fusion (t1 t2 : term) (k1 k2 : int) : term :=
+  match t1 with
+  | ([v1] * Tint x1 + l1)%term =>
+    (fix fusion_t1 t2 : term :=
+       match t2 with
+         | ([v2] * Tint x2 + l2)%term =>
+           match N.compare v1 v2 with
+             | Eq =>
+               let k := x1 * k1 + x2 * k2 in
+               if beq k 0 then fusion l1 l2 k1 k2
+               else ([v1] * Tint k + fusion l1 l2 k1 k2)%term
+             | Lt => ([v2] * Tint (x2 * k2) + fusion_t1 l2)%term
+             | Gt => ([v1] * Tint (x1 * k1) + fusion l1 t2 k1 k2)%term
+           end
+         | Tint x2 => ([v1] * Tint (x1 * k1) + fusion l1 t2 k1 k2)%term
+         | _ => (t1 * Tint k1 + t2 * Tint k2)%term
+       end) t2
+  | Tint x1 => scalar_norm_add t2 k2 (x1 * k1)
+  | _ => (t1 * Tint k1 + t2 * Tint k2)%term (* shouldn't happen *)
+  end.
+
+Theorem fusion_stable e t1 t2 k1 k2 :
+ interp_term e (t1 * Tint k1 + t2 * Tint k2)%term =
+ interp_term e (fusion t1 t2 k1 k2).
+Proof.
+ revert t2; induction t1; simpl; Simplify; simpl; auto.
+ - intros; rewrite <- scalar_norm_add_stable. simpl. apply plus_comm.
+ - intros. Simplify. induction t2; simpl; Simplify; simpl; auto.
+   + rewrite <- IHt1_2. simpl. apply OMEGA11.
+   + rewrite <- IHt1_2. simpl. subst n0. rewrite OMEGA10, H0.
+     now rewrite mult_comm, mult_0_l, plus_0_l.
+   + rewrite <- IHt1_2. simpl. subst n0. apply OMEGA10.
+   + rewrite <- IHt2_2. simpl. apply OMEGA12.
+   + rewrite <- IHt1_2. simpl. apply OMEGA11.
+Qed.
+
+(* Main function of term normalization.
+   Precondition: all [Tmult] should be on at least one [Tint].
+   Postcondition: [([v1]*Tint k1 + ([v2]*Tint k2 + (... + Tint cst)))]
+    with [v1>v2>...] and [ki<>0].
+ *)
+
+Fixpoint normalize t :=
+  match t with
+  | Tint n => Tint n
+  | [n]%term => ([n] * Tint 1 + Tint 0)%term
+  | (t + t')%term => fusion (normalize t) (normalize t') 1 1
+  | (- t)%term => scalar_norm (normalize t) (-(1))
+  | (t - t')%term => fusion (normalize t) (normalize t') 1 (-(1))
+  | (Tint k * t)%term | (t * Tint k)%term =>
+    if beq k 0 then Tint 0
+    else scalar_norm (normalize t) k
+  | (t1 * t2)%term => (t1 * t2)%term (* shouldn't happen *)
+  end.
+
+Theorem normalize_stable : term_stable normalize.
+Proof.
+ intros e t.
+ induction t; simpl; Simplify; simpl;
+ rewrite <- ?scalar_norm_stable; simpl in *; rewrite <- ?IHt1;
+ rewrite <- ?fusion_stable; simpl;
+ rewrite ?mult_0_l, ?mult_0_r, ?mult_1_l, ?mult_1_r, ?plus_0_r; auto.
+ - now f_equal.
+ - rewrite mult_comm. now f_equal.
+ - rewrite <- opp_eq_mult_neg_1, <-minus_def. now f_equal.
+ - rewrite <- opp_eq_mult_neg_1. now f_equal.
+Qed.
 
+(* \paragraph{Fusion avec annihilation} *)
+(* Normalement le résultat est une constante *)
 
-Fixpoint t_rewrite (s : step) : term -> term :=
-  match s with
-  | C_DO_BOTH s1 s2 => apply_both (t_rewrite s1) (t_rewrite s2)
-  | C_LEFT s => apply_left (t_rewrite s)
-  | C_RIGHT s => apply_right (t_rewrite s)
-  | C_SEQ s1 s2 => fun t : term => t_rewrite s2 (t_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
-  | C_OPP_ONE => Topp_one
-  | C_REDUCE => reduce
-  | C_MULT_PLUS_DISTR => Tmult_plus_distr
-  | C_MULT_OPP_LEFT => Tmult_opp_left
-  | C_MULT_ASSOC_R => Tmult_assoc_r
-  | C_PLUS_ASSOC_R => Tplus_assoc_r
-  | C_PLUS_ASSOC_L => Tplus_assoc_l
-  | C_PLUS_PERMUTE => Tplus_permute
-  | C_PLUS_COMM => Tplus_comm
-  | C_RED0 => Tred_factor0
-  | C_RED1 => Tred_factor1
-  | C_RED2 => Tred_factor2
-  | C_RED3 => Tred_factor3
-  | C_RED4 => Tred_factor4
-  | C_RED5 => Tred_factor5
-  | C_RED6 => Tred_factor6
-  | C_MULT_ASSOC_REDUCED => Tmult_assoc_reduced
-  | C_MINUS => Tminus_def
-  | C_MULT_COMM => Tmult_comm
+Fixpoint fusion_cancel (t1 t2 : term) : term :=
+  match t1, t2 with
+  | (v1 * Tint x1 + l1)%term, (v2 * Tint x2 + l2)%term =>
+    if eq_term v1 v2 && beq x1 (-x2)
+    then fusion_cancel l1 l2
+    else (t1+t2)%term (* should not happen *)
+  | Tint x1, Tint x2 => Tint (x1+x2)
+  | _, _ => (t1+t2)%term (* should not happen *)
   end.
 
-Theorem t_rewrite_stable : forall s : step, term_stable (t_rewrite s).
+Theorem fusion_cancel_stable e t1 t2 :
+ interp_term e (t1+t2)%term = interp_term e (fusion_cancel t1 t2).
 Proof.
- simple induction s; simpl.
- - intros; apply apply_both_stable; auto.
- - intros; apply apply_left_stable; auto.
- - intros; apply apply_right_stable; auto.
- - unfold term_stable; intros; elim H0; apply H.
- - unfold term_stable; auto.
- - exact Topp_plus_stable.
- - exact Topp_opp_stable.
- - exact Topp_mult_r_stable.
- - exact Topp_one_stable.
- - exact reduce_stable.
- - exact Tmult_plus_distr_stable.
- - exact Tmult_opp_left_stable.
- - exact Tmult_assoc_r_stable.
- - exact Tplus_assoc_r_stable.
- - exact Tplus_assoc_l_stable.
- - exact Tplus_permute_stable.
- - exact Tplus_comm_stable.
- - exact Tred_factor0_stable.
- - exact Tred_factor1_stable.
- - exact Tred_factor2_stable.
- - exact Tred_factor3_stable.
- - exact Tred_factor4_stable.
- - exact Tred_factor5_stable.
- - exact Tred_factor6_stable.
- - exact Tmult_assoc_reduced_stable.
- - exact Tminus_def_stable.
- - exact Tmult_comm_stable.
+ revert t2. induction t1; destruct t2; simpl; Simplify; auto.
+ simpl in *.
+ rewrite <- IHt1_2.
+ apply OMEGA13.
 Qed.
 
 (* \subsection{tactiques de résolution d'un but omega normalisé}
@@ -1926,8 +1432,8 @@ Proof.
 Qed.
 
 (* \paragraph{[NOT_EXACT_DIVIDE]} *)
-Definition not_exact_divide (k1 k2 : int) (body : term)
-  (i : nat) (l : hyps) :=
+Definition not_exact_divide (i : nat) (k1 k2 : int) (body : term)
+  (l : hyps) :=
   match nth_hyps i l with
   | EqTerm (Tint Nul) b =>
       if beq Nul 0 &&
@@ -1940,8 +1446,8 @@ Definition not_exact_divide (k1 k2 : int) (body : term)
   end.
 
 Theorem not_exact_divide_valid :
- forall (k1 k2 : int) (body : term) (i : nat),
- valid_hyps (not_exact_divide k1 k2 body i).
+ forall (i : nat)(k1 k2 : int) (body : term),
+ valid_hyps (not_exact_divide i k1 k2 body).
 Proof.
  unfold valid_hyps, not_exact_divide; intros.
  generalize (nth_valid ep e i lp); Simplify.
@@ -2068,19 +1574,17 @@ Qed.
  preuve un peu compliquée. On utilise quelques lemmes qui sont des
  généralisations des théorèmes utilisés par OMEGA. *)
 
-Definition sum (k1 k2 : int) (trace : list t_fusion)
-  (prop1 prop2 : proposition) :=
+Definition sum (k1 k2 : int) (prop1 prop2 : proposition) :=
   match prop1 with
   | EqTerm (Tint Null) b1 =>
       match prop2 with
       | EqTerm (Tint Null') b2 =>
           if beq Null 0 && beq Null' 0
-          then EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
+          then EqTerm (Tint 0) (fusion b1 b2 k1 k2)
           else TrueTerm
       | LeqTerm (Tint Null') b2 =>
           if beq Null 0 && beq Null' 0 && bgt k2 0
-          then LeqTerm (Tint 0)
-                (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
+          then LeqTerm (Tint 0) (fusion b1 b2 k1 k2)
           else TrueTerm
       | _ => TrueTerm
       end
@@ -2089,13 +1593,11 @@ Definition sum (k1 k2 : int) (trace : list t_fusion)
       then match prop2 with
           | EqTerm (Tint Null') b2 =>
               if beq Null' 0 then
-              LeqTerm (Tint 0)
-                (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
+              LeqTerm (Tint 0) (fusion b1 b2 k1 k2)
               else TrueTerm
           | LeqTerm (Tint Null') b2 =>
               if beq Null' 0 && bgt k2 0
-              then LeqTerm (Tint 0)
-                    (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
+              then LeqTerm (Tint 0) (fusion b1 b2 k1 k2)
               else TrueTerm
           | _ => TrueTerm
           end
@@ -2104,8 +1606,7 @@ Definition sum (k1 k2 : int) (trace : list t_fusion)
       match prop2 with
       | EqTerm (Tint Null') b2 =>
           if beq Null 0 && beq Null' 0 && (negb (beq k1 0))
-          then NeqTerm (Tint 0)
-                 (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
+          then NeqTerm (Tint 0) (fusion b1 b2 k1 k2)
           else TrueTerm
       | _ => TrueTerm
       end
@@ -2114,11 +1615,11 @@ Definition sum (k1 k2 : int) (trace : list t_fusion)
 
 
 Theorem sum_valid :
- forall (k1 k2 : int) (t : list t_fusion), valid2 (sum k1 k2 t).
+ forall (k1 k2 : int), valid2 (sum k1 k2).
 Proof.
  unfold valid2; intros k1 k2 t ep e p1 p2; unfold sum;
- Simplify; simpl; auto; try elim (fusion_stable t);
- simpl; intros.
+ Simplify; simpl; rewrite <- ?fusion_stable;
+ simpl; intros; auto.
  - apply sum1; assumption.
  - apply sum2; try assumption; apply sum4; assumption.
  - rewrite plus_comm; apply sum2; try assumption; apply sum4; assumption.
@@ -2227,25 +1728,25 @@ Qed.
 
 (* \paragraph{[O_STATE]} *)
 
-Definition state (m : int) (s : step) (prop1 prop2 : proposition) :=
+Definition state (m : int) (prop1 prop2 : proposition) :=
   match prop1 with
   | EqTerm (Tint Null) b1 =>
       match prop2 with
-      | EqTerm b2 b3 =>
-          if beq Null 0
-          then EqTerm (Tint 0) (t_rewrite s (b1 + (- b3 + b2) * Tint m)%term)
+      | EqTerm (Tint Null') b2 =>
+          if beq Null 0 && beq Null' 0
+          then EqTerm (Tint 0) (fusion b1 b2 1 m)
           else TrueTerm
       | _ => TrueTerm
       end
   | _ => TrueTerm
   end.
 
-Theorem state_valid : forall (m : int) (s : step), valid2 (state m s).
+Theorem state_valid : forall (m : int), valid2 (state m).
 Proof.
- unfold valid2; intros m s ep e p1 p2; unfold state; Simplify;
- simpl; auto; elim (t_rewrite_stable s e); simpl;
- intros H1 H2; elim H1.
- now rewrite H2, plus_opp_l, plus_0_l, mult_0_l.
+ unfold valid2; intros m ep e p1 p2.
+ unfold state; Simplify; simpl; auto.
+ rewrite <- fusion_stable. simpl in *. intros H H'.
+ rewrite <- H, <- H'. now rewrite !mult_0_l, plus_0_l.
 Qed.
 
 (* \subsubsection{Tactiques générant plusieurs but}
@@ -2288,14 +1789,14 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
   match t with
   | O_CONSTANT_NOT_NUL n => singleton (constant_not_nul n l)
   | O_CONSTANT_NEG n => singleton (constant_neg n l)
-  | O_DIV_APPROX k1 k2 body cont n =>
+  | O_DIV_APPROX n k1 k2 body cont =>
       execute_omega cont (apply_oper_1 n (divide_and_approx k1 k2 body) l)
-  | O_NOT_EXACT_DIVIDE k1 k2 body i =>
-      singleton (not_exact_divide k1 k2 body i l)
-  | O_EXACT_DIVIDE k body cont n =>
+  | O_NOT_EXACT_DIVIDE i k1 k2 body =>
+      singleton (not_exact_divide i k1 k2 body l)
+  | O_EXACT_DIVIDE n k body cont =>
       execute_omega cont (apply_oper_1 n (exact_divide k body) l)
-  | O_SUM k1 i1 k2 i2 t cont =>
-      execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2 t) l)
+  | O_SUM k1 i1 k2 i2 cont =>
+      execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2) l)
   | O_CONTRADICTION i j => singleton (contradiction i j l)
   | O_MERGE_EQ i1 i2 cont =>
       execute_omega cont (apply_oper_2 i1 i2 merge_eq l)
@@ -2305,8 +1806,8 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
   | O_NEGATE_CONTRADICT i j => singleton (negate_contradict i j l)
   | O_NEGATE_CONTRADICT_INV i j =>
       singleton (negate_contradict_inv i j l)
-  | O_STATE m s i1 i2 cont =>
-      execute_omega cont (apply_oper_2 i1 i2 (state m s) l)
+  | O_STATE m i1 i2 cont =>
+      execute_omega cont (apply_oper_2 i1 i2 (state m) l)
   end.
 
 Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr).
@@ -2317,21 +1818,21 @@ Proof.
  - unfold valid_list_hyps; simpl; intros; left;
     apply (constant_neg_valid n ep e lp H).
  - unfold valid_list_hyps, valid_hyps;
-    intros k1 k2 body t' Ht' m ep e lp H; apply Ht';
+    intros m k1 k2 body t' Ht' ep e lp H; apply Ht';
     apply
      (apply_oper_1_valid m (divide_and_approx k1 k2 body)
         (divide_and_approx_valid k1 k2 body) ep e lp H).
  - unfold valid_list_hyps; simpl; intros; left;
     apply (not_exact_divide_valid _ _ _ _ ep e lp H).
  - unfold valid_list_hyps, valid_hyps;
-    intros k body t' Ht' m ep e lp H; apply Ht';
+    intros m k body t' Ht' ep e lp H; apply Ht';
     apply
      (apply_oper_1_valid m (exact_divide k body)
         (exact_divide_valid k body) ep e lp H).
  - unfold valid_list_hyps, valid_hyps;
-    intros k1 i1 k2 i2 trace t' Ht' ep e lp H; apply Ht';
+    intros k1 i1 k2 i2 t' Ht' ep e lp H; apply Ht';
     apply
-     (apply_oper_2_valid i1 i2 (sum k1 k2 trace) (sum_valid k1 k2 trace) ep e
+     (apply_oper_2_valid i1 i2 (sum k1 k2) (sum_valid k1 k2) ep e
         lp H).
  - unfold valid_list_hyps; simpl; intros; left.
     apply (contradiction_valid n n0 ep e lp H).
@@ -2352,164 +1853,98 @@ Proof.
  - unfold valid_list_hyps; simpl; intros i j ep e lp H;
     left; apply (negate_contradict_inv_valid i j ep e lp H).
  - unfold valid_list_hyps, valid_hyps;
-    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).
+    intros m i1 i2 t' Ht' ep e lp H; apply Ht';
+    apply (apply_oper_2_valid i1 i2 (state m) (state_valid m) ep e lp H).
 Qed.
 
-
 (* \subsection{Les opérations globales sur le but}
    \subsubsection{Normalisation} *)
 
-Definition move_right (s : step) (p : proposition) :=
+Fixpoint normalize_prop (negated:bool)(p:proposition) :=
   match p with
-  | EqTerm t1 t2 => EqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term)
-  | LeqTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t2 + - t1)%term)
-  | GeqTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term)
-  | LtTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t2 + Tint (-(1)) + - t1)%term)
-  | GtTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t1 + Tint (-(1)) + - t2)%term)
-  | NeqTerm t1 t2 => NeqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term)
-  | p => p
-  end.
-
-Definition prop_stable (f : proposition -> proposition) :=
-  forall (ep : list Prop) (e : list int) (p : proposition),
-  interp_proposition ep e p <-> interp_proposition ep e (f p).
-
-Definition p_apply_left (f : proposition -> proposition)
-  (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).
-Proof.
- unfold prop_stable; intros f H ep e p; split;
- (case p; simpl; 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).
-Proof.
- unfold prop_stable; intros f H ep e p.
- case p; simpl; try tauto.
- - intros p1; rewrite (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).
-Proof.
- unfold prop_stable; intros f H ep e p.
- case p; simpl; try tauto; intros t1 t2; rewrite <- (H ep e); simpl.
- - generalize (dec_eq (interp_term e t1) (interp_term e t2));
-   unfold decidable; try tauto.
- - generalize (dec_gt (interp_term e t1) (interp_term e t2));
-   unfold decidable; rewrite le_lt_iff, <- gt_lt_iff; tauto.
- - generalize (dec_lt (interp_term e t1) (interp_term e t2));
-   unfold decidable; rewrite ge_le_iff, le_lt_iff; tauto.
- - generalize (dec_gt (interp_term e t1) (interp_term e t2));
-   unfold decidable; rewrite ?le_lt_iff, ?gt_lt_iff; tauto.
- - generalize (dec_lt (interp_term e t1) (interp_term e t2));
-   unfold decidable; rewrite ?ge_le_iff, ?le_lt_iff; tauto.
- - reflexivity.
-Qed.
-
-Theorem move_right_stable : forall s : step, prop_stable (move_right s).
-Proof.
- unfold move_right, prop_stable; intros s ep e p; split.
- - Simplify; simpl; elim (t_rewrite_stable s e); simpl.
-    + symmetry ; apply egal_left; assumption.
-    + intro; apply le_left; assumption.
-    + intro; apply le_left; rewrite <- ge_le_iff; assumption.
-    + intro; apply lt_left; rewrite <- gt_lt_iff; assumption.
-    + intro; apply lt_left; assumption.
-    + intro; apply ne_left_2; assumption.
- - case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s);
-   simpl; intro H1.
-   + rewrite (plus_0_r_reverse (interp_term e t1)); rewrite H1;
-     now rewrite plus_permute, plus_opp_r, plus_0_r.
-   + apply (fun a b => plus_le_reg_r a b (- interp_term e t0));
-     rewrite plus_opp_r; assumption.
-   + rewrite ge_le_iff;
-     apply (fun a b => plus_le_reg_r a b (- interp_term e t1));
-     rewrite plus_opp_r; assumption.
-   + rewrite gt_lt_iff; apply lt_left_inv; assumption.
-   + apply lt_left_inv; assumption.
-   + unfold not; intro H2; apply H1;
-     rewrite H2, plus_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)
-  end.
-
-Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s).
-Proof.
- simple induction s; simpl.
- - 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.
-Qed.
-
-Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps :=
-  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).
-Proof.
- simple induction l; unfold valid_hyps; simpl.
- - 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; 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 : list Prop) (env : list int) (l : hyps),
- interp_goal ep env (normalize_hyps s l) -> interp_goal ep env l.
+  | EqTerm t1 t2 =>
+    if negated then Tnot (NeqTerm (Tint 0) (normalize (t1-t2)))
+    else EqTerm (Tint 0) (normalize (t1-t2))
+  | NeqTerm t1 t2 =>
+    if negated then Tnot (EqTerm (Tint 0) (normalize (t1-t2)))
+    else NeqTerm (Tint 0) (normalize (t1-t2))
+  | LeqTerm t1 t2 =>
+    if negated then Tnot (LeqTerm (Tint 0) (normalize (t1-t2+Tint (-(1)))))
+    else LeqTerm (Tint 0) (normalize (t2-t1))
+  | GeqTerm t1 t2 =>
+    if negated then Tnot (LeqTerm (Tint 0) (normalize (t2-t1+Tint (-(1)))))
+    else LeqTerm (Tint 0) (normalize (t1-t2))
+  | LtTerm t1 t2 =>
+    if negated then Tnot (LeqTerm (Tint 0) (normalize (t1-t2)))
+    else LeqTerm (Tint 0) (normalize (t2-t1+Tint (-(1))))
+  | GtTerm t1 t2 =>
+    if negated then Tnot (LeqTerm (Tint 0) (normalize (t2-t1)))
+    else LeqTerm (Tint 0) (normalize (t1-t2+Tint (-(1))))
+  | Tnot p => Tnot (normalize_prop (negb negated) p)
+  | Tor p p' => Tor (normalize_prop negated p) (normalize_prop negated p')
+  | Tand p p' => Tand (normalize_prop negated p) (normalize_prop negated p')
+  | Timp p p' => Timp (normalize_prop (negb negated) p)
+                      (normalize_prop negated p')
+  | Tprop _ | TrueTerm | FalseTerm => p
+  end.
+
+Definition normalize_hyps := List.map (normalize_prop false).
+
+Opaque normalize.
+
+Theorem normalize_prop_valid b e ep p :
+  interp_proposition e ep p <->
+  interp_proposition e ep (normalize_prop b p).
+Proof.
+ revert b.
+ induction p; intros; simpl; try tauto.
+ - destruct b; simpl;
+   rewrite <- ?normalize_stable; simpl; rewrite ?minus_def.
+   + rewrite not_eq. apply egal_left_iff.
+   + apply egal_left_iff.
+ - destruct b; simpl;
+   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
+   + rewrite le_lt_iff. apply not_iff_compat.
+     rewrite le_lt_int. rewrite le_left.
+     rewrite <- !plus_assoc. now rewrite (plus_comm (-(1))).
+   + apply le_left.
+ - now rewrite <- IHp.
+ - destruct b; simpl;
+   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
+   + rewrite ge_le_iff, le_lt_iff. apply not_iff_compat.
+     rewrite le_lt_int. rewrite le_left.
+     rewrite <- !plus_assoc. now rewrite (plus_comm (-(1))).
+   + rewrite ge_le_iff. apply le_left.
+ - destruct b; simpl;
+   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
+   + rewrite gt_lt_iff, lt_le_iff. apply not_iff_compat.
+     apply le_left.
+   + rewrite gt_lt_iff. rewrite le_lt_int. rewrite le_left.
+     rewrite <- !plus_assoc. now rewrite (plus_comm (-(1))).
+ - destruct b; simpl;
+   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
+   + rewrite lt_le_iff. apply not_iff_compat.
+     apply le_left.
+   + rewrite le_lt_int, le_left.
+     rewrite <- !plus_assoc. now rewrite (plus_comm (-(1))).
+ - destruct b; simpl;
+   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def;
+   apply not_iff_compat, egal_left_iff.
+ - now rewrite <- IHp1, <- IHp2.
+ - now rewrite <- IHp1, <- IHp2.
+ - now rewrite <- IHp1, <- IHp2.
+Qed.
+
+Transparent normalize.
+
+Theorem normalize_hyps_valid : valid_hyps normalize_hyps.
+Proof.
+ intros e ep l. induction l; simpl; intuition.
+ now rewrite <- normalize_prop_valid.
+Qed.
+
+Theorem normalize_hyps_goal (ep : list Prop) (env : list int) (l : hyps) :
+ interp_goal ep env (normalize_hyps l) -> interp_goal ep env l.
 Proof.
  intros; apply valid_goal with (2 := H); apply normalize_hyps_valid.
 Qed.
@@ -2692,19 +2127,20 @@ Proof.
  - simpl in *; tauto.
 Qed.
 
-Definition omega_tactic (t1 : e_step) (t2 : list h_step)
-  (c : proposition) (l : hyps) :=
-  reduce_lhyps (decompose_solve t1 (normalize_hyps t2 (concl_to_hyp c :: l))).
+Definition omega_tactic (t1 : e_step) (c : proposition) (l : hyps) :=
+  reduce_lhyps (decompose_solve t1 (normalize_hyps (concl_to_hyp c :: l))).
 
 Theorem do_omega :
- forall (t1 : e_step) (t2 : list h_step) (envp : list Prop)
+ forall (t : e_step) (envp : list Prop)
    (env : list int) (c : proposition) (l : hyps),
- interp_list_goal envp env (omega_tactic t1 t2 c l) ->
+ interp_list_goal envp env (omega_tactic t c l) ->
  interp_goal_concl c envp env l.
 Proof.
- unfold omega_tactic; intros; apply do_concl_to_hyp;
- apply (normalize_hyps_goal t2); apply (decompose_solve_valid t1);
- apply do_reduce_lhyps; assumption.
+ unfold omega_tactic; intros t ep e c l H.
+ apply do_concl_to_hyp.
+ apply normalize_hyps_goal.
+ apply (decompose_solve_valid t).
+ now apply do_reduce_lhyps.
 Qed.
 
 End IntOmega.
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index d7faaac96..4fd224e2b 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -79,13 +79,6 @@ let coq_I = lazy(init_constant "I")
 
 (* ReflOmegaCore/ZOmega *)
 
-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_t_int = lazy (constant  "Tint")
 let coq_t_plus = lazy (constant  "Tplus")
 let coq_t_mult = lazy (constant  "Tmult")
@@ -108,43 +101,6 @@ let coq_p_and = lazy (constant  "Tand")
 let coq_p_imp = lazy (constant  "Timp")
 let coq_p_prop = lazy (constant  "Tprop")
 
-(* Constructors for shuffle tactic *)
-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_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_comm = lazy (constant  "C_PLUS_COMM")
-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 (constant  "C_MULT_ASSOC_REDUCED")
-let coq_c_minus = lazy (constant  "C_MINUS")
-let coq_c_mult_comm = lazy (constant  "C_MULT_COMM")
-
 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")
@@ -171,31 +127,6 @@ let coq_e_solve = lazy  (constant  "E_SOLVE")
 let coq_interp_sequent = lazy (constant  "interp_goal_concl")
 let coq_do_omega = lazy (constant  "do_omega")
 
-(* \subsection{Construction d'expressions} *)
-
-let do_left t =
-  if Term.eq_constr t (Lazy.force coq_c_nop) then Lazy.force coq_c_nop
-  else Term.mkApp (Lazy.force coq_c_do_left, [|t |] )
-
-let do_right t =
-  if Term.eq_constr t (Lazy.force coq_c_nop) then Lazy.force coq_c_nop
-  else Term.mkApp (Lazy.force coq_c_do_right, [|t |])
-
-let do_both t1 t2 =
-  if Term.eq_constr t1 (Lazy.force coq_c_nop) then do_right t2
-  else if Term.eq_constr t2 (Lazy.force coq_c_nop) then do_left t1
-  else Term.mkApp (Lazy.force coq_c_do_both , [|t1; t2 |])
-
-let do_seq t1 t2 =
-  if Term.eq_constr t1 (Lazy.force coq_c_nop) then t2
-  else if Term.eq_constr t2 (Lazy.force coq_c_nop) then t1
-  else Term.mkApp (Lazy.force coq_c_do_seq, [|t1; t2 |])
-
-let rec do_list = function
-  | [] -> Lazy.force coq_c_nop
-  | [x] -> x
-  | (x::l) -> do_seq x (do_list l)
-
 (* Nat *)
 
 let coq_S = lazy(init_constant "S")
@@ -232,8 +163,6 @@ let mk_plist =
     fun l -> mk_list type1lev Term.mkProp l
 
 let mk_list = mk_list Univ.Level.set
-let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l
-
 
 type parse_term =
   | Tplus of Term.constr * Term.constr
@@ -306,7 +235,7 @@ module type Int = sig
   val parse_term : Term.constr -> parse_term
   val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
   (* check whether t is built only with numbers and + * - *)
-  val is_scalar : Term.constr -> bool
+  val get_scalar : Term.constr -> Bigint.bigint option
 end
 
 module Z : Int = struct
@@ -376,11 +305,18 @@ let parse_rel gl t =
   | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2)
   | _ -> parse_logic_rel t
 
-let rec is_scalar t =
+let rec get_scalar t =
   match destructurate t with
-  | Kapp(("Z.add"|"Z.sub"|"Z.mul"),[t1;t2]) -> is_scalar t1 && is_scalar t2
-  | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> is_scalar t
-  | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> Option.has_some (recognize_Z t)
-  | _ -> false
+  | Kapp("Z.add", [t1;t2]) ->
+     Option.lift2 Bigint.add (get_scalar t1) (get_scalar t2)
+  | Kapp ("Z.sub",[t1;t2]) ->
+     Option.lift2 Bigint.sub (get_scalar t1) (get_scalar t2)
+  | Kapp ("Z.mul",[t1;t2]) ->
+     Option.lift2 Bigint.mult (get_scalar t1) (get_scalar t2)
+  | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar t)
+  | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar t)
+  | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar t)
+  | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z t
+  | _ -> None
 
 end
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 2901cc028..787ace603 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -19,12 +19,6 @@ val coq_False : Term.constr lazy_t
 val coq_I : Term.constr lazy_t
 
 (* from ReflOmegaCore/ZOmega *)
-val coq_h_step : Term.constr lazy_t
-val coq_pair_step : Term.constr lazy_t
-val coq_p_left : Term.constr lazy_t
-val coq_p_right : Term.constr lazy_t
-val coq_p_invert : Term.constr lazy_t
-val coq_p_step : Term.constr lazy_t
 
 val coq_t_int : Term.constr lazy_t
 val coq_t_plus : Term.constr lazy_t
@@ -48,40 +42,6 @@ val coq_p_and : Term.constr lazy_t
 val coq_p_imp : Term.constr lazy_t
 val coq_p_prop : Term.constr lazy_t
 
-val coq_f_equal : Term.constr lazy_t
-val coq_f_cancel : Term.constr lazy_t
-val coq_f_left : Term.constr lazy_t
-val coq_f_right : Term.constr lazy_t
-
-val coq_c_do_both : Term.constr lazy_t
-val coq_c_do_left : Term.constr lazy_t
-val coq_c_do_right : Term.constr lazy_t
-val coq_c_do_seq : Term.constr lazy_t
-val coq_c_nop : Term.constr lazy_t
-val coq_c_opp_plus : Term.constr lazy_t
-val coq_c_opp_opp : Term.constr lazy_t
-val coq_c_opp_mult_r : Term.constr lazy_t
-val coq_c_opp_one : Term.constr lazy_t
-val coq_c_reduce : Term.constr lazy_t
-val coq_c_mult_plus_distr : Term.constr lazy_t
-val coq_c_opp_left : Term.constr lazy_t
-val coq_c_mult_assoc_r : Term.constr lazy_t
-val coq_c_plus_assoc_r : Term.constr lazy_t
-val coq_c_plus_assoc_l : Term.constr lazy_t
-val coq_c_plus_permute : Term.constr lazy_t
-val coq_c_plus_comm : Term.constr lazy_t
-val coq_c_red0 : Term.constr lazy_t
-val coq_c_red1 : Term.constr lazy_t
-val coq_c_red2 : Term.constr lazy_t
-val coq_c_red3 : Term.constr lazy_t
-val coq_c_red4 : Term.constr lazy_t
-val coq_c_red5 : Term.constr lazy_t
-val coq_c_red6 : Term.constr lazy_t
-val coq_c_mult_opp_left : Term.constr lazy_t
-val coq_c_mult_assoc_reduced : Term.constr lazy_t
-val coq_c_minus : Term.constr lazy_t
-val coq_c_mult_comm : Term.constr lazy_t
-
 val coq_s_constant_not_nul : Term.constr lazy_t
 val coq_s_constant_neg : Term.constr lazy_t
 val coq_s_div_approx : Term.constr lazy_t
@@ -107,21 +67,12 @@ val coq_e_solve : Term.constr lazy_t
 val coq_interp_sequent : Term.constr lazy_t
 val coq_do_omega : Term.constr lazy_t
 
-(** Building expressions *)
-
-val do_left : Term.constr -> Term.constr
-val do_right : Term.constr -> Term.constr
-val do_both : Term.constr -> Term.constr -> Term.constr
-val do_seq : Term.constr -> Term.constr -> Term.constr
-val do_list : Term.constr list -> Term.constr
-
 val mk_nat : int -> Term.constr
 val mk_N : int -> Term.constr
 
 (** Precondition: the type of the list is in Set *)
 val mk_list : Term.constr -> Term.constr list -> Term.constr
 val mk_plist : Term.types list -> Term.types
-val mk_shuffle_list : Term.constr list -> Term.constr
 
 (** Analyzing a coq term *)
 
@@ -171,7 +122,7 @@ module type Int =
     (* parsing a relation expression, including = < <= >= > *)
     val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
     (* Is a particular term only made of numbers and + * - ? *)
-    val is_scalar : Term.constr -> bool
+    val get_scalar : Term.constr -> Bigint.bigint option
   end
 
 (* Currently, we only use Z numbers *)
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index a0ed68a8a..7b63d5503 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -46,19 +46,19 @@ type occ_path = occ_step list
    d'une liste de pas à partir de la racine de l'hypothèse *)
 type occurrence = {o_hyp : Id.t; o_path : occ_path}
 
+type atom_index = int
+
 (* \subsection{reifiable formulas} *)
 type oformula =
     (* integer *)
   | Oint of Bigint.bigint
     (* recognized binary and unary operations *)
   | Oplus of oformula * oformula
-  | Omult of oformula * oformula
+  | Omult of oformula * oformula (* Invariant : one side is [Oint] *)
   | Ominus of oformula * oformula
   | Oopp of  oformula
     (* an atom in the environment *)
-  | Oatom of int
-    (* weird expression that cannot be translated *)
-  | Oufo of oformula
+  | Oatom of atom_index
 
 (* Operators for comparison recognized by Omega *)
 type comparaison = Eq | Leq | Geq | Gt | Lt | Neq
@@ -83,7 +83,6 @@ 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: occurrence;		(* l'hypothèse dont vient le terme *)
     e_negated: bool;			(* vrai si apparait en position nié
 					   après normalisation *)
@@ -108,7 +107,7 @@ type environment = {
   (* La meme chose pour les propositions *)
   mutable props : Term.constr list;
   (* Les variables introduites par omega *)
-  mutable om_vars : (oformula * int) list;
+  mutable om_vars : (int * oformula) 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 IntHtbl.t;
@@ -155,7 +154,6 @@ let rec oform_eq f f' = match f,f' with
   | Ominus (f1,f2), Ominus (f1',f2') -> oform_eq f1 f1' && oform_eq f2 f2'
   | Oopp f, Oopp f' -> oform_eq f f'
   | Oatom a, Oatom a' -> Int.equal a a'
-  | Oufo f, Oufo f' -> oform_eq f f'
   | _ -> false
 
 let dir_eq d d' = match d, d' with
@@ -201,42 +199,38 @@ let print_env_reification env =
 (* generation d'identifiant d'equation pour Omega *)
 
 let new_omega_eq, rst_omega_eq =
-  let cpt = ref 0 in
+  let cpt = ref (-1) in
   (function () -> incr cpt; !cpt),
-  (function () -> cpt:=0)
+  (function () -> cpt:=(-1))
 
 (* generation d'identifiant de variable pour Omega *)
 
 let new_omega_var, rst_omega_var =
-  let cpt = ref 0 in
+  let cpt = ref (-1) in
   (function () -> incr cpt; !cpt),
-  (function () -> cpt:=0)
+  (function () -> cpt:=(-1))
 
 (* Affichage des variables d'un système *)
 
 let display_omega_var i = Printf.sprintf "OV%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) *)
+(* Register a new internal variable corresponding to some oformula
+   (normally an [Oatom]). *)
 
-let intern_omega env t =
-  try List.assoc_f oform_eq t env.om_vars
-  with Not_found ->
-    let v = new_omega_var () in
-    env.om_vars <- (t,v) :: env.om_vars; v
+let add_omega_var env t =
+  let v = new_omega_var () in
+  env.om_vars <- (v,t) :: env.om_vars
 
 (* Ajout forcé d'un lien entre un terme et une variable  Cas où la
    variable est créée par Omega et où il faut la lier après coup à un atome
    réifié introduit de force *)
-let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars
+let force_omega_var env t v =
+  env.om_vars <- (v,t) :: env.om_vars
 
-(* Récupère le terme associé à une variable *)
-let unintern_omega env id =
-  let rec loop = function
-    | [] -> failwith "unintern"
-    | ((t,j)::l) -> if Int.equal id j then t else loop l in
-  loop env.om_vars
+(* Récupère le terme associé à une variable omega *)
+let unintern_omega env v =
+  try List.assoc_f Int.equal v env.om_vars
+  with Not_found -> failwith "unintern_omega"
 
 (* \subsection{Gestion des environnements de variable pour la réflexion}
    Gestion des environnements de traduction entre termes des constructions
@@ -244,10 +238,12 @@ let unintern_omega env id =
    l'environnement initial contenant tout. Il faudra le réduire après
    calcul des variables utiles. *)
 
-let add_reified_atom t env =
+let add_reified_atom sync t env =
   try List.index0 Term.eq_constr t env.terms
   with Not_found ->
     let i = List.length env.terms in
+    (* synchronize atom indexes and omega variables *)
+    let () = if sync then add_omega_var env (Oatom i) in
     env.terms <- env.terms @ [t]; i
 
 let get_reified_atom env =
@@ -284,7 +280,6 @@ let rec oprint ch = function
   | 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 print_comp = function
   | Eq -> "=" | Leq -> "<=" | Geq -> ">="
@@ -301,31 +296,6 @@ let rec pprint ch = function
   | 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} *)
-
-(* \subsection{Oformula vers Omega} *)
-
-let omega_of_oformula env kind =
-  let rec loop accu = function
-    | Oplus(Omult(v,Oint n),r) ->
-       loop ({v=intern_omega env v; c=n} :: accu) r
-    | Oint n ->
-       let id = new_omega_eq () in
-       (*i tag_equation name id; i*)
-       {kind = kind; body = List.rev accu;
-       constant = n; id = id}
-    | t -> print_string "CO"; oprint stdout t; failwith "compile_equation" in
-  loop []
-
 (* \subsection{Omega vers Oformula} *)
 
 let oformula_of_omega env af =
@@ -345,7 +315,6 @@ let coq_of_formula env t =
   | Oopp t -> app Z.opp [| loop t |]
   | Omult(t1,t2) -> app Z.mult [| loop t1; loop t2 |]
   | Oint v ->   Z.mk v
-  | Oufo t -> loop t
   | Oatom var ->
       (* attention ne traite pas les nouvelles variables si on ne les
        * met pas dans env.term *)
@@ -362,53 +331,49 @@ let reified_of_atom env i =
     IntHtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices;
     raise Not_found
 
-let rec reified_of_formula env = function
-  | Oplus (t1,t2) ->
-      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 [| Z.mk v |]
-  | Oufo t -> reified_of_formula env t
+let reified_binop = function
+  | Oplus _ -> app coq_t_plus
+  | Ominus _ -> app coq_t_minus
+  | Omult _ -> app coq_t_mult
+  | _ -> assert false
+
+let rec reified_of_formula env t = match t with
+  | Oplus (t1,t2) | Omult (t1,t2) | Ominus (t1,t2) ->
+     reified_binop t [| reified_of_formula env t1; reified_of_formula env t2 |]
+  | Oopp t -> app coq_t_opp [| reified_of_formula env t |]
+  | Oint v -> app coq_t_int [| Z.mk v |]
   | Oatom i -> app coq_t_var [| mk_N (reified_of_atom env i) |]
-  | Ominus(t1,t2) ->
-      app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |]
 
 let reified_of_formula env f =
   try reified_of_formula env f
   with reraise -> oprint stderr f; raise reraise
 
-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 |]
+let reified_cmp = function
+  | Eq -> app coq_p_eq
+  | Leq -> app coq_p_leq
+  | Geq -> app coq_p_geq
+  | Gt -> app coq_p_gt
+  | Lt -> app coq_p_lt
+  | Neq -> app coq_p_neq
+
+let reified_conn = function
+  | Por _ -> app coq_p_or
+  | Pand _ -> app coq_p_and
+  | Pimp _ -> app coq_p_imp
+  | _ -> assert false
+
+let rec reified_of_oprop env t = match t with
+  | Pequa (_,{ e_comp=cmp; e_left=t1; e_right=t2 }) ->
+     reified_cmp cmp [| 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 |]
+  | Pnot t -> app coq_p_not [| reified_of_oprop env t |]
+  | Por (_,t1,t2) | Pand (_,t1,t2) | Pimp (_,t1,t2) ->
+     reified_conn t [| reified_of_oprop env t1; reified_of_oprop env t2 |]
   | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |]
 
 let reified_of_proposition env f =
-  try reified_of_proposition env f
+  try reified_of_oprop env f
   with reraise -> pprint stderr f; raise reraise
 
 (* \subsection{Omega vers COQ réifié} *)
@@ -445,7 +410,6 @@ let rec vars_of_formula = function
   | Ominus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
   | Oopp e -> vars_of_formula e
   | Oatom i -> IntSet.singleton i
-  | Oufo _ -> IntSet.empty
 
 let rec vars_of_equations = function
   | [] -> IntSet.empty
@@ -462,241 +426,99 @@ let rec vars_of_prop = function
   | Pimp(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
   | Pprop _ | Ptrue | Pfalse -> IntSet.empty
 
-(* \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')
- | Oopp t ->
-     do_list [Lazy.force coq_c_mult_opp_left], Omult(t,Oint(Bigint.neg n))
- | Omult(t1,Oint x) ->
-     do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x))
- | Omult(t1,t2) ->
-     CErrors.error "Omega: Can't solve a goal with non-linear products"
- | (Oatom _ as t) -> do_list [], Omult(t,Oint n)
- | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i)
- | (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')
- | Oopp t ->
-     do_list [Lazy.force coq_c_opp_opp], t
- | Omult(t1,Oint x) ->
-     do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x))
- | Omult(t1,t2) ->
-     CErrors.error "Omega: Can't solve a goal with non-linear products"
- | (Oatom _ as t) ->
-     do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone))
- | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i)
- | Oufo c -> do_list [], Oufo (Oopp c)
- | Ominus _ -> failwith "negate minus"
-
-let norm l = (List.length l)
-
-(* \subsection{Mélange (fusion) de deux équations} *)
-(* \subsubsection{Version avec coefficients} *)
-let shuffle_path k1 e1 k2 e2 =
-  let rec loop = function
-      (({c=c1;v=v1}::l1) as l1'),
-      (({c=c2;v=v2}::l2) as l2') ->
-	if Int.equal v1 v2 then
-          if Bigint.equal (k1 * c1 + k2 * c2) zero then (
-            Lazy.force coq_f_cancel :: loop (l1,l2))
-          else (
-            Lazy.force coq_f_equal :: loop (l1,l2) )
-	else if v1 > v2 then (
-	  Lazy.force coq_f_left :: loop(l1,l2'))
-	else (
-	  Lazy.force coq_f_right :: loop(l1',l2))
-    | ({c=c1;v=v1}::l1), [] ->
-	  Lazy.force coq_f_left :: loop(l1,[])
-    | [],({c=c2;v=v2}::l2) ->
-	  Lazy.force coq_f_right :: loop([],l2)
-    | [],[] -> flush stdout; [] in
-  mk_shuffle_list (loop (e1,e2))
-
-(* \subsubsection{Version sans coefficients} *)
-let rec shuffle env (t1,t2) =
-  match t1,t2 with
-    Oplus(l1,r1), Oplus(l2,r2) ->
-      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 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 env l1 > weight env t2 then
-        let (l_action,t') = shuffle env (r1,t2) in
-	do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action],Oplus(l1, t')
-      else do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1)
-  | t1,Oplus(l2,r2) ->
-      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)
-  | Oint t1,Oint t2 ->
-      do_list [Lazy.force coq_c_reduce], Oint(t1+t2)
-  | t1,t2 ->
-      if weight env t1 < weight env t2 then
-	do_list [Lazy.force coq_c_plus_comm], 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, Omult(Oatom v,Oint two)
-   | Oatom v, Omult(_,c2) ->
-       Lazy.force coq_c_red2, Omult(Oatom v,Oplus(c2,Oint one))
-   | Omult (v1,c1),Oatom v ->
-       Lazy.force coq_c_red3, Omult(Oatom v,Oplus(c1,Oint one))
-   | Omult (Oatom v,c1),Omult (v2,c2) ->
-       Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2))
-   | t1,t2 ->
-       oprint stdout t1; print_newline (); oprint stdout t2; print_newline ();
-       flush Pervasives.stdout; CErrors.error "shrink.1"
-  end
-
-(* \subsection{Calcul d'une sous formule constante} *)
-
-let reduce_factor = function
-   Oatom v ->
-     let r = Omult(Oatom v,Oint one) in
-       [Lazy.force coq_c_red0],r
-  | Omult(Oatom v,Oint n) as f -> [],f
-  | Omult(Oatom v,c) ->
-      let rec compute = function
-          Oint n -> n
-	| Oplus(t1,t2) -> compute t1 + compute t2
-	| _ -> CErrors.error "condense.1" in
-	[Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c))
-  | t -> CErrors.error "reduce_factor.1"
-
-(* \subsection{Réordonnancement} *)
-
-let rec condense env = function
-    Oplus(f1,(Oplus(f2,r) as t)) ->
-      if Int.equal (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 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 env t in
-	[do_both (do_list tac) (do_list tac')], Oplus(f,t')
-      end
-  | Oplus(f1,Oint n) ->
-      let tac,f1' = reduce_factor f1 in
-      [do_left (do_list tac)],Oplus(f1',Oint n)
-  | Oplus(f1,f2) ->
-      if Int.equal (weight env f1) (weight env f2) then begin
-	let tac_shrink,t = shrink_pair f1 f2 in
-	let tac,t' = condense env t in
-	tac_shrink :: tac,t'
-      end else begin
-	let tac,f = reduce_factor f1 in
-	let tac',t' = condense env f2 in
-	[do_both (do_list tac) (do_list tac')],Oplus(f,t')
-      end
-  | (Oint _ as t)-> [],t
-  | t ->
-      let tac,t' = reduce_factor t in
-      let final = Oplus(t',Oint zero) in
-      tac @ [Lazy.force coq_c_red6], final
-
-(* \subsection{Elimination des zéros} *)
-
-let rec clear_zero = function
-   Oplus(Omult(Oatom v,Oint n),r) when Bigint.equal n zero ->
-     let tac',t = clear_zero r in
-     Lazy.force coq_c_red5 :: tac',t
-  | Oplus(f,r) ->
-      let tac,t = clear_zero r in
-      (if List.is_empty tac then [] else [do_right (do_list tac)]),Oplus(f,t)
-  | t -> [],t;;
-
-(* \subsection{Transformation des hypothèses} *)
-
-let rec reduce env = function
-    Oplus(t1,t2) ->
-      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 env (Oplus(t1, Oopp t2)) in
-      t, do_list [Lazy.force coq_c_minus; trace]
-  | Omult(t1,t2) as t ->
-      let t1', trace1 = reduce env t1 in
-      let t2', trace2 = reduce env t2 in
-      begin match t1',t2' with
-      | (_, Oint n) ->
-	  let tac,t' = scalar n t1' in
-	  t', do_list [do_both trace1 trace2; tac]
-      | (Oint n,_) ->
-	  let tac,t' = scalar n t2' in
-	  t', do_list [do_both trace1 trace2; Lazy.force coq_c_mult_comm; tac]
-      | _ -> Oufo t, Lazy.force coq_c_nop
-      end
-  | Oopp t ->
-      let t',trace = reduce env  t in
-      let trace',t'' = negate t' in
-      t'', do_list [do_left trace; trace']
-  | (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
-
-(* Cette fonction reproduit très exactement le comportement de [p_invert] *)
+(* Normalized formulas :
+
+   - sorted list of monomials, largest index first,
+     with non-null coefficients
+   - a constant coefficient
+
+   /!\ Keep in sync with the corresponding functions in ReflOmegaCore !
+*)
+
+type nformula =
+  { coefs : (atom_index * bigint) list;
+    cst : bigint }
+
+let scale n { coefs; cst } =
+  { coefs = List.map (fun (v,k) -> (v,k*n)) coefs;
+    cst = cst*n }
+
+let shuffle nf1 nf2 =
+  let rec merge l1 l2 = match l1,l2 with
+    | [],_ -> l2
+    | _,[] -> l1
+    | (v1,k1)::r1,(v2,k2)::r2 ->
+       if Int.equal v1 v2 then
+         let k = k1+k2 in
+         if Bigint.equal k Bigint.zero then merge r1 r2
+         else (v1,k) :: merge r1 r2
+       else if v1 > v2 then (v1,k1) :: merge r1 l2
+       else (v2,k2) :: merge l1 r2
+  in
+  { coefs = merge nf1.coefs nf2.coefs;
+    cst = nf1.cst + nf2.cst }
+
+let rec normalize = function
+  | Oplus(t1,t2) -> shuffle (normalize t1) (normalize t2)
+  | Ominus(t1,t2) -> normalize (Oplus (t1, Oopp(t2)))
+  | Oopp(t) -> scale negone (normalize t)
+  | Omult(t,Oint n) | Omult (Oint n, t) ->
+     if Bigint.equal n Bigint.zero then { coefs = []; cst = zero }
+     else scale n (normalize t)
+  | Omult _ -> assert false (* invariant on Omult *)
+  | Oint n -> { coefs = []; cst = n }
+  | Oatom v -> { coefs = [v,Bigint.one]; cst=Bigint.zero}
+
+(* From normalized formulas to omega representations *)
+
+let omega_of_nformula env kind nf =
+  { id = new_omega_eq ();
+    kind;
+    constant=nf.cst;
+    body = List.map (fun (v,c) -> { v; c }) nf.coefs }
+
+
 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 t kind =
-    let trace, oterm = normalize_linear_term env t in
-    let equa = omega_of_oformula env kind oterm in
+let normalize_equation env (negated,depends,origin,path) oper t1 t2 =
+  let mk_step t kind =
+    let equa = omega_of_nformula env kind (normalize t) 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 }
+      e_omega = equa }
   in
   try match (if negated then (negate_oper oper) else oper) with
-    | Eq  -> mk_step t1 t2 (Oplus (t1,Oopp t2)) EQUA
-    | Neq -> mk_step t1 t2 (Oplus (t1,Oopp t2)) DISE
-    | Leq -> mk_step t1 t2 (Oplus (t2,Oopp t1)) INEQ
-    | Geq -> mk_step t1 t2 (Oplus (t1,Oopp t2)) INEQ
-    | Lt  -> mk_step t1 t2 (Oplus (Oplus(t2,Oint negone),Oopp t1)) INEQ
-    | Gt -> mk_step t1 t2 (Oplus (Oplus(t1,Oint negone),Oopp t2)) INEQ
+    | Eq  -> mk_step (Oplus (t1,Oopp t2)) EQUA
+    | Neq -> mk_step (Oplus (t1,Oopp t2)) DISE
+    | Leq -> mk_step (Oplus (t2,Oopp t1)) INEQ
+    | Geq -> mk_step (Oplus (t1,Oopp t2)) INEQ
+    | Lt  -> mk_step (Oplus (Oplus(t2,Oint negone),Oopp t1)) INEQ
+    | Gt -> mk_step (Oplus (Oplus(t1,Oint negone),Oopp t2)) INEQ
   with e when Logic.catchable_exception e -> raise e
 
 (* \section{Compilation des hypothèses} *)
 
+let mkPor i x y = Por (i,x,y)
+let mkPand i x y = Pand (i,x,y)
+let mkPimp i x y = Pimp (i,x,y)
+
 let rec oformula_of_constr env t =
   match Z.parse_term t with
     | Tplus (t1,t2) -> binop env (fun x y -> Oplus(x,y)) t1 t2
     | Tminus (t1,t2) -> binop env (fun x y -> Ominus(x,y)) t1 t2
-    | Tmult (t1,t2) when Z.is_scalar t1 || Z.is_scalar t2 ->
-	binop env (fun x y -> Omult(x,y)) t1 t2
+    | Tmult (t1,t2) ->
+       (match Z.get_scalar t1 with
+        | Some n -> Omult (Oint n,oformula_of_constr env t2)
+        | None ->
+           match Z.get_scalar t2 with
+           | Some n -> Omult (oformula_of_constr env t1, Oint n)
+           | None -> Oatom (add_reified_atom true t env))
     | Topp t -> Oopp(oformula_of_constr env t)
     | Tsucc t -> Oplus(oformula_of_constr env t, Oint one)
     | Tnum n -> Oint n
-    | _ -> Oatom (add_reified_atom t env)
+    | Tother -> Oatom (add_reified_atom true t env)
 
 and binop env c t1 t2 =
   let t1' = oformula_of_constr env t1 in
@@ -721,7 +543,7 @@ 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
+  let omega = normalize_equation env ctxt connector t1' t2' in
   add_equation env omega;
   Pequa (c,omega)
 
@@ -736,22 +558,16 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
     | Rtrue -> Ptrue
     | Rfalse -> Pfalse
     | Rnot t ->
-	let t' =
-	  oproposition_of_constr
-	    env (not negated, depends, origin,(O_mono::path)) gl t in
-	Pnot t'
-    | Ror (t1,t2) ->
-	binprop env ctxt (not negated) negated gl (fun i x y -> Por(i,x,y)) t1 t2
-    | Rand (t1,t2) ->
-	binprop env ctxt negated negated gl
-	  (fun i x y -> Pand(i,x,y)) t1 t2
+       let ctxt' = (not negated, depends, origin,(O_mono::path)) in
+       Pnot (oproposition_of_constr env ctxt' gl t)
+    | Ror (t1,t2) -> binprop env ctxt (not negated) negated gl mkPor t1 t2
+    | Rand (t1,t2) -> binprop env ctxt negated negated gl mkPand t1 t2
     | Rimp (t1,t2) ->
-	binprop env ctxt (not negated) (not negated) gl
-	  (fun i x y -> Pimp(i,x,y)) t1 t2
+       binprop env ctxt (not negated) (not negated) gl mkPimp t1 t2
     | Riff (t1,t2) ->
        (* No lifting here, since Omega only works on closed propositions. *)
-       binprop env ctxt negated negated gl
-          (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1)
+       binprop env ctxt negated negated gl mkPand
+         (Term.mkArrow t1 t2) (Term.mkArrow t2 t1)
     | _ -> Pprop c
 
 (* Destructuration des hypothèses et de la conclusion *)
@@ -836,7 +652,7 @@ let display_systems syst_list =
       (operator_of_eq om_e.kind) in
 
   let display_equation oformula_eq =
-    pprint stdout (Pequa (Lazy.force coq_c_nop,oformula_eq)); print_newline ();
+    pprint stdout (Pequa (Lazy.force coq_I,oformula_eq)); print_newline ();
     display_omega oformula_eq.e_omega;
     Printf.printf "  Depends on:";
     List.iter display_depend oformula_eq.e_depends;
@@ -897,14 +713,14 @@ let add_stated_equations env tree =
     (* 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
+    let v = add_reified_atom false coq_v env in
     (* Le terme qu'il va falloir introduire *)
     let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; 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.st_var;
+    force_omega_var env (Oatom v) st.st_var;
     (v, term_to_generalize,term_to_reify,st.st_def.id) in
  List.map add_env stated_equations
 
@@ -1054,38 +870,35 @@ let replay_history env env_hyp =
                 [| mk_nat (get_hyp env_hyp e1.id);
                    mk_nat (get_hyp env_hyp e2.id) |])
       | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
-	  mkApp (Lazy.force coq_s_div_approx,
-		 [| Z.mk k; Z.mk d;
-		    reified_of_omega env e2.body e2.constant;
-		    loop env_hyp l; mk_nat (get_hyp env_hyp e1.id) |])
+         mkApp (Lazy.force coq_s_div_approx,
+                [| mk_nat (get_hyp env_hyp e1.id); Z.mk k; Z.mk d;
+                   reified_of_omega env e2.body e2.constant;
+                   loop env_hyp l |])
       | NOT_EXACT_DIVIDE (e1,k) :: l ->
-	  let e2_constant = floor_div e1.constant k in
-	  let d = e1.constant - e2_constant * k in
-	  let e2_body = map_eq_linear (fun c -> c / k) e1.body in
-          mkApp (Lazy.force coq_s_not_exact_divide,
-		 [|Z.mk k; Z.mk d;
-		   reified_of_omega env e2_body e2_constant;
-		   mk_nat (get_hyp env_hyp e1.id)|])
+         let e2_constant = floor_div e1.constant k in
+         let d = e1.constant - e2_constant * k in
+         let e2_body = map_eq_linear (fun c -> c / k) e1.body in
+         mkApp (Lazy.force coq_s_not_exact_divide,
+                [| mk_nat (get_hyp env_hyp e1.id); Z.mk k; Z.mk d;
+                   reified_of_omega env e2_body e2_constant |])
       | EXACT_DIVIDE (e1,k) :: l ->
-	  let e2_body =
-	    map_eq_linear (fun c -> c / k) e1.body in
-	  let e2_constant = floor_div e1.constant k in
-          mkApp (Lazy.force coq_s_exact_divide,
-		 [|Z.mk k;
-		   reified_of_omega env e2_body e2_constant;
-		   loop env_hyp l; mk_nat (get_hyp env_hyp e1.id)|])
+         let e2_body = map_eq_linear (fun c -> c / k) e1.body in
+         let e2_constant = floor_div e1.constant k in
+         mkApp (Lazy.force coq_s_exact_divide,
+                [| mk_nat (get_hyp env_hyp e1.id); Z.mk k;
+                   reified_of_omega env e2_body e2_constant;
+                   loop env_hyp l |])
       | (MERGE_EQ(e3,e1,e2)) :: l ->
 	  let n1 = get_hyp env_hyp e1.id and n2 = get_hyp env_hyp e2 in
           mkApp (Lazy.force coq_s_merge_eq,
 		 [| mk_nat n1; mk_nat n2;
 		    loop (CCEqua e3:: env_hyp) l |])
       | SUM(e3,(k1,e1),(k2,e2)) :: l ->
-	  let n1 = get_hyp env_hyp e1.id
-	  and n2 = get_hyp env_hyp e2.id in
-	  let trace = shuffle_path k1 e1.body k2 e2.body in
-          mkApp (Lazy.force coq_s_sum,
-		 [| Z.mk k1; mk_nat n1; Z.mk k2;
-		    mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |])
+         let n1 = get_hyp env_hyp e1.id
+         and n2 = get_hyp env_hyp e2.id in
+         mkApp (Lazy.force coq_s_sum,
+                [| Z.mk k1; mk_nat n1; Z.mk k2;
+                   mk_nat n2; (loop (CCEqua e3 :: env_hyp) l) |])
       | CONSTANT_NOT_NUL(e,k) :: l ->
           mkApp (Lazy.force coq_s_constant_not_nul,
 		 [|  mk_nat (get_hyp env_hyp e) |])
@@ -1093,19 +906,13 @@ let replay_history env env_hyp =
           mkApp (Lazy.force coq_s_constant_neg,
 		 [|  mk_nat (get_hyp env_hyp e) |])
       | STATE {st_new_eq=new_eq; st_def =def;
-		      st_orig=orig; st_coef=m;
-                      st_var=sigma } :: l ->
-	  let n1 = get_hyp env_hyp orig.id
-	  and n2 = get_hyp env_hyp def.id in
-	  let v = unintern_omega env sigma in
-	  let o_def = oformula_of_omega env def in
-	  let o_orig = oformula_of_omega env orig in
-	  let body =
-	     Oplus (o_orig,Omult (Oplus (Oopp v,o_def), Oint m)) in
-          let trace,_ = normalize_linear_term env body in
-	  mkApp (Lazy.force coq_s_state,
-		 [| Z.mk m; trace; mk_nat n1; mk_nat n2;
-		    loop (CCEqua new_eq.id :: env_hyp) l |])
+               st_orig=orig; st_coef=m;
+               st_var=sigma } :: l ->
+         let n1 = get_hyp env_hyp orig.id
+         and n2 = get_hyp env_hyp def.id in
+         mkApp (Lazy.force coq_s_state,
+                [| Z.mk m; mk_nat n1; mk_nat n2;
+                   loop (CCEqua new_eq.id :: env_hyp) l |])
       |	HYP _ :: l -> loop env_hyp l
       |	CONSTANT_NUL e :: l ->
 	  mkApp (Lazy.force coq_s_constant_nul,
@@ -1205,7 +1012,6 @@ let resolution env (reified_concl,reified_hyps) systems_list =
     List.fold_left (fun s e -> Id.Set.add e.e_origin.o_hyp s) Id.Set.empty in
   let hyps = hyps_of_eqns equations in
   let useful_hypnames = Id.Set.elements (Id.Set.remove id_concl hyps) in
-  let all_names = id_concl :: useful_hypnames in
   let useful_hyptypes =
     List.map (fun id -> List.assoc_f Id.equal id reified_hyps) useful_hypnames
   in
@@ -1229,6 +1035,8 @@ let resolution env (reified_concl,reified_hyps) systems_list =
          IntHtbl.add env.real_indices var i; t :: loop (succ i) l
     in
     loop 0 all_vars_env in
+  (* Since [all_vars_env] is sorted, this renumbering of variables
+     should have preserved order *)
   let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in
   (* On peut maintenant généraliser le but : env est a jour *)
   let l_reified_stated =
@@ -1249,24 +1057,8 @@ let resolution env (reified_concl,reified_hyps) systems_list =
             (l_reified_stated @ l_reified_terms) in
   let reified =
     app coq_interp_sequent
-       [| reified_concl;env_props_reified;env_terms_reified;reified_goal|] in
-  let reified = EConstr.of_constr reified 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
-    let correct_index =
-      let i = List.index0 Id.equal e.e_origin.o_hyp all_names in
-      (* PL: it seems that additionally introduced hyps are in the way during
-             normalization, hence this index shifting... *)
-      if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce)
-    in
-    app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in
-  let normalization_trace =
-    mk_list (Lazy.force coq_h_step) (List.map normalize_equation equations) in
-
+       [| reified_concl;env_props_reified;env_terms_reified;reified_goal|]
+  in
   let initial_context =
     List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) useful_hypnames in
   let context =
@@ -1275,8 +1067,8 @@ let resolution env (reified_concl,reified_hyps) systems_list =
 
   Tactics.generalize
     (l_generalize_arg @ List.map EConstr.mkVar useful_hypnames) >>
-  Tactics.change_concl reified >>
-  Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
+  Tactics.change_concl (EConstr.of_constr reified) >>
+  Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >>
   show_goal >>
   Tactics.normalise_vm_in_concl >>
   (*i Alternatives to the previous line: