Merge PR#666: romega revisited : no more normalization trace, cleaned-up resolution trace

9 files changed, 1577 insertions, 3239 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
index e95604ffc..1ecc2ce2c 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -257,9 +257,9 @@ let sub_mult m d q k =
     end
   done
 
-(** Euclid division m/d = (q,r)
-    This is the "Floor" variant, as with ocaml's /
-    (but not as ocaml's Big_int.quomod_big_int).
+(** Euclid division m/d = (q,r), with m = q*d+r and |r|<|q|.
+    This is the "Trunc" variant (a.k.a "Truncated-Toward-Zero"),
+    as with ocaml's / (but not as ocaml's Big_int.quomod_big_int).
     We have sign r = sign m *)
 
 let euclid m d =
diff --git a/lib/bigint.mli b/lib/bigint.mli
index e5525f164..a1dc66077 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -30,6 +30,12 @@ val mult_2 : bigint -> bigint
 val add : bigint -> bigint -> bigint
 val sub : bigint -> bigint -> bigint
 val mult : bigint -> bigint -> bigint
+
+(** Euclid division m/d = (q,r), with m = q*d+r and |r|<|q|.
+    This is the "Trunc" variant (a.k.a "Truncated-Toward-Zero"),
+    as with ocaml's / (but not as ocaml's Big_int.quomod_big_int).
+    We have sign r = sign m *)
+
 val euclid : bigint -> bigint -> bigint * bigint
 
 val less_than : bigint -> bigint -> bool
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 334b03de1..2a018fa3f 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -96,7 +96,7 @@ type afine = {
 
 type state_action = {
   st_new_eq : afine;
-  st_def    : afine;
+  st_def    : afine; (* /!\ this represents [st_def = st_var] *)
   st_orig   : afine;
   st_coef   : bigint;
   st_var    : int }
@@ -587,10 +587,6 @@ let rec depend relie_on accu = function
       end
   | [] -> relie_on, accu
 
-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,_ = List.partition (fun e -> e.kind = DISE) ineqs in
   let normal = function
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 187601fc6..d242264a9 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -10,12 +10,14 @@
 Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base.
 Delimit Scope Int_scope with I.
 
-(* Abstract Integers. *)
+(** * Abstract Integers. *)
 
 Module Type Int.
 
   Parameter t : Set.
 
+  Bind Scope Int_scope with t.
+
   Parameter zero : t.
   Parameter one : t.
   Parameter plus : t -> t -> t.
@@ -32,10 +34,10 @@ Module Type Int.
 
   Open Scope Int_scope.
 
-  (* First, int is a ring: *)
+  (** First, Int is a ring: *)
   Axiom ring : @ring_theory t 0 1 plus mult minus opp (@eq t).
 
-  (* int should also be ordered: *)
+  (** Int should also be ordered: *)
 
   Parameter le : t -> t -> Prop.
   Parameter lt : t -> t -> Prop.
@@ -49,35 +51,47 @@ Module Type Int.
   Axiom ge_le_iff : forall i j, (i>=j) <-> (j<=i).
   Axiom gt_lt_iff : forall i j, (i>j) <-> (j<i).
 
-  (* Basic properties of this order *)
+  (** Basic properties of this order *)
   Axiom lt_trans : forall i j k, i<j -> j<k -> i<k.
   Axiom lt_not_eq : forall i j, i<j -> i<>j.
 
-  (* Compatibilities *)
+  (** Compatibilities *)
   Axiom lt_0_1 : 0<1.
   Axiom plus_le_compat : forall i j k l, i<=j -> k<=l -> i+k<=j+l.
   Axiom opp_le_compat : forall i j, i<=j -> (-j)<=(-i).
   Axiom mult_lt_compat_l :
    forall i j k, 0 < k -> i < j -> k*i<k*j.
 
-  (* We should have a way to decide the equality and the order*)
+  (** We should have a way to decide the equality and the order*)
   Parameter compare : t -> t -> comparison.
   Infix "?=" := compare (at level 70, no associativity) : Int_scope.
   Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j.
   Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j.
   Axiom compare_Gt : forall i j, compare i j = Gt <-> i>j.
 
-  (* Up to here, these requirements could be fulfilled
+  (** Up to here, these requirements could be fulfilled
      by any totally ordered ring. Let's now be int-specific: *)
   Axiom le_lt_int : forall x y, x<y <-> x<=y+-(1).
 
-  (* Btw, lt_0_1 could be deduced from this last axiom *)
+  (** Btw, lt_0_1 could be deduced from this last axiom *)
+
+  (** Now we also require a division function.
+      It is deliberately underspecified, since that's enough
+      for the proofs below. But the most appropriate variant
+      (and the one needed to stay in sync with the omega engine)
+      is "Floor" (the historical version of Coq's [Z.div]). *)
+
+  Parameter diveucl : t -> t -> t * t.
+  Notation "i / j" := (fst (diveucl i j)).
+  Notation "i 'mod' j" := (snd (diveucl i j)).
+  Axiom diveucl_spec :
+    forall i j, j<>0 -> i = j * (i/j) + (i mod j).
 
 End Int.
 
 
 
-(* Of course, Z is a model for our abstract int *)
+(** Of course, Z is a model for our abstract int *)
 
 Module Z_as_Int <: Int.
 
@@ -131,21 +145,24 @@ Module Z_as_Int <: Int.
 
   Definition le_lt_int := Z.lt_le_pred.
 
-End Z_as_Int.
+  Definition diveucl := Z.div_eucl.
+  Definition diveucl_spec := Z.div_mod.
 
+End Z_as_Int.
 
 
+(** * Properties of abstract integers *)
 
 Module IntProperties (I:Int).
  Import I.
  Local Notation int := I.t.
 
- (* Primo, some consequences of being a ring theory... *)
+ (** Primo, some consequences of being a ring theory... *)
 
  Definition two := 1+1.
  Notation "2" := two : Int_scope.
 
- (* Aliases for properties packed in the ring record. *)
+ (** Aliases for properties packed in the ring record. *)
 
  Definition plus_assoc := ring.(Radd_assoc).
  Definition plus_comm := ring.(Radd_comm).
@@ -160,31 +177,22 @@ Module IntProperties (I:Int).
  Opaque plus_assoc plus_comm plus_0_l mult_assoc mult_comm mult_1_l
   mult_plus_distr_r opp_def minus_def.
 
- (* More facts about plus *)
+ (** More facts about [plus] *)
 
  Lemma plus_0_r : forall x, x+0 = x.
  Proof. intros; rewrite plus_comm; apply plus_0_l. Qed.
 
- Lemma plus_0_r_reverse : forall x, x = x+0.
- Proof. intros; symmetry; apply plus_0_r. Qed.
-
- Lemma plus_assoc_reverse : forall x y z, x+y+z = x+(y+z).
- Proof. intros; symmetry; apply plus_assoc. Qed.
-
  Lemma plus_permute : forall x y z, x+(y+z) = y+(x+z).
  Proof. intros; do 2 rewrite plus_assoc; f_equal; apply plus_comm. Qed.
 
  Lemma plus_reg_l : forall x y z, x+y = x+z -> y = z.
  Proof.
   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.
 
- (* More facts about mult *)
-
- Lemma mult_assoc_reverse : forall x y z, x*y*z = x*(y*z).
- Proof. intros; symmetry; apply mult_assoc. Qed.
+ (** More facts about [mult] *)
 
  Lemma mult_plus_distr_l : forall x y z, x*(y+z)=x*y+x*z.
  Proof.
@@ -193,18 +201,25 @@ 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 *)
+ (** More facts about [opp] *)
 
  Definition plus_opp_r := opp_def.
 
@@ -249,104 +264,47 @@ Module IntProperties (I:Int).
   now rewrite opp_def, <-mult_plus_distr_r, opp_def, mult_0_l.
  Qed.
 
- Lemma egal_left : forall n m, n=m -> n+-m = 0.
- Proof. intros; subst; apply opp_def. Qed.
-
- Lemma ne_left_2 : forall x y : int, x<>y -> 0<>(x + - y).
- Proof.
- intros; contradict H.
- apply (plus_reg_l (-y)).
- now rewrite plus_opp_l, plus_comm, H.
- Qed.
-
- (* Special lemmas for factorisation. *)
-
- Lemma red_factor0 : forall n, n = n*1.
- Proof. symmetry; rewrite mult_comm; apply mult_1_l. Qed.
-
- Lemma red_factor1 : forall n, n+n = n*2.
- Proof.
-  intros; unfold two.
-  now rewrite mult_comm, mult_plus_distr_r, mult_1_l.
- Qed.
-
- 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.
- Qed.
-
- Lemma red_factor3 : forall n m, n*m + n = n*(1+m).
- Proof. intros; now rewrite plus_comm, red_factor2. Qed.
-
- Lemma red_factor4 : forall n m p, n*m + n*p = n*(m+p).
+ Lemma egal_left n m : 0 = n+-m <-> n = m.
  Proof.
-  intros; now rewrite mult_plus_distr_l.
+  split; intros.
+  - apply plus_reg_l with (-m).
+    rewrite plus_comm, <- H. symmetry. apply plus_opp_l.
+  - symmetry. subst; apply opp_def.
  Qed.
 
- Lemma red_factor5 : forall n m , n * 0 + m = m.
- Proof. intros; now rewrite mult_comm, mult_0_l, plus_0_l. Qed.
-
- Definition red_factor6 := plus_0_r_reverse.
-
-
- (* Specialized distributivities *)
+ (** Specialized distributivities *)
 
  Hint Rewrite mult_plus_distr_l mult_plus_distr_r mult_assoc : int.
  Hint Rewrite <- plus_assoc : int.
 
- Lemma OMEGA10 :
-  forall v c1 c2 l1 l2 k1 k2 : int,
-  (v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
-  v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).
- Proof.
-  intros; autorewrite with int; f_equal; now rewrite plus_permute.
- Qed.
-
- Lemma OMEGA11 :
-  forall v1 c1 l1 l2 k1 : int,
-  (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).
- Proof.
-  intros; now autorewrite with int.
- Qed.
+ Hint Rewrite plus_0_l plus_0_r mult_0_l mult_0_r mult_1_l mult_1_r : int.
 
- Lemma OMEGA12 :
-  forall v2 c2 l1 l2 k2 : int,
-  l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).
+ Lemma OMEGA10 v c1 c2 l1 l2 k1 k2 :
+  v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2) =
+  (v * c1 + l1) * k1 + (v * c2 + l2) * k2.
  Proof.
-  intros; autorewrite with int; now rewrite plus_permute.
+  autorewrite with int; f_equal; now rewrite plus_permute.
  Qed.
 
- Lemma OMEGA13 :
-  forall v l1 l2 x : int,
-  v * -x + l1 + (v * x + l2) = l1 + l2.
+ Lemma OMEGA11 v1 c1 l1 l2 k1 :
+  v1 * (c1 * k1) + (l1 * k1 + l2) = (v1 * c1 + l1) * k1 + l2.
  Proof.
- intros; autorewrite with int.
- rewrite plus_permute; f_equal.
- rewrite plus_assoc.
- now rewrite <- mult_plus_distr_l, plus_opp_l, mult_comm, mult_0_l, plus_0_l.
+  now autorewrite with int.
  Qed.
 
- Lemma OMEGA15 :
-  forall v c1 c2 l1 l2 k2 : int,
-  v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).
+ Lemma OMEGA12 v2 c2 l1 l2 k2 :
+   v2 * (c2 * k2) + (l1 + l2 * k2) = l1 + (v2 * c2 + l2) * k2.
  Proof.
-  intros; autorewrite with int; f_equal; now rewrite plus_permute.
+  autorewrite with int; now rewrite plus_permute.
  Qed.
 
- Lemma OMEGA16 : forall v c l k : int, (v * c + l) * k = v * (c * k) + l * k.
+ Lemma sum1 a b c d : 0 = a -> 0 = b -> 0 = a * c + b * d.
  Proof.
-  intros; now autorewrite with int.
- Qed.
-
- Lemma sum1 : forall a b c d : int, 0 = a -> 0 = b -> 0 = a * c + b * d.
- Proof.
- intros; elim H; elim H0; simpl; auto.
- now rewrite mult_0_l, mult_0_l, plus_0_l.
+ intros; subst. now autorewrite with int.
  Qed.
 
 
- (* Secondo, some results about order (and equality) *)
+ (** Secondo, some results about order (and equality) *)
 
  Lemma lt_irrefl : forall n, ~ n<n.
  Proof.
@@ -413,86 +371,74 @@ Module IntProperties (I:Int).
 
  Definition beq i j := match compare i j with Eq => true | _ => false end.
 
- Lemma beq_iff : forall i j, beq i j = true <-> i=j.
- Proof.
- intros; unfold beq; generalize (compare_Eq i j).
- destruct compare; intuition discriminate.
- Qed.
+ Infix "=?" := beq : Int_scope.
 
- Lemma beq_true : forall i j, beq i j = true -> i=j.
+ Lemma beq_iff i j : (i =? j) = true <-> i=j.
  Proof.
- intros.
- rewrite <- beq_iff; auto.
+ unfold beq. rewrite <- (compare_Eq i j). now destruct compare.
  Qed.
 
- Lemma beq_false : forall i j, beq i j = false -> i<>j.
+ Lemma beq_reflect i j : reflect (i=j) (i =? j).
  Proof.
- intros.
- intro H'.
- rewrite <- beq_iff in H'; rewrite H' in H; discriminate.
+ apply iff_reflect. symmetry. apply beq_iff.
  Qed.
 
  Lemma eq_dec : forall n m:int, { n=m } + { n<>m }.
  Proof.
-  intros; generalize (beq_iff n m); destruct beq; [left|right]; intuition.
+  intros n m; generalize (beq_iff n m); destruct beq; [left|right]; intuition.
  Qed.
 
- Definition bgt i j := match compare i j with Gt => true | _ => false end.
+ Definition blt i j := match compare i j with Lt => true | _ => false end.
+
+ Infix "<?" := blt : Int_scope.
 
- Lemma bgt_iff : forall i j, bgt i j = true <-> i>j.
+ Lemma blt_iff i j : (i <? j) = true <-> i<j.
  Proof.
- intros; unfold bgt; generalize (compare_Gt i j).
- destruct compare; intuition discriminate.
+ unfold blt. rewrite <- (compare_Lt i j). now destruct compare.
  Qed.
 
- Lemma bgt_true : forall i j, bgt i j = true -> i>j.
- Proof. intros; now rewrite <- bgt_iff. Qed.
-
- Lemma bgt_false : forall i j, bgt i j = false -> i<=j.
+ Lemma blt_reflect i j : reflect (i<j) (i <? j).
  Proof.
-  intros.
-  rewrite le_lt_iff, <-gt_lt_iff, <-bgt_iff; intro H'; now rewrite H' in H.
+ apply iff_reflect. symmetry. apply blt_iff.
  Qed.
 
  Lemma le_is_lt_or_eq : forall n m, n<=m -> { n<m } + { n=m }.
  Proof.
-  intros.
+  intros n m Hnm.
   destruct (eq_dec n m) as [H'|H'].
-  right; intuition.
-  left; rewrite lt_le_iff.
-  contradict H'.
-  apply le_antisym; auto.
+  - right; intuition.
+  - left; rewrite lt_le_iff.
+    contradict H'.
+    now apply le_antisym.
  Qed.
 
  Lemma le_neq_lt : forall n m, n<=m -> n<>m -> n<m.
  Proof.
-  intros.
-  destruct (le_is_lt_or_eq _ _ H); intuition.
+  intros n m H. now destruct (le_is_lt_or_eq _ _ H).
  Qed.
 
  Lemma le_trans : forall n m p, n<=m -> m<=p -> n<=p.
  Proof.
-  intros n m p; do 3 rewrite le_lt_iff; intros A B C.
+  intros n m p; rewrite 3 le_lt_iff; intros A B C.
   destruct (lt_eq_lt_dec p m) as [[H|H]|H]; subst; auto.
   generalize (lt_trans _ _ _ H C); intuition.
  Qed.
 
- (* order and operations *)
-
- Lemma le_0_neg : forall n, 0 <= n <-> -n <= 0.
+ Lemma not_eq (a b:int) : ~ a <> b <-> a = b.
  Proof.
- intros.
- pattern 0 at 2; rewrite <- (mult_0_l (-(1))).
- rewrite <- opp_eq_mult_neg_1.
- split; intros.
- apply opp_le_compat; auto.
- rewrite <-(opp_involutive 0), <-(opp_involutive n).
- apply opp_le_compat; auto.
+  destruct (eq_dec a b); intuition.
  Qed.
 
- Lemma le_0_neg' : forall n, n <= 0 <-> 0 <= -n.
+ (** Order and operations *)
+
+ Lemma le_0_neg n : n <= 0 <-> 0 <= -n.
  Proof.
- intros; rewrite le_0_neg, opp_involutive; intuition.
+ rewrite <- (mult_0_l (-(1))) at 2.
+ rewrite <- opp_eq_mult_neg_1.
+ split; intros.
+ - now apply opp_le_compat.
+ - rewrite <-(opp_involutive 0), <-(opp_involutive n).
+   now apply opp_le_compat.
  Qed.
 
  Lemma plus_le_reg_r : forall n m p, n + p <= m + p -> n <= m.
@@ -534,20 +480,14 @@ Module IntProperties (I:Int).
  apply opp_le_compat; auto.
  Qed.
 
- Lemma lt_0_neg : forall n, 0 < n <-> -n < 0.
+ Lemma lt_0_neg n : n < 0 <-> 0 < -n.
  Proof.
- intros.
- pattern 0 at 2; rewrite <- (mult_0_l (-(1))).
+ rewrite <- (mult_0_l (-(1))) at 2.
  rewrite <- opp_eq_mult_neg_1.
  split; intros.
- apply opp_lt_compat; auto.
- rewrite <-(opp_involutive 0), <-(opp_involutive n).
- apply opp_lt_compat; auto.
- Qed.
-
- Lemma lt_0_neg' : forall n, n < 0 <-> 0 < -n.
- Proof.
- intros; rewrite lt_0_neg, opp_involutive; intuition.
+ - now apply opp_lt_compat.
+ - rewrite <-(opp_involutive 0), <-(opp_involutive n).
+   now apply opp_lt_compat.
  Qed.
 
  Lemma mult_lt_0_compat : forall n m, 0 < n -> 0 < m -> 0 < n*m.
@@ -557,111 +497,70 @@ Module IntProperties (I:Int).
  apply mult_lt_compat_l; auto.
  Qed.
 
- Lemma mult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0.
+ Lemma mult_integral_r n m : 0 < n -> n * m = 0 -> m = 0.
  Proof.
- intros.
- destruct (lt_eq_lt_dec n 0) as [[Hn|Hn]|Hn]; auto;
-  destruct (lt_eq_lt_dec m 0) as [[Hm|Hm]|Hm]; auto; exfalso.
-
- rewrite lt_0_neg' in Hn.
- rewrite lt_0_neg' in Hm.
- generalize (mult_lt_0_compat _ _ Hn Hm).
- rewrite <- opp_mult_distr_r, mult_comm, <- opp_mult_distr_r, opp_involutive.
- rewrite mult_comm, H.
- exact (lt_irrefl 0).
-
- rewrite lt_0_neg' in Hn.
- generalize (mult_lt_0_compat _ _ Hn Hm).
- rewrite mult_comm, <- opp_mult_distr_r, mult_comm.
- rewrite H.
- rewrite opp_eq_mult_neg_1, mult_0_l.
- exact (lt_irrefl 0).
-
- rewrite lt_0_neg' in Hm.
- generalize (mult_lt_0_compat _ _ Hn Hm).
- rewrite <- opp_mult_distr_r.
- rewrite H.
- rewrite opp_eq_mult_neg_1, mult_0_l.
- exact (lt_irrefl 0).
-
- generalize (mult_lt_0_compat _ _ Hn Hm).
- rewrite H.
- exact (lt_irrefl 0).
+ intros Hn H.
+ destruct (lt_eq_lt_dec 0 m) as [[Hm| <- ]|Hm]; auto; exfalso.
+ - generalize (mult_lt_0_compat _ _ Hn Hm).
+   rewrite H.
+   exact (lt_irrefl 0).
+ - rewrite lt_0_neg in Hm.
+   generalize (mult_lt_0_compat _ _ Hn Hm).
+   rewrite <- opp_mult_distr_r, opp_eq_mult_neg_1, H, mult_0_l.
+   exact (lt_irrefl 0).
  Qed.
 
- Lemma mult_le_compat :
-   forall i j k l, i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l.
+ Lemma mult_integral n m : n * m = 0 -> n = 0 \/ m = 0.
  Proof.
- intros.
- destruct (le_is_lt_or_eq _ _ H1).
-
- apply le_trans with (i*l).
- destruct (le_is_lt_or_eq _ _ H0); [ | subst; apply le_refl].
- apply lt_le_weak.
- apply mult_lt_compat_l; auto.
-
- generalize (le_trans _ _ _ H2 H0); clear H0 H1 H2; intros.
- rewrite (mult_comm i), (mult_comm j).
- destruct (le_is_lt_or_eq _ _ H0);
-  [ | subst; do 2 rewrite mult_0_l; apply le_refl].
- destruct (le_is_lt_or_eq _ _ H);
-  [ | subst; apply le_refl].
- apply lt_le_weak.
- apply mult_lt_compat_l; auto.
-
- subst i.
- rewrite mult_0_l.
- generalize (le_trans _ _ _ H2 H0); clear H0 H1 H2; intros.
- destruct (le_is_lt_or_eq _ _ H);
-  [ | subst; rewrite mult_0_l; apply le_refl].
- destruct (le_is_lt_or_eq _ _ H0);
-  [ | subst; rewrite mult_comm, mult_0_l; apply le_refl].
- apply lt_le_weak.
- apply mult_lt_0_compat; auto.
+ intros H.
+ destruct (lt_eq_lt_dec 0 n) as [[Hn|Hn]|Hn].
+ - right; apply (mult_integral_r n m); trivial.
+ - now left.
+ - right; apply (mult_integral_r (-n) m).
+   + now apply lt_0_neg.
+   + rewrite mult_comm, <- opp_mult_distr_r, mult_comm, H.
+     now rewrite opp_eq_mult_neg_1, mult_0_l.
  Qed.
 
- Lemma sum5 :
- forall a b c d : int, c <> 0 -> 0 <> a -> 0 = b -> 0 <> a * c + b * d.
+ Lemma mult_le_compat_l i j k :
+   0<=k -> i<=j -> k*i <= k*j.
  Proof.
- intros.
- subst b; rewrite mult_0_l, plus_0_r.
- contradict H.
- symmetry in H; destruct (mult_integral _ _ H); congruence.
+ intros Hk Hij.
+ apply le_is_lt_or_eq in Hk. apply le_is_lt_or_eq in Hij.
+ destruct Hk as [Hk | <-], Hij as [Hij | <-];
+  rewrite ? mult_0_l; try apply le_refl.
+ now apply lt_le_weak, mult_lt_compat_l.
  Qed.
 
- Lemma one_neq_zero : 1 <> 0.
+ Lemma mult_le_compat i j k l :
+   i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l.
  Proof.
- red; intro.
- symmetry in H.
- apply (lt_not_eq 0 1); auto.
- apply lt_0_1.
+ intros Hij Hkl Hi Hk.
+ apply le_trans with (i*l).
+ - now apply mult_le_compat_l.
+ - rewrite (mult_comm i), (mult_comm j).
+   apply mult_le_compat_l; trivial.
+   now apply le_trans with k.
  Qed.
 
- Lemma minus_one_neq_zero : -(1) <> 0.
+ Lemma sum5 a b c d : 0 <> c -> 0 <> a -> 0 = b -> 0 <> a * c + b * d.
  Proof.
- apply lt_not_eq.
- rewrite <- lt_0_neg.
- apply lt_0_1.
+ intros Hc Ha <-. autorewrite with int. contradict Hc.
+ symmetry in Hc. destruct (mult_integral _ _ Hc); congruence.
  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.
- Proof.
- intros.
- replace 0 with (0+0).
- apply plus_le_compat; auto.
- rewrite plus_0_l; auto.
- Qed.
-
- Lemma OMEGA8 : forall x y, 0 <= x -> 0 <= y -> x = - y -> x = 0.
+ Lemma OMEGA8 x y : 0 <= x -> 0 <= y -> x = - y -> x = 0.
  Proof.
  intros.
  assert (y=-x).
@@ -675,17 +574,15 @@ Module IntProperties (I:Int).
  elim (lt_not_eq _ _ H1); auto.
  Qed.
 
- Lemma sum2 :
- forall a b c d : int, 0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d.
+ Lemma sum2 a b c d :
+   0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d.
  Proof.
- intros.
- subst a; rewrite mult_0_l, plus_0_l.
+ intros Hd <- Hb. autorewrite with int.
  rewrite <- (mult_0_l 0).
  apply mult_le_compat; auto; apply le_refl.
  Qed.
 
- Lemma sum3 :
- forall a b c d : int,
+ Lemma sum3 a b c d :
   0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d.
  Proof.
  intros.
@@ -697,56 +594,39 @@ Module IntProperties (I:Int).
  apply mult_le_compat; auto; apply le_refl.
  Qed.
 
- Lemma sum4 : forall k : int, k>0 -> 0 <= k.
- Proof.
- intros k; rewrite gt_lt_iff; apply lt_le_weak.
- Qed.
-
- (* Lemmas specific to integers (they use lt_le_int) *)
-
- Lemma lt_left : forall n m, n < m -> 0 <= m + -(1) + - n.
- Proof.
- intros; apply le_left.
- now rewrite <- le_lt_int.
- Qed.
+ (** Lemmas specific to integers (they use [le_lt_int]) *)
 
- Lemma lt_left_inv : forall x y, 0 <= y + -(1) + - x -> x < y.
+ Lemma lt_left n m : n < m <-> 0 <= m + -n + -(1).
  Proof.
- intros.
- generalize (plus_le_compat _ _ _ _ H (le_refl x)); clear H.
- now rewrite plus_0_l, <-plus_assoc, plus_opp_l, plus_0_r, le_lt_int.
+ rewrite <- plus_assoc, (plus_comm (-n)), plus_assoc.
+ rewrite <- le_left.
+ apply le_lt_int.
  Qed.
 
- Lemma OMEGA4 : forall x y z, x > 0 -> y > x -> z * y + x <> 0.
+ Lemma OMEGA4 x y z : 0 < x -> x < y -> z * y + x <> 0.
  Proof.
- intros.
- intro H'.
- rewrite gt_lt_iff in H,H0.
+ intros H H0 H'.
+ assert (0 < y) by now apply lt_trans with x.
  destruct (lt_eq_lt_dec z 0) as [[G|G]|G].
 
- rewrite lt_0_neg' in G.
- generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0).
- rewrite H'.
- pattern y at 2; rewrite <-(mult_1_l y), <-mult_plus_distr_r.
- intros.
- rewrite le_lt_int in G.
- rewrite <- opp_plus_distr in G.
- assert (0 < y) by (apply lt_trans with x; auto).
- generalize (mult_le_compat _ _ _ _ G (lt_le_weak _ _ H2) (le_refl 0) (le_refl 0)).
- rewrite mult_0_l, mult_comm, <- opp_mult_distr_r, mult_comm, <-le_0_neg', le_lt_iff.
- intuition.
+ - generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0).
+   rewrite H'.
+   rewrite <-(mult_1_l y) at 2. rewrite <-mult_plus_distr_r.
+   apply le_lt_iff.
+   rewrite mult_comm. rewrite <- (mult_0_r y).
+   apply mult_le_compat_l; auto using lt_le_weak.
+   apply le_0_neg. rewrite opp_plus_distr.
+   apply le_lt_int. now apply lt_0_neg.
 
- subst; rewrite mult_0_l, plus_0_l in H'; subst.
- apply (lt_not_eq _ _ H); auto.
+ - apply (lt_not_eq 0 (z*y+x)); auto.
+   subst. now autorewrite with int.
 
- apply (lt_not_eq 0 (z*y+x)); auto.
- rewrite <- (plus_0_l 0).
- apply plus_lt_compat; auto.
- apply mult_lt_0_compat; auto.
- apply lt_trans with x; auto.
+ - apply (lt_not_eq 0 (z*y+x)); auto.
+   rewrite <- (plus_0_l 0).
+   auto using plus_lt_compat, mult_lt_0_compat.
  Qed.
 
- Lemma OMEGA19 : forall x, x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1).
+ Lemma OMEGA19 x : x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1).
  Proof.
  intros.
  do 2 rewrite <- le_lt_int.
@@ -759,35 +639,22 @@ Module IntProperties (I:Int).
  apply opp_lt_compat; auto.
  Qed.
 
- Lemma mult_le_approx :
-  forall n m p, n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.
+ Lemma mult_le_approx n m p :
+  0 < n -> p < n -> 0 <= m * n + p -> 0 <= m.
  Proof.
- intros n m p.
- do 2 rewrite gt_lt_iff.
- do 2 rewrite le_lt_iff; intros.
- contradict H1.
- rewrite lt_0_neg' in H1.
- rewrite lt_0_neg'.
- rewrite opp_plus_distr.
- rewrite mult_comm, opp_mult_distr_r.
+ do 2 rewrite le_lt_iff; intros Hn Hpn H Hm. destruct H.
+ apply lt_0_neg, le_lt_int, le_left in Hm.
+ rewrite lt_0_neg.
+ rewrite opp_plus_distr, mult_comm, opp_mult_distr_r.
+ rewrite le_lt_int. apply lt_left.
  rewrite le_lt_int.
- rewrite <- plus_assoc, (plus_comm (-p)), plus_assoc.
- apply lt_left.
- rewrite le_lt_int.
- rewrite le_lt_int in H0.
- apply le_trans with (n+-(1)); auto.
+ apply le_trans with (n+-(1)); [ now apply le_lt_int | ].
  apply plus_le_compat; [ | apply le_refl ].
- rewrite le_lt_int in H1.
- generalize (mult_le_compat _ _ _ _ (lt_le_weak _ _ H) H1 (le_refl 0) (le_refl 0)).
- rewrite mult_0_l.
- rewrite mult_plus_distr_l.
- rewrite <- opp_eq_mult_neg_1.
- intros.
- generalize (plus_le_compat _ _ _ _ (le_refl n) H2).
- now rewrite plus_permute, opp_def, plus_0_r, plus_0_r.
+ rewrite <- (mult_1_r n) at 1.
+ apply mult_le_compat_l; auto using lt_le_weak.
  Qed.
 
- (* Some decidabilities *)
+ (** Some decidabilities *)
 
  Lemma dec_eq : forall i j:int, decidable (i=j).
  Proof.
@@ -822,7 +689,7 @@ Module IntProperties (I:Int).
 End IntProperties.
 
 
-
+(** * The Coq side of the romega tactic *)
 
 Module IntOmega (I:Int).
 Import I.
@@ -830,13 +697,16 @@ Module IP:=IntProperties(I).
 Import IP.
 Local Notation int := I.t.
 
-(* \subsubsection{Definition of reified integer expressions}
+(* ** Definition 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. *)
+   - integers [Tint]
+   - variables [Tvar]
+   - operation over integers (addition, product, opposite, subtraction)
+
+   Opposite and subtraction are translated in additions and products.
+   Note that we'll only deal with products for which at least one side
+   is [Tint]. *)
 
 Inductive term : Set :=
   | Tint : int -> term
@@ -844,8 +714,9 @@ Inductive term : Set :=
   | Tmult : term -> term -> term
   | Tminus : term -> term -> term
   | Topp : term -> term
-  | Tvar : nat -> term.
+  | Tvar : N -> term.
 
+Bind Scope romega_scope with term.
 Delimit Scope romega_scope with term.
 Arguments Tint _%I.
 Arguments Tplus (_ _)%term.
@@ -859,400 +730,212 @@ Infix "-" := Tminus : romega_scope.
 Notation "- x" := (Topp x) : romega_scope.
 Notation "[ x ]" := (Tvar x) (at level 0) : romega_scope.
 
-(* \subsubsection{Definition of reified goals} *)
+(* ** Definition of reified goals
 
-(* Very restricted definition of handled predicates that should be extended
+   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 (* equality between terms *)
-  | LeqTerm : term -> term -> proposition (* less or equal on terms *)
-  | TrueTerm : proposition (* true *)
-  | FalseTerm : proposition (* false *)
-  | Tnot : proposition -> proposition (* negation *)
+  (** First, basic equations, disequations, inequations *)
+  | EqTerm : term -> term -> proposition
+  | NeqTerm : term -> term -> proposition
+  | LeqTerm : term -> term -> proposition
   | GeqTerm : term -> term -> proposition
   | GtTerm : term -> term -> proposition
   | LtTerm : term -> term -> proposition
-  | NeqTerm : term -> term -> proposition
+  (** Then, the supported logical connectors *)
+  | TrueTerm : proposition
+  | FalseTerm : proposition
+  | Tnot : proposition -> proposition
   | Tor : proposition -> proposition -> proposition
   | Tand : proposition -> proposition -> proposition
   | Timp : proposition -> proposition -> proposition
+  (** Everything else is left as a propositional atom (and ignored). *)
   | Tprop : nat -> proposition.
 
-(* Definition of goals as a list of hypothesis *)
+(** Definition of goals as a list of hypothesis *)
 Notation hyps := (list proposition).
 
-(* Definition of lists of subgoals  (set of open goals) *)
+(** Definition of lists of subgoals (set of open goals) *)
 Notation lhyps := (list hyps).
 
-(* a single goal packed in a subgoal list *)
+(** A single goal packed in a subgoal list *)
 Notation singleton := (fun a : hyps => a :: nil).
 
-(* an absurd goal *)
+(** 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. *)
-
-Inductive t_omega : Set :=
-  (* n = 0 and n!= 0 *)
-  | 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 -> nat -> t_omega -> nat -> t_omega
-  (* no solution because no exact division *)
-  | O_NOT_EXACT_DIVIDE : int -> int -> term -> nat -> nat -> t_omega
-  (* exact division *)
-  | O_EXACT_DIVIDE : int -> term -> nat -> t_omega -> nat -> t_omega
-  | O_SUM : int -> nat -> int -> 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 : 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.
-   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
-  | P_NOP : 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.
-
-(* \subsubsection{Rules for decomposing the hypothesis} *)
-(* This type allows navigation in the logical constructors that
-   form the predicats of the hypothesis in order to decompose them.
-   This allows in particular to extract one hypothesis from a
-   conjunction with possibly the right level of negations. *)
-
-Inductive direction : Set :=
-  | D_left : direction
-  | D_right : direction
-  | D_mono : direction.
-
-(* This type allows extracting useful components from hypothesis, either
-   hypothesis generated by splitting a disjonction, or equations.
-   The last constructor indicates how to solve the obtained system
-   via the use of the trace type of Omega [t_omega] *)
-
-Inductive e_step : Set :=
-  | 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{Efficient decidable equality} *)
-(* For each reified data-type, we define an efficient equality test.
-   It is not the one produced by [Decide Equality].
-
-   Then we prove two theorem allowing elimination of such equalities :
-   \begin{verbatim}
-   (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2.
-   (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2.
-   \end{verbatim} *)
-
-(* \subsubsection{Reified terms} *)
-
-Open Scope romega_scope.
+(** ** Decidable equality on terms *)
 
 Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
   match t1, t2 with
-  | Tint st1, Tint st2 => beq st1 st2
-  | (st11 + st12), (st21 + st22) => eq_term st11 st21 && eq_term st12 st22
-  | (st11 * st12), (st21 * st22) => eq_term st11 st21 && eq_term st12 st22
-  | (st11 - st12), (st21 - st22) => eq_term st11 st21 && eq_term st12 st22
-  | (- st1), (- st2) => eq_term st1 st2
-  | [st1], [st2] => beq_nat st1 st2
+  | Tint i1, Tint i2 => i1 =? i2
+  | (t11 + t12), (t21 + t22) => eq_term t11 t21 && eq_term t12 t22
+  | (t11 * t12), (t21 * t22) => eq_term t11 t21 && eq_term t12 t22
+  | (t11 - t12), (t21 - t22) => eq_term t11 t21 && eq_term t12 t22
+  | (- t1), (- t2) => eq_term t1 t2
+  | [v1], [v2] => N.eqb v1 v2
   | _, _ => false
-  end.
-
-Close Scope romega_scope.
+  end%term.
 
-Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2.
-Proof.
- induction t1; destruct t2; simpl in *; try discriminate;
- (rewrite andb_true_iff; intros (H1,H2)) || intros H; f_equal;
- auto using beq_true, beq_nat_true.
-Qed.
+Infix "=?" := eq_term : romega_scope.
 
-Theorem eq_term_refl : forall t0 : term, eq_term t0 t0 = true.
+Theorem eq_term_iff (t t' : term) :
+ (t =? t')%term = true <-> t = t'.
 Proof.
- induction t0; simpl in *; try (apply andb_true_iff; split); trivial.
- - now apply beq_iff.
- - now apply beq_nat_true_iff.
+ revert t'. induction t; destruct t'; simpl in *;
+ rewrite ?andb_true_iff, ?beq_iff, ?N.eqb_eq, ?IHt, ?IHt1, ?IHt2;
+  intuition congruence.
 Qed.
 
-Ltac trivial_case := unfold not; intros; discriminate.
-
-Theorem eq_term_false :
- forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2.
+Theorem eq_term_reflect (t t' : term) : reflect (t=t') (t =? t')%term.
 Proof.
- intros t1 t2 H E. subst t2. now rewrite eq_term_refl in H.
+ apply iff_reflect. symmetry. apply eq_term_iff.
 Qed.
 
-(* \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
-   telles fonctions sont trop lentes. *)
-
-(* 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 :=
-  let Aux := fresh "Aux" in
-  pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux;
-   [ generalize (eq_term_true t1 t2 Aux); clear Aux
-   | generalize (eq_term_false t1 t2 Aux); clear Aux ].
-
-Ltac elim_beq t1 t2 :=
-  let Aux := fresh "Aux" in
-  pattern (beq t1 t2); apply bool_eq_ind; intro Aux;
-   [ generalize (beq_true t1 t2 Aux); clear Aux
-   | generalize (beq_false t1 t2 Aux); clear Aux ].
-
-Ltac elim_bgt t1 t2 :=
-  let Aux := fresh "Aux" in
-  pattern (bgt t1 t2); apply bool_eq_ind; intro Aux;
-  [ generalize (bgt_true t1 t2 Aux); clear Aux
-  | generalize (bgt_false t1 t2 Aux); clear Aux ].
-
+(** ** Interpretations of terms (as integers). *)
 
-(* \subsection{Interprétations}
-   \subsubsection{Interprétation des termes dans Z} *)
+Fixpoint Nnth {A} (n:N)(l:list A)(default:A) :=
+ match n, l with
+   | _, nil => default
+   | 0%N, x::_ => x
+   | _, _::l => Nnth (N.pred n) l default
+ end.
 
-Fixpoint interp_term (env : list int) (t : term) {struct t} : int :=
+Fixpoint interp_term (env : list int) (t : term) : int :=
   match t with
   | Tint x => x
   | (t1 + t2)%term => interp_term env t1 + interp_term env t2
   | (t1 * t2)%term => interp_term env t1 * interp_term env t2
   | (t1 - t2)%term => interp_term env t1 - interp_term env t2
   | (- t)%term => - interp_term env t
-  | [n]%term => nth n env 0
+  | [n]%term => Nnth n env 0
   end.
 
-(* \subsubsection{Interprétation des prédicats} *)
+(** ** Interpretation of predicats (as Coq propositions) *)
 
-Fixpoint interp_proposition (envp : list Prop) (env : list int)
- (p : proposition) {struct p} : Prop :=
+Fixpoint interp_prop (envp : list Prop) (env : list int)
+ (p : proposition) : Prop :=
   match p with
   | EqTerm t1 t2 => interp_term env t1 = interp_term env t2
+  | NeqTerm t1 t2 => (interp_term env t1) <> (interp_term env t2)
   | LeqTerm t1 t2 => interp_term env t1 <= interp_term env t2
-  | TrueTerm => True
-  | FalseTerm => False
-  | Tnot p' => ~ interp_proposition envp env p'
   | GeqTerm t1 t2 => interp_term env t1 >= interp_term env t2
   | GtTerm t1 t2 => interp_term env t1 > interp_term env t2
   | LtTerm t1 t2 => interp_term env t1 < interp_term env t2
-  | NeqTerm t1 t2 => (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
+  | TrueTerm => True
+  | FalseTerm => False
+  | Tnot p' => ~ interp_prop envp env p'
+  | Tor p1 p2 => interp_prop envp env p1 \/ interp_prop envp env p2
+  | Tand p1 p2 => interp_prop envp env p1 /\ interp_prop envp env p2
+  | Timp p1 p2 => interp_prop envp env p1 -> interp_prop envp env p2
   | Tprop n => nth n envp True
   end.
 
-(* \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 *)
+(** ** Intepretation of hypothesis lists (as Coq conjunctions) *)
 
-Fixpoint interp_hyps (envp : list Prop) (env : list int)
- (l : hyps) {struct l} : Prop :=
+Fixpoint interp_hyps (envp : list Prop) (env : list int) (l : hyps)
+  : Prop :=
   match l with
   | nil => True
-  | p' :: l' => interp_proposition envp env p' /\ interp_hyps envp env l'
+  | p' :: l' => interp_prop 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) *)
+(** ** Interpretation of conclusion + hypotheses
+
+   Here we use Coq implications : it's less easy to manipulate,
+   but handy to relate to the Coq original goal (cf. the use of
+   [generalize], and lighter (no repetition of types in intermediate
+   conjunctions). *)
 
 Fixpoint interp_goal_concl (c : proposition) (envp : list Prop)
- (env : list int) (l : hyps) {struct l} : Prop :=
+ (env : list int) (l : hyps) : Prop :=
   match l with
-  | nil => interp_proposition envp env c
+  | nil => interp_prop envp env c
   | p' :: l' =>
-      interp_proposition envp env p' -> interp_goal_concl c envp env l'
+      interp_prop envp env p' -> interp_goal_concl c envp env l'
   end.
 
 Notation interp_goal := (interp_goal_concl FalseTerm).
 
-(* Les théorèmes qui suivent assurent la correspondance entre les deux
-   interprétations. *)
+(** Equivalence between these two interpretations. *)
 
 Theorem goal_to_hyps :
  forall (envp : list Prop) (env : list int) (l : hyps),
  (interp_hyps envp env l -> False) -> interp_goal envp env l.
 Proof.
- simple induction l;
- [ simpl; auto
- | simpl; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ].
+ induction l; simpl; auto.
 Qed.
 
 Theorem hyps_to_goal :
  forall (envp : list Prop) (env : list int) (l : hyps),
  interp_goal envp env l -> interp_hyps envp env l -> False.
 Proof.
- simple induction l; simpl; [ auto | intros; apply H; elim H1; auto ].
-Qed.
-
-(* \subsection{Manipulations sur les hypothèses} *)
-
-(* \subsubsection{Définitions de base de stabilité pour la réflexion} *)
-(* Une opération laisse un terme stable si l'égalité est préservée *)
-Definition term_stable (f : term -> term) :=
-  forall (e : list int) (t : term), interp_term e t = interp_term e (f t).
-
-(* Une opération est valide sur une hypothèse, si l'hypothèse implique le
-   résultat de l'opération. \emph{Attention : cela ne concerne que des
-   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 (ep : list Prop) (e : list int) (p1 : proposition),
-  interp_proposition ep e p1 -> interp_proposition ep e (f p1).
-
-Definition valid2 (f : proposition -> proposition -> proposition) :=
-  forall (ep : list Prop) (e : list int) (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 proposition.
-   On reste contravariant *)
-
-Definition valid_hyps (f : hyps -> hyps) :=
-  forall (ep : list Prop) (e : list int) (lp : hyps),
-  interp_hyps ep e lp -> interp_hyps ep e (f lp).
-
-(* Enfin ce théorème élimine la contravariance et nous ramène à une
-   opération sur les buts *)
-
-Theorem valid_goal :
-  forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps),
-  valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l.
-Proof.
- intros; simpl; apply goal_to_hyps; intro H1;
- apply (hyps_to_goal ep env (a l) H0); apply H; assumption.
+ induction l; simpl; auto.
+ intros H (H1,H2). auto.
 Qed.
 
-(* \subsubsection{Généralisation a des listes de buts (disjonctions)} *)
+(** ** Interpretations of list of goals
 
+    Here again, two flavours... *)
 
 Fixpoint interp_list_hyps (envp : list Prop) (env : list int)
- (l : lhyps) {struct l} : Prop :=
+ (l : lhyps) : Prop :=
   match l with
   | nil => False
   | h :: l' => interp_hyps envp env h \/ interp_list_hyps envp env l'
   end.
 
 Fixpoint interp_list_goal (envp : list Prop) (env : list int)
- (l : lhyps) {struct l} : Prop :=
+ (l : lhyps) : Prop :=
   match l with
   | nil => True
   | h :: l' => interp_goal envp env h /\ interp_list_goal envp env l'
   end.
 
+(** Equivalence between the two flavours. *)
+
 Theorem list_goal_to_hyps :
  forall (envp : list Prop) (env : list int) (l : lhyps),
  (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l.
 Proof.
- simple induction l; simpl;
- [ auto
- | intros h1 l1 H H1; split;
-    [ apply goal_to_hyps; intro H2; apply H1; auto
-    | apply H; intro H2; apply H1; auto ] ].
+ induction l; simpl; intuition. now apply goal_to_hyps.
 Qed.
 
 Theorem list_hyps_to_goal :
  forall (envp : list Prop) (env : list int) (l : lhyps),
  interp_list_goal envp env l -> interp_list_hyps envp env l -> False.
 Proof.
- simple induction l; simpl;
- [ auto
- | intros h1 l1 H (H1, H2) H3; elim H3; intro H4;
-    [ apply hyps_to_goal with (1 := H1); assumption | auto ] ].
+ induction l; simpl; intuition. eapply hyps_to_goal; eauto.
 Qed.
 
+(** ** Stabiliy and validity of operations *)
+
+(** An operation on terms is stable if the interpretation is unchanged. *)
+
+Definition term_stable (f : term -> term) :=
+  forall (e : list int) (t : term), interp_term e t = interp_term e (f t).
+
+(** An operation on one hypothesis is valid if this hypothesis implies
+    the result of this operation. *)
+
+Definition valid1 (f : proposition -> proposition) :=
+  forall (ep : list Prop) (e : list int) (p1 : proposition),
+  interp_prop ep e p1 -> interp_prop ep e (f p1).
+
+Definition valid2 (f : proposition -> proposition -> proposition) :=
+  forall (ep : list Prop) (e : list int) (p1 p2 : proposition),
+  interp_prop ep e p1 ->
+  interp_prop ep e p2 -> interp_prop ep e (f p1 p2).
+
+(** Same for lists of hypotheses, and for list of goals *)
+
+Definition valid_hyps (f : hyps -> hyps) :=
+  forall (ep : list Prop) (e : list int) (lp : hyps),
+  interp_hyps ep e lp -> interp_hyps ep e (f lp).
+
 Definition valid_list_hyps (f : hyps -> lhyps) :=
   forall (ep : list Prop) (e : list int) (lp : hyps),
   interp_hyps ep e lp -> interp_list_hyps ep e (f lp).
@@ -1261,6 +944,16 @@ Definition valid_list_goal (f : hyps -> lhyps) :=
   forall (ep : list Prop) (e : list int) (lp : hyps),
   interp_list_goal ep e (f lp) -> interp_goal ep e lp.
 
+(** Some results about these validities. *)
+
+Theorem valid_goal :
+  forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps),
+  valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l.
+Proof.
+ intros; simpl; apply goal_to_hyps; intro H1;
+ apply (hyps_to_goal ep env (a l) H0); apply H; assumption.
+Qed.
+
 Theorem goal_valid :
  forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f.
 Proof.
@@ -1274,33 +967,31 @@ Theorem append_valid :
  interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 ->
  interp_list_hyps ep e (l1 ++ l2).
 Proof.
- intros ep e; simple induction l1;
- [ simpl; intros l2 [H| H]; [ contradiction | trivial ]
- | simpl; intros h1 t1 HR l2 [[H| H]| H];
-    [ auto
-    | right; apply (HR l2); left; trivial
-    | right; apply (HR l2); right; trivial ] ].
-
+ induction l1; simpl in *.
+ - now intros l2 [H| H].
+ - intros l2 [[H| H]| H].
+   + auto.
+   + right; apply IHl1; now left.
+   + right; apply IHl1; now right.
 Qed.
 
-(* \subsubsection{Opérateurs valides sur les hypothèses} *)
+(** ** Valid operations on hypotheses *)
+
+(** Extract an hypothesis from the list *)
 
-(* Extraire une hypothèse de la liste *)
 Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm.
-Unset Printing Notations.
+
 Theorem nth_valid :
  forall (ep : list Prop) (e : list int) (i : nat) (l : hyps),
- interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l).
+ interp_hyps ep e l -> interp_prop ep e (nth_hyps i l).
 Proof.
- unfold nth_hyps; simple induction i;
- [ simple induction l; simpl; [ auto | intros; elim H0; auto ]
- | intros n H; simple induction l;
-    [ simpl; trivial
-    | intros; simpl; apply H; elim H1; auto ] ].
+ unfold nth_hyps. induction i; destruct l; simpl in *; try easy.
+ intros (H1,H2). now apply IHi.
 Qed.
 
-(* Appliquer une opération (valide) sur deux hypothèses extraites de
-   la liste et ajouter le résultat à la liste. *)
+(** Apply a valid operation on two hypotheses from the list, and
+    store the result in the list. *)
+
 Definition apply_oper_2 (i j : nat)
   (f : proposition -> proposition -> proposition) (l : hyps) :=
   f (nth_hyps i l) (nth_hyps j l) :: l.
@@ -1310,15 +1001,18 @@ Theorem apply_oper_2_valid :
  valid2 f -> valid_hyps (apply_oper_2 i j f).
 Proof.
  intros i j f Hf; unfold apply_oper_2, valid_hyps; simpl;
- intros lp Hlp; split; [ apply Hf; apply nth_valid; assumption | assumption ].
+ intros lp Hlp; split.
+ - apply Hf; apply nth_valid; assumption.
+ - assumption.
 Qed.
 
-(* Modifier une hypothèse par application d'une opération valide *)
+(** In-place modification of an hypothesis by application of
+    a valid operation. *)
 
 Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition)
  (l : hyps) {struct i} : hyps :=
   match l with
-  | nil => nil (A:=proposition)
+  | nil => nil
   | p :: l' =>
       match i with
       | O => f p :: l'
@@ -1330,105 +1024,11 @@ Theorem apply_oper_1_valid :
  forall (i : nat) (f : proposition -> proposition),
  valid1 f -> valid_hyps (apply_oper_1 i f).
 Proof.
- unfold valid_hyps; intros i f Hf ep e; elim i;
- [ intro lp; case lp;
-    [ simpl; trivial
-    | simpl; intros p l' (H1, H2); split;
-       [ apply Hf with (1 := H1) | assumption ] ]
- | intros n Hrec lp; case lp;
-    [ simpl; auto
-    | simpl; intros p l' (H1, H2); split;
-       [ assumption | apply Hrec; assumption ] ] ].
+ unfold valid_hyps.
+ induction i; intros f Hf ep e [ | p lp]; simpl; intuition.
 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é} *)
+(** ** A tactic for proving stability *)
 
 Ltac loop t :=
   match t with
@@ -1438,54 +1038,33 @@ Ltac loop t :=
   (* Interpretations *)
   | (interp_hyps _ _ ?X1) => loop X1
   | (interp_list_hyps _ _ ?X1) => loop X1
-  | (interp_proposition _ _ ?X1) => loop X1
+  | (interp_prop _ _ ?X1) => loop X1
   | (interp_term _ ?X1) => loop X1
   (* Propositions *)
   | (EqTerm ?X1 ?X2) => loop X1 || loop X2
   | (LeqTerm ?X1 ?X2) => loop X1 || loop X2
-  (* Termes *)
+  (* Terms *)
   | (?X1 + ?X2)%term => loop X1 || loop X2
   | (?X1 - ?X2)%term => loop X1 || loop X2
   | (?X1 * ?X2)%term => loop X1 || loop X2
   | (- ?X1)%term => loop X1
   | (Tint ?X1) => loop X1
   (* Eliminations *)
-  | match ?X1 with
-    | EqTerm _ _ => _
-    | LeqTerm _ _ => _
-    | TrueTerm => _
-    | FalseTerm => _
-    | Tnot _ => _
-    | GeqTerm _ _ => _
-    | GtTerm _ _ => _
-    | LtTerm _ _ => _
-    | NeqTerm _ _ => _
-    | Tor _ _ => _
-    | Tand _ _ => _
-    | Timp _ _ => _
-    | Tprop _ => _
-    end => destruct X1; auto; Simplify
-  | match ?X1 with
-    | Tint _ => _
-    | (_ + _)%term => _
-    | (_ * _)%term => _
-    | (_ - _)%term => _
-    | (- _)%term => _
-    | [_]%term => _
-    end => destruct X1; auto; Simplify
-  | (if beq ?X1 ?X2 then _ else _) =>
+  | (if ?X1 =? ?X2 then _ else _) =>
       let H := fresh "H" in
-      elim_beq X1 X2; intro H; try (rewrite H in *; clear H);
-       simpl; auto; Simplify
-  | (if bgt ?X1 ?X2 then _ else _) =>
+      case (beq_reflect X1 X2); intro H;
+      try (rewrite H in *; clear H); simpl; auto; Simplify
+  | (if ?X1 <? ?X2 then _ else _) =>
+      case (blt_reflect X1 X2); intro; simpl; auto; Simplify
+  | (if (?X1 =? ?X2)%term then _ else _) =>
       let H := fresh "H" in
-      elim_bgt X1 X2; intro H; simpl; auto; Simplify
-  | (if eq_term ?X1 ?X2 then _ else _) =>
-      let H := fresh "H" in
-      elim_eq_term X1 X2; intro H; try (rewrite H in *; clear H);
-       simpl; auto; Simplify
+      case (eq_term_reflect X1 X2); intro H;
+      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
 
@@ -1494,875 +1073,529 @@ 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 T_OMEGA13 (t : term) :=
-  match t with
-  | (v * Tint x + l1 + (v' * Tint x' + l2))%term =>
-      if eq_term v v' && beq x (-x')
-      then (l1+l2)%term
-      else t
-  | _ => t
-  end.
-
-Theorem T_OMEGA13_stable : term_stable T_OMEGA13.
-Proof.
- unfold term_stable, T_OMEGA13; intros; Simplify; simpl;
- apply OMEGA13.
-Qed.
-
-Definition T_OMEGA15 (t : term) :=
-  match t with
-  | (v * Tint c1 + l1 + (v' * Tint c2 + l2) * Tint k2)%term =>
-      if eq_term v v'
-      then (v * Tint (c1 + c2 * k2)%I + (l1 + l2 * Tint k2))%term
-      else t
-  | _ => t
-  end.
-
-Theorem T_OMEGA15_stable : term_stable T_OMEGA15.
-Proof.
- prove_stable T_OMEGA15 OMEGA15.
-Qed.
-
-Definition T_OMEGA16 (t : term) :=
-  match t with
-  | ((v * Tint c + l) * Tint k)%term => (v * Tint (c * k) + l * Tint k)%term
-  | _ => t
-  end.
-
-
-Theorem T_OMEGA16_stable : term_stable T_OMEGA16.
-Proof.
- prove_stable T_OMEGA16 OMEGA16.
-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.
+(** ** Operations on equation bodies *)
 
-Definition Tmult_assoc_reduced (t : term) :=
-  match t with
-  | (n * Tint m * Tint p)%term => (n * Tint (m * p))%term
-  | _ => t
-  end.
+(** The operations below handle in priority _normalized_ terms, i.e.
+    terms of the form:
+      [([v1]*Tint k1 + ([v2]*Tint k2 + (... + Tint cst)))]
+    with [v1>v2>...] and all [ki<>0].
+    See [normalize] below for a way to put terms in this form.
 
-Theorem Tmult_assoc_reduced_stable : term_stable Tmult_assoc_reduced.
-Proof.
- prove_stable Tmult_assoc_reduced mult_assoc_reverse.
-Qed.
+    These operations also produce a correct (but suboptimal)
+    result in case of non-normalized input terms, but this situation
+    should normally not happen when running [romega].
 
-Definition Tred_factor0 (t : term) := (t * Tint 1)%term.
+     /!\ Do not modify this section (especially [fusion] and [normalize])
+    without tweaking the corresponding functions in [refl_omega.ml].
+*)
 
-Theorem Tred_factor0_stable : term_stable Tred_factor0.
-Proof.
- prove_stable Tred_factor0 red_factor0.
-Qed.
+(** Multiplication and sum by two constants. Invariant: [k1<>0]. *)
 
-Definition Tred_factor1 (t : term) :=
+Fixpoint scalar_mult_add (t : term) (k1 k2 : int) : term :=
   match t with
-  | (x + y)%term =>
-      if eq_term x y
-      then (x * Tint 2)%term
-      else t
-  | _ => t
-  end.
+  | v1 * Tint x1 + l1 =>
+    v1 * Tint (x1 * k1) + scalar_mult_add l1 k1 k2
+  | Tint x => Tint (k1 * x + k2)
+  | _ => t * Tint k1 + Tint k2 (* shouldn't happen *)
+  end%term.
 
-Theorem Tred_factor1_stable : term_stable Tred_factor1.
+Theorem scalar_mult_add_stable e t k1 k2 :
+ interp_term e (scalar_mult_add t k1 k2) =
+ interp_term e (t * Tint k1 + Tint k2).
 Proof.
- prove_stable Tred_factor1 red_factor1.
+ induction t; simpl; Simplify; simpl; auto. f_equal. apply mult_comm.
+ rewrite IHt2. simpl. apply OMEGA11.
 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.
+(** Multiplication by a (non-nul) constant. *)
 
-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.
+Definition scalar_mult (t : term) (k : int) := scalar_mult_add t k 0.
 
-Theorem Tred_factor3_stable : term_stable Tred_factor3.
+Theorem scalar_mult_stable e t k :
+ interp_term e (scalar_mult t k) =
+ interp_term e (t * Tint k).
 Proof.
- prove_stable Tred_factor3 red_factor3.
+ unfold scalar_mult. rewrite scalar_mult_add_stable. simpl.
+ apply plus_0_r.
 Qed.
 
+(** Adding a constant
 
-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.
+    Instead of using [scalar_norm_add t 1 k], the following
+    definition spares some computations.
+ *)
 
-Definition Tminus_def (t : term) :=
+Fixpoint scalar_add (t : term) (k : int) : term :=
   match t with
-  | (x - y)%term => (x + - y)%term
-  | _ => t
-  end.
+  | m + l => m + scalar_add l k
+  | Tint x => Tint (x + k)
+  | _ => t + Tint k
+  end%term.
 
-Theorem Tminus_def_stable : term_stable Tminus_def.
+Theorem scalar_add_stable e t k :
+ interp_term e (scalar_add t k) = interp_term e (t + Tint k).
 Proof.
- prove_stable Tminus_def minus_def.
+ induction t; simpl; Simplify; simpl; auto.
+ rewrite IHt2. simpl. apply plus_assoc.
 Qed.
 
-(* \subsection{Fonctions de réécriture complexes} *)
+(** Division by a constant
 
-(* \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''.  *)
+    All the non-constant coefficients should be exactly dividable *)
 
-Fixpoint reduce (t : term) : term :=
+Fixpoint scalar_div (t : term) (k : int) : option (term * int) :=
   match t with
-  | (x + y)%term =>
-      match reduce x with
-      | Tint x' =>
-          match reduce y with
-          | Tint y' => Tint (x' + y')
-          | y' => (Tint x' + y')%term
-          end
-      | x' => (x' + reduce y)%term
-      end
-  | (x * y)%term =>
-      match reduce x with
-      | Tint x' =>
-          match reduce y with
-          | Tint y' => Tint (x' * y')
-          | y' => (Tint x' * y')%term
-          end
-      | x' => (x' * reduce y)%term
-      end
-  | (x - y)%term =>
-      match reduce x with
-      | Tint x' =>
-          match reduce y with
-          | Tint y' => Tint (x' - y')
-          | y' => (Tint x' - y')%term
-          end
-      | x' => (x' - reduce y)%term
+  | v * Tint x + l =>
+    let (q,r) := diveucl x k in
+    if (r =? 0)%I then
+      match scalar_div l k with
+      | None => None
+      | Some (u,c) => Some (v * Tint q + u, c)
       end
-  | (- x)%term =>
-      match reduce x with
-      | Tint x' => Tint (- x')
-      | x' => (- x')%term
-      end
-  | _ => t
-  end.
+    else None
+  | Tint x =>
+    let (q,r) := diveucl x k in
+    Some (Tint q, r)
+  | _ => None
+  end%term.
+
+Lemma scalar_div_stable e t k u c : k<>0 ->
+  scalar_div t k = Some (u,c) ->
+  interp_term e (u * Tint k + Tint c) = interp_term e t.
+Proof.
+ revert u c.
+ induction t; simpl; Simplify; try easy.
+ - intros u c Hk. assert (H := diveucl_spec t0 k Hk).
+   simpl in H.
+   destruct diveucl as (q,r). simpl in H. rewrite H.
+   injection 1 as <- <-. simpl. f_equal. apply mult_comm.
+ - intros u c Hk.
+   destruct t1; simpl; Simplify; try easy.
+   destruct t1_2; simpl; Simplify; try easy.
+   assert (H := diveucl_spec t0 k Hk).
+   simpl in H.
+   destruct diveucl as (q,r). simpl in H. rewrite H.
+   case beq_reflect; [intros -> | easy].
+   destruct (scalar_div t2 k) as [(u',c')|] eqn:E; [|easy].
+   injection 1 as <- ->. simpl.
+   rewrite <- (IHt2 u' c Hk); simpl; auto.
+   rewrite plus_0_r , (mult_comm k q). symmetry. apply OMEGA11.
+Qed.
+
+
+(** Fusion of two equations.
+
+    From two normalized equations, this fusion will produce
+    a normalized output corresponding to the coefficiented sum.
+    Invariant: [k1<>0] and [k2<>0].
+*)
 
-Theorem reduce_stable : term_stable reduce.
-Proof.
- unfold term_stable; intros e t; elim t; auto;
- try
-  (intros t0 H0 t1 H1; simpl; rewrite H0; rewrite H1;
-    (case (reduce t0);
-      [ intro z0; case (reduce t1); intros; auto
-      | intros; auto
-      | intros; auto
-      | intros; auto
-      | intros; auto
-      | intros; auto ])); intros t0 H0; simpl;
- rewrite H0; case (reduce t0); intros; auto.
-Qed.
+Fixpoint fusion (t1 t2 : term) (k1 k2 : int) : term :=
+  match t1 with
+  | [v1] * Tint x1 + l1 =>
+    (fix fusion_t1 t2 : term :=
+       match t2 with
+         | [v2] * Tint x2 + l2 =>
+           match N.compare v1 v2 with
+             | Eq =>
+               let k := (k1 * x1 + k2 * x2)%I in
+               if (k =? 0)%I then fusion l1 l2 k1 k2
+               else [v1] * Tint k + fusion l1 l2 k1 k2
+             | Lt => [v2] * Tint (k2 * x2) + fusion_t1 l2
+             | Gt => [v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2
+           end
+         | Tint x2 => [v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2
+         | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *)
+       end) t2
+  | Tint x1 => scalar_mult_add t2 k2 (k1 * x1)
+  | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *)
+  end%term.
+
+Theorem fusion_stable e t1 t2 k1 k2 :
+ interp_term e (fusion t1 t2 k1 k2) =
+ interp_term e (t1 * Tint k1 + t2 * Tint k2).
+Proof.
+ revert t2; induction t1; simpl; Simplify; simpl; auto.
+ - intros; rewrite scalar_mult_add_stable. simpl.
+   rewrite plus_comm. f_equal. apply mult_comm.
+ - intros. Simplify. induction t2; simpl; Simplify; simpl; auto.
+   + rewrite IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11.
+   + rewrite IHt1_2. simpl. subst n0.
+     rewrite (mult_comm k1), (mult_comm k2) in H0.
+     rewrite <- OMEGA10, H0. now autorewrite with int.
+   + rewrite IHt1_2. simpl. subst n0.
+     rewrite (mult_comm k1), (mult_comm k2); apply OMEGA10.
+   + rewrite IHt2_2. simpl. rewrite (mult_comm k2); apply OMEGA12.
+   + rewrite IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11.
+Qed.
+
+(** Term normalization.
+
+   Precondition: all [Tmult] should be on at least one [Tint].
+   Postcondition: a normalized equivalent term (see below).
+*)
 
-(* \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
+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_mult (normalize t) (-(1))
+  | (t - t')%term => fusion (normalize t) (normalize t') 1 (-(1))
+  | (Tint k * t)%term | (t * Tint k)%term =>
+    if k =? 0 then Tint 0 else scalar_mult (normalize t) k
+  | (t1 * t2)%term => (t1 * t2)%term (* shouldn't happen *)
   end.
 
-Theorem fusion_stable : forall trace : list t_fusion, term_stable (fusion trace).
+Theorem normalize_stable : term_stable normalize.
 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 ] ] ].
+ intros e t.
+ induction t; simpl; Simplify; simpl;
+ rewrite ?scalar_mult_stable; simpl in *; rewrite <- ?IHt1;
+ rewrite ?fusion_stable; simpl; autorewrite with int; 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 de deux équations dont une sans coefficient} *)
-
-Definition fusion_right (trace : list t_fusion) (t : term) : term :=
-  match trace with
-  | nil => reduce t (* Il faut mettre un compute *)
-  | step :: trace' =>
-      match step with
-      | F_equal => apply_right (fusion trace') (T_OMEGA15 t)
-      | F_cancel => fusion trace' (Tred_factor5 (T_OMEGA15 t))
-      | F_left => apply_right (fusion trace') (Tplus_assoc_r t)
-      | F_right => apply_right (fusion trace') (T_OMEGA12 t)
-      end
-  end.
+(** ** Normalization of a proposition.
 
-(* \paragraph{Fusion avec annihilation} *)
-(* Normalement le résultat est une constante *)
+    The only basic facts left after normalization are
+    [0 = ...] or [0 <> ...] or [0 <= ...].
+    When a fact is in negative position, we factorize a [Tnot]
+    out of it, and normalize the reversed fact inside.
 
-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.
+    /!\ Here again, do not change this code without corresponding
+    modifications in [refl_omega.ml].
+*)
 
-Theorem fusion_cancel_stable : forall t : nat, term_stable (fusion_cancel t).
+Fixpoint normalize_prop (negated:bool)(p:proposition) :=
+  match p with
+  | 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).
+
+Local Ltac simp := cbn -[normalize].
+
+Theorem normalize_prop_valid b e ep p :
+  interp_prop e ep (normalize_prop b p) <-> interp_prop e ep p.
+Proof.
+ revert b.
+ induction p; intros; simp; try tauto.
+ - destruct b; simp;
+   rewrite <- ?normalize_stable; simpl; rewrite ?minus_def.
+   + rewrite not_eq. apply egal_left.
+   + apply egal_left.
+ - destruct b; simp;
+   rewrite <- ?normalize_stable; simpl; rewrite ?minus_def;
+   apply not_iff_compat, egal_left.
+ - destruct b; simp;
+   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
+   + symmetry. rewrite le_lt_iff. apply not_iff_compat, lt_left.
+   + now rewrite <- le_left.
+ - destruct b; simp;
+   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
+   + symmetry. rewrite ge_le_iff, le_lt_iff.
+     apply not_iff_compat, lt_left.
+   + rewrite ge_le_iff. now rewrite <- le_left.
+ - destruct b; simp;
+   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
+   + rewrite gt_lt_iff, lt_le_iff. apply not_iff_compat.
+     now rewrite <- le_left.
+   + symmetry. rewrite gt_lt_iff. apply lt_left.
+ - destruct b; simp;
+   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
+   + rewrite lt_le_iff. apply not_iff_compat.
+     now rewrite <- le_left.
+   + symmetry. apply lt_left.
+ - now rewrite IHp.
+ - now rewrite IHp1, IHp2.
+ - now rewrite IHp1, IHp2.
+ - now rewrite IHp1, IHp2.
+Qed.
+
+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.
- unfold term_stable, fusion_cancel; intros trace e; elim trace;
- [ exact (reduce_stable e)
- | intros n H t; elim H; exact (T_OMEGA13_stable e t) ].
+ intros; apply valid_goal with (2 := H); apply normalize_hyps_valid.
 Qed.
 
-(* \subsubsection{Opérations affines sur une équation} *)
-(* \paragraph{Multiplication scalaire et somme d'une constante} *)
-
-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.
+(** ** A simple decidability checker
 
-Theorem scalar_norm_add_stable :
- forall t : nat, term_stable (scalar_norm_add t).
-Proof.
- unfold term_stable, scalar_norm_add; intros trace; elim trace;
- [ exact reduce_stable
- | intros n H e t; elim apply_right_stable;
-    [ exact (T_OMEGA11_stable e t) | exact H ] ].
-Qed.
+   For us, everything is considered decidable except
+   propositional atoms [Tprop _]. *)
 
-(* \paragraph{Multiplication scalaire} *)
-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)
+Fixpoint decidability (p : proposition) : bool :=
+  match p with
+  | 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
+  | _ => true
   end.
 
-Theorem scalar_norm_stable : forall t : nat, term_stable (scalar_norm t).
-Proof.
- unfold term_stable, scalar_norm; intros trace; elim trace;
- [ exact reduce_stable
- | intros n H e t; elim apply_right_stable;
-    [ exact (T_OMEGA16_stable e t) | exact H ] ].
-Qed.
-
-(* \paragraph{Somme d'une constante} *)
-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 decidable_correct :
+ forall (ep : list Prop) (e : list int) (p : proposition),
+ decidability p = true -> decidable (interp_prop ep e p).
+Proof.
+ induction p; simpl; intros Hp; try destruct (andb_prop _ _ Hp).
+ - apply dec_eq.
+ - apply dec_ne.
+ - apply dec_le.
+ - apply dec_ge.
+ - apply dec_gt.
+ - apply dec_lt.
+ - left; auto.
+ - right; unfold not; auto.
+ - apply dec_not; auto.
+ - apply dec_or; auto.
+ - apply dec_and; auto.
+ - apply dec_imp; auto.
+ - discriminate.
+Qed.
+
+(** ** Omega steps
+
+   The following inductive type describes steps as they can be
+   found in the trace coming from the decision procedure Omega.
+   We consider here only normalized equations [0=...], disequations
+   [0<>...] or inequations [0<=...].
+
+   First, the final steps leading to a contradiction:
+   - [O_BAD_CONSTANT i] : hypothesis i has a constant body
+     and this constant is not compatible with the kind of i.
+   - [O_NOT_EXACT_DIVIDE i k] :
+     equation i can be factorized as some [k*t+c] with [0<c<k].
+
+   Now, the intermediate steps leading to a new hypothesis:
+   - [O_DIVIDE i k cont] :
+     the body of hypothesis i could be factorized as [k*t+c]
+     with either [k<>0] and [c=0] for a (dis)equation, or
+     [0<k] and [c<k] for an inequation. We change in-place the
+     body of i for [t].
+   - [O_SUM k1 i1 k2 i2 cont] : creates a new hypothesis whose
+     kind depends on the kind of hypotheses [i1] and [i2], and
+     whose body is [k1*body(i1) + k2*body(i2)]. Depending of the
+     situation, [k1] or [k2] might have to be positive or non-nul.
+   - [O_MERGE_EQ i j cont] :
+     inequations i and j have opposite bodies, we add an equation
+     with one these bodies.
+   - [O_SPLIT_INEQ i cont1 cont2] :
+     disequation i is split into a disjonction of inequations.
+*)
 
-Theorem add_norm_stable : forall t : nat, term_stable (add_norm t).
-Proof.
- unfold term_stable, add_norm; intros trace; elim trace;
- [ exact reduce_stable
- | intros n H e t; elim apply_right_stable;
-    [ exact (Tplus_assoc_r_stable e t) | exact H ] ].
-Qed.
+Definition idx := nat. (** Index of an hypothesis in the list *)
 
-(* \subsection{La fonction de normalisation des termes (moteur de réécriture)} *)
+Inductive t_omega : Set :=
+  | O_BAD_CONSTANT : idx -> t_omega
+  | O_NOT_EXACT_DIVIDE : idx -> int -> t_omega
 
+  | O_DIVIDE : idx -> int -> t_omega -> t_omega
+  | O_SUM : int -> idx -> int -> idx -> t_omega -> t_omega
+  | O_MERGE_EQ : idx -> idx -> t_omega -> t_omega
+  | O_SPLIT_INEQ : idx -> t_omega -> t_omega -> t_omega.
 
-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
-  end.
+(** ** Actual resolution steps of an omega normalized goal *)
 
-Theorem t_rewrite_stable : forall s : step, term_stable (t_rewrite s).
-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 ].
-Qed.
+(** First, the final steps, leading to a 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]} *)
+(** [O_BAD_CONSTANT] *)
 
-Definition constant_not_nul (i : nat) (h : hyps) :=
+Definition bad_constant (i : nat) (h : hyps) :=
   match nth_hyps i h with
-  | EqTerm (Tint Nul) (Tint n) =>
-      if beq n Nul then h else absurd
+  | EqTerm (Tint Nul) (Tint n) => if n =? Nul then h else absurd
+  | NeqTerm (Tint Nul) (Tint n) => if n =? Nul then absurd else h
+  | LeqTerm (Tint Nul) (Tint n) => if n <? Nul then absurd else h
   | _ => h
   end.
 
-Theorem constant_not_nul_valid :
- forall i : nat, valid_hyps (constant_not_nul i).
+Theorem bad_constant_valid i : valid_hyps (bad_constant i).
 Proof.
- unfold valid_hyps, constant_not_nul; intros i ep e lp H.
+ unfold valid_hyps, bad_constant; intros ep e lp H.
  generalize (nth_valid ep e i lp H); Simplify.
+ rewrite le_lt_iff. intuition.
 Qed.
 
-(* \paragraph{[O_CONSTANT_NEG]} *)
+(** [O_NOT_EXACT_DIVIDE] *)
 
-Definition constant_neg (i : nat) (h : hyps) :=
-  match nth_hyps i h with
-  | LeqTerm (Tint Nul) (Tint Neg) =>
-     if bgt Nul Neg then absurd else h
-  | _ => h
-  end.
-
-Theorem constant_neg_valid : forall i : nat, valid_hyps (constant_neg i).
-Proof.
- unfold valid_hyps, constant_neg; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl.
- rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition.
-Qed.
-
-(* \paragraph{[NOT_EXACT_DIVIDE]} *)
-Definition not_exact_divide (k1 k2 : int) (body : term)
-  (t i : nat) (l : hyps) :=
+Definition not_exact_divide (i : nat) (k : int) (l : hyps) :=
   match nth_hyps i l with
   | EqTerm (Tint Nul) b =>
-      if beq Nul 0 &&
-         eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b &&
-         bgt k2 0 &&
-         bgt k1 k2
-      then absurd
+    match scalar_div b k with
+    | Some (body,c) =>
+      if (Nul =? 0) && (0 <? c) && (c <? k) then absurd
       else l
+    | None => l
+    end
   | _ => l
   end.
 
-Theorem not_exact_divide_valid :
- forall (k1 k2 : int) (body : term) (t0 i : nat),
- valid_hyps (not_exact_divide k1 k2 body t0 i).
+Theorem not_exact_divide_valid i k :
+ valid_hyps (not_exact_divide i k).
 Proof.
- unfold valid_hyps, not_exact_divide; intros;
- generalize (nth_valid ep e i lp); Simplify.
- rewrite (scalar_norm_add_stable t0 e), <-H1.
- do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros.
- absurd (interp_term e body * k1 + k2 = 0);
- [ now apply OMEGA4 | symmetry; auto ].
+ unfold valid_hyps, not_exact_divide; intros.
+ generalize (nth_valid ep e i lp).
+ destruct (nth_hyps i lp); simpl; auto.
+ destruct t0; auto.
+ destruct (scalar_div t1 k) as [(body,c)|] eqn:E; auto.
+ Simplify.
+ assert (k <> 0).
+ { intro. apply (lt_not_eq 0 k); eauto using lt_trans. }
+ apply (scalar_div_stable e) in E; auto. simpl in E.
+ intros H'; rewrite <- H' in E; auto.
+ exfalso. revert E. now apply OMEGA4.
 Qed.
 
-(* \paragraph{[O_CONTRADICTION]} *)
+(** Now, the steps generating a new equation. *)
 
-Definition contradiction (t i j : nat) (l : hyps) :=
-  match nth_hyps i l with
-  | LeqTerm (Tint Nul) b1 =>
-      match nth_hyps j l with
-      | LeqTerm (Tint Nul') b2 =>
-          match fusion_cancel t (b1 + b2)%term with
-          | Tint k => if beq Nul 0 && beq Nul' 0 && bgt 0 k
-                      then absurd
-                      else l
-          | _ => l
-          end
-      | _ => l
-      end
-  | _ => l
-  end.
-
-Theorem contradiction_valid :
- forall t i j : nat, valid_hyps (contradiction t i j).
-Proof.
- unfold valid_hyps, contradiction; intros t i j ep e l H;
- generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
- case (nth_hyps i l); auto; intros t1 t2; case t1;
- auto; case (nth_hyps j l);
- auto; intros t3 t4; case t3; auto;
- simpl; intros z z' H1 H2;
- generalize (eq_refl (interp_term e (fusion_cancel t (t2 + t4)%term)));
- pattern (fusion_cancel t (t2 + t4)%term) at 2 3;
- case (fusion_cancel t (t2 + t4)%term); simpl;
- auto; intro k; elim (fusion_cancel_stable t); simpl.
- Simplify; intro H3.
- generalize (OMEGA2 _ _ H2 H1); rewrite H3.
- rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition.
-Qed.
+(** [O_DIVIDE] *)
 
-(* \paragraph{[O_NEGATE_CONTRADICT]} *)
-
-Definition negate_contradict (i1 i2 : nat) (h : hyps) :=
-  match nth_hyps i1 h with
-  | EqTerm (Tint Nul) b1 =>
-      match nth_hyps i2 h with
-      | NeqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2
-          then absurd
-          else h
-      | _ => h
-      end
-  | NeqTerm (Tint Nul) b1 =>
-      match nth_hyps i2 h with
-      | EqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2
-          then absurd
-          else h
-      | _ => h
-      end
-  | _ => h
-  end.
-
-Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) :=
-  match nth_hyps i1 h with
-  | EqTerm (Tint Nul) b1 =>
-      match nth_hyps i2 h with
-      | NeqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 &&
-             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
-          then absurd
-          else h
-      | _ => h
-      end
-  | NeqTerm (Tint Nul) b1 =>
-      match nth_hyps i2 h with
-      | EqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 &&
-             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
-          then absurd
-          else h
-      | _ => h
-      end
-  | _ => h
+Definition divide (k : int) (prop : proposition) :=
+  match prop with
+  | EqTerm (Tint o) b =>
+    match scalar_div b k with
+    | Some (body,c) =>
+      if (o =? 0) && (c =? 0) && negb (k =? 0)
+      then EqTerm (Tint 0) body
+      else TrueTerm
+    | None => TrueTerm
+    end
+  | NeqTerm (Tint o) b =>
+    match scalar_div b k with
+    | Some (body,c) =>
+      if (o =? 0) && (c =? 0) && negb (k =? 0)
+      then NeqTerm (Tint 0) body
+      else TrueTerm
+    | None => TrueTerm
+    end
+  | LeqTerm (Tint o) b =>
+    match scalar_div b k with
+    | Some (body,c) =>
+      if (o =? 0) && (0 <? k) && (c <? k)
+      then LeqTerm (Tint 0) body
+      else prop
+    | None => prop
+    end
+  | _ => TrueTerm
   end.
 
-Theorem negate_contradict_valid :
- forall i j : nat, valid_hyps (negate_contradict i j).
-Proof.
- unfold valid_hyps, negate_contradict; intros i j ep e l H;
- generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
- case (nth_hyps i l); auto; intros t1 t2; case t1;
- auto; intros z; auto; case (nth_hyps j l);
- auto; intros t3 t4; case t3; auto; intros z';
- auto; simpl; intros H1 H2; Simplify.
-Qed.
-
-Theorem negate_contradict_inv_valid :
- forall t i j : nat, valid_hyps (negate_contradict_inv t i j).
+Theorem divide_valid k : valid1 (divide k).
 Proof.
- unfold valid_hyps, negate_contradict_inv; intros t i j ep e l H;
- generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
- case (nth_hyps i l); auto; intros t1 t2; case t1;
- auto; intros z; auto; case (nth_hyps j l);
- auto; intros t3 t4; case t3; auto; intros z';
- auto; simpl; intros H1 H2; Simplify;
- [
- rewrite <- scalar_norm_stable in H2; simpl in *;
- elim (mult_integral (interp_term e t4) (-(1))); intuition;
- elim minus_one_neq_zero; auto
- |
- elim H2; clear H2;
- rewrite <- scalar_norm_stable; simpl in *;
- now rewrite <- H1, mult_0_l
- ].
+ unfold valid1, divide; intros ep e p;
+ destruct p; simpl; auto;
+ destruct t0; simpl; auto;
+ destruct scalar_div as [(body,c)|] eqn:E; simpl; Simplify; auto.
+ - apply (scalar_div_stable e) in E; auto. simpl in E.
+   intros H'; rewrite <- H' in E. rewrite plus_0_r in E.
+   apply mult_integral in E. intuition.
+ - apply (scalar_div_stable e) in E; auto. simpl in E.
+   intros H' H''. now rewrite <- H'', mult_0_l, plus_0_l in E.
+ - assert (k <> 0).
+   { intro. apply (lt_not_eq 0 k); eauto using lt_trans. }
+   apply (scalar_div_stable e) in E; auto. simpl in E. rewrite <- E.
+   intro H'. now apply mult_le_approx with (3 := H').
 Qed.
 
-(* \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. *)
+(** [O_SUM]. Invariant: [k1] and [k2] non-nul. *)
 
-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 =>
+  | EqTerm (Tint o) 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)
+      | EqTerm (Tint o') b2 =>
+          if (o =? 0) && (o' =? 0)
+          then EqTerm (Tint 0) (fusion b1 b2 k1 k2)
+          else TrueTerm
+      | LeqTerm (Tint o') b2 =>
+          if (o =? 0) && (o' =? 0) && (0 <? k2)
+          then LeqTerm (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)
+      | NeqTerm (Tint o') b2 =>
+          if (o =? 0) && (o' =? 0) && negb (k2 =? 0)
+          then NeqTerm (Tint 0) (fusion b1 b2 k1 k2)
           else TrueTerm
       | _ => TrueTerm
       end
-  | LeqTerm (Tint Null) b1 =>
-      if beq Null 0 && bgt k1 0
+  | LeqTerm (Tint o) b1 =>
+      if (o =? 0) && (0 <? k1)
       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)
+          | EqTerm (Tint o') b2 =>
+              if o' =? 0 then
+              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)
+          | LeqTerm (Tint o') b2 =>
+              if (o' =? 0) && (0 <? k2)
+              then LeqTerm (Tint 0) (fusion b1 b2 k1 k2)
               else TrueTerm
           | _ => TrueTerm
           end
       else TrueTerm
-  | NeqTerm (Tint Null) b1 =>
+  | NeqTerm (Tint o) b1 =>
       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)
+      | EqTerm (Tint o') b2 =>
+          if (o =? 0) && (o' =? 0) && negb (k1 =? 0)
+          then NeqTerm (Tint 0) (fusion b1 b2 k1 k2)
           else TrueTerm
       | _ => TrueTerm
       end
   | _ => TrueTerm
   end.
 
-
 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;
- [ apply sum1; assumption
- | apply sum2; try assumption; apply sum4; assumption
- | rewrite plus_comm; apply sum2; try assumption; apply sum4; assumption
- | apply sum3; try assumption; apply sum4; assumption
- | apply sum5; auto ].
-Qed.
-
-(* \paragraph{[O_EXACT_DIVIDE]}
-   c'est une oper1 valide mais on préfère une substitution a ce point la *)
-
-Definition exact_divide (k : int) (body : term) (t : nat)
-  (prop : proposition) :=
-  match prop with
-  | EqTerm (Tint Null) b =>
-      if beq Null 0 &&
-         eq_term (scalar_norm t (body * Tint k)%term) b &&
-         negb (beq k 0)
-      then EqTerm (Tint 0) body
-      else TrueTerm
-  | NeqTerm (Tint Null) b =>
-      if beq Null 0 &&
-         eq_term (scalar_norm t (body * Tint k)%term) b &&
-         negb (beq k 0)
-      then NeqTerm (Tint 0) body
-      else TrueTerm
-  | _ => TrueTerm
-  end.
-
-Theorem exact_divide_valid :
- forall (k : int) (t : term) (n : nat), valid1 (exact_divide k t n).
-Proof.
- unfold valid1, exact_divide; intros k1 k2 t ep e p1;
- Simplify; simpl; auto; subst;
- rewrite <- scalar_norm_stable; simpl; intros;
- [ destruct (mult_integral _ _ (eq_sym H0)); intuition
- | contradict H0; rewrite <- H0, mult_0_l; auto
- ].
+ Simplify; simpl; rewrite ?fusion_stable;
+ simpl; intros; auto.
+ - apply sum1; auto.
+ - rewrite plus_comm. apply sum5; auto.
+ - apply sum2; auto using lt_le_weak.
+ - apply sum5; auto.
+ - rewrite plus_comm. apply sum2; auto using lt_le_weak.
+ - apply sum3; auto using lt_le_weak.
 Qed.
 
+(** [MERGE_EQ] *)
 
-(* \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. *)
-
-Definition divide_and_approx (k1 k2 : int) (body : term)
-  (t : nat) (prop : proposition) :=
-  match prop with
-  | LeqTerm (Tint Null) b =>
-      if beq Null 0 &&
-         eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b &&
-         bgt k1 0 &&
-         bgt k1 k2
-      then LeqTerm (Tint 0) body
-      else prop
-  | _ => prop
-  end.
-
-Theorem divide_and_approx_valid :
- forall (k1 k2 : int) (body : term) (t : nat),
- valid1 (divide_and_approx k1 k2 body t).
-Proof.
- unfold valid1, divide_and_approx; intros k1 k2 body t ep e p1;
- Simplify; simpl; auto; subst;
- elim (scalar_norm_add_stable t e); simpl.
- intro H2; apply mult_le_approx with (3 := H2); assumption.
-Qed.
-
-(* \paragraph{[MERGE_EQ]} *)
-
-Definition merge_eq (t : nat) (prop1 prop2 : proposition) :=
+Definition merge_eq (prop1 prop2 : proposition) :=
   match prop1 with
-  | LeqTerm (Tint Null) b1 =>
+  | LeqTerm (Tint o) b1 =>
       match prop2 with
-      | LeqTerm (Tint Null') b2 =>
-          if beq Null 0 && beq Null' 0 &&
-             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
+      | LeqTerm (Tint o') b2 =>
+          if (o =? 0) && (o' =? 0) &&
+             (b1 =? scalar_mult b2 (-(1)))%term
           then EqTerm (Tint 0) b1
           else TrueTerm
       | _ => TrueTerm
@@ -2370,680 +1603,153 @@ Definition merge_eq (t : nat) (prop1 prop2 : proposition) :=
   | _ => TrueTerm
   end.
 
-Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n).
-Proof.
- unfold valid2, merge_eq; intros n ep e p1 p2; Simplify; simpl;
- auto; elim (scalar_norm_stable n e); simpl;
- intros; symmetry ; apply OMEGA8 with (2 := H0);
- [ assumption | elim opp_eq_mult_neg_1; trivial ].
-Qed.
-
-
-
-(* \paragraph{[O_CONSTANT_NUL]} *)
-
-Definition constant_nul (i : nat) (h : hyps) :=
-  match nth_hyps i h with
-  | NeqTerm (Tint Null) (Tint Null') =>
-      if beq Null Null' then absurd else h
-  | _ => h
-  end.
-
-Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i).
-Proof.
- unfold valid_hyps, constant_nul; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl;
- intro H1; absurd (0 = 0); intuition.
-Qed.
-
-(* \paragraph{[O_STATE]} *)
-
-Definition state (m : int) (s : step) (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)
-          else TrueTerm
-      | _ => TrueTerm
-      end
-  | _ => TrueTerm
-  end.
-
-Theorem state_valid : forall (m : int) (s : step), valid2 (state m s).
+Theorem merge_eq_valid : valid2 merge_eq.
 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, merge_eq; intros ep e p1 p2; Simplify; simpl; auto.
+ rewrite scalar_mult_stable. simpl.
+ intros; symmetry ; apply OMEGA8 with (2 := H0).
+ - assumption.
+ - elim opp_eq_mult_neg_1; trivial.
 Qed.
 
-(* \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). *)
+(** [O_SPLIT_INEQ] (only step to produce two subgoals). *)
 
-Definition split_ineq (i t : nat) (f1 f2 : hyps -> lhyps)
-  (l : hyps) :=
+Definition split_ineq (i : nat) (f1 f2 : hyps -> lhyps) (l : hyps) :=
   match nth_hyps i l with
-  | NeqTerm (Tint Null) b1 =>
-      if beq Null 0 then
-      f1 (LeqTerm (Tint 0) (add_norm t (b1 + Tint (-(1)))%term) :: l) ++
-      f2
-        (LeqTerm (Tint 0)
-           (scalar_norm_add t (b1 * Tint (-(1)) + Tint (-(1)))%term) :: l)
-       else l :: nil
+  | NeqTerm (Tint o) b1 =>
+      if o =? 0 then
+       f1 (LeqTerm (Tint 0) (scalar_add b1 (-(1))) :: l) ++
+       f2 (LeqTerm (Tint 0) (scalar_mult_add b1 (-(1)) (-(1))) :: l)
+      else l :: nil
   | _ => l :: nil
   end.
 
 Theorem split_ineq_valid :
- forall (i t : nat) (f1 f2 : hyps -> lhyps),
+ forall (i : nat) (f1 f2 : hyps -> lhyps),
  valid_list_hyps f1 ->
- valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2).
+ valid_list_hyps f2 -> valid_list_hyps (split_ineq i f1 f2).
 Proof.
- unfold valid_list_hyps, split_ineq; intros i t f1 f2 H1 H2 ep e lp H;
+ unfold valid_list_hyps, split_ineq; intros i f1 f2 H1 H2 ep e lp H;
  generalize (nth_valid _ _ i _ H); case (nth_hyps i lp);
  simpl; auto; intros t1 t2; case t1; simpl;
  auto; intros z; simpl; auto; intro H3.
  Simplify.
- apply append_valid; elim (OMEGA19 (interp_term e t2));
- [ intro H4; left; apply H1; simpl; elim (add_norm_stable t);
-    simpl; auto
- | intro H4; right; apply H2; simpl; elim (scalar_norm_add_stable t);
-    simpl; auto
- | generalize H3; unfold not; intros E1 E2; apply E1;
-    symmetry ; trivial ].
+ apply append_valid; elim (OMEGA19 (interp_term e t2)).
+ - intro H4; left; apply H1; simpl; rewrite scalar_add_stable;
+    simpl; auto.
+ - intro H4; right; apply H2; simpl; rewrite scalar_mult_add_stable;
+    simpl; auto.
+ - generalize H3; unfold not; intros E1 E2; apply E1;
+    symmetry ; trivial.
 Qed.
 
+(** ** Replaying the resolution trace *)
 
-(* \subsection{La fonction de rejeu de la trace} *)
-
-Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
+Fixpoint execute_omega (t : t_omega) (l : hyps) : 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 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)
-  | 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_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_NEGATE_CONTRADICT_INV t i j =>
-      singleton (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)
+  | O_BAD_CONSTANT i => singleton (bad_constant i l)
+  | O_NOT_EXACT_DIVIDE i k => singleton (not_exact_divide i k l)
+  | O_DIVIDE i k cont =>
+      execute_omega cont (apply_oper_1 i (divide k) l)
+  | O_SUM k1 i1 k2 i2 cont =>
+      execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2) l)
+  | O_MERGE_EQ i1 i2 cont =>
+      execute_omega cont (apply_oper_2 i1 i2 merge_eq l)
+  | O_SPLIT_INEQ i cont1 cont2 =>
+      split_ineq i (execute_omega cont1) (execute_omega cont2) l
   end.
 
 Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr).
 Proof.
- simple induction tr; simpl;
- [ unfold valid_list_hyps; simpl; intros; left;
-    apply (constant_not_nul_valid n ep e lp H)
- | 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 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) 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 n t' Ht' m ep e lp H; apply Ht';
+ simple induction tr; unfold valid_list_hyps, valid_hyps; simpl.
+ - intros; left; now apply bad_constant_valid.
+ - intros; left; now apply not_exact_divide_valid.
+ - intros m k t' Ht' ep e lp H; apply Ht';
     apply
-     (apply_oper_1_valid m (exact_divide k body n)
-        (exact_divide_valid k body n) ep e lp H)
- | unfold valid_list_hyps, valid_hyps;
-    intros k1 i1 k2 i2 trace t' Ht' ep e lp H; apply Ht';
+     (apply_oper_1_valid m (divide k)
+        (divide_valid k) ep e lp H).
+ - 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
-        lp H)
- | unfold valid_list_hyps; simpl; intros; left;
-    apply (contradiction_valid n n0 n1 ep e lp H)
- | unfold valid_list_hyps, valid_hyps;
-    intros trace i1 i2 t' Ht' ep e lp H; apply Ht';
+     (apply_oper_2_valid i1 i2 (sum k1 k2) (sum_valid k1 k2) ep e
+        lp H).
+ - intros i1 i2 t' Ht' ep e lp H; apply Ht';
     apply
-     (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; simpl;
-    intros ep e lp H;
+     (apply_oper_2_valid i1 i2 merge_eq merge_eq_valid ep e
+        lp H).
+ - intros i k1 H1 k2 H2 ep e lp H;
     apply
-     (split_ineq_valid i t' (execute_omega k1) (execute_omega k2) H1 H2 ep e
-        lp H)
- | unfold valid_list_hyps; simpl; intros i ep e lp H; left;
-    apply (constant_nul_valid i ep e lp H)
- | unfold valid_list_hyps; simpl; intros i j ep e lp H; left;
-    apply (negate_contradict_valid i j ep e lp H)
- | unfold valid_list_hyps; simpl; 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;
-    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}
-   \subsubsection{Normalisation} *)
-
-Definition move_right (s : step) (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.
-
-Theorem move_right_valid : forall s : step, valid1 (move_right s).
-Proof.
- unfold valid1, move_right; intros s ep e p; 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 ].
-Qed.
-
-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).
-Proof.
- intros; unfold do_normalize; apply apply_oper_1_valid;
- apply move_right_valid.
-Qed.
-
-Fixpoint do_normalize_list (l : list step) (i : nat)
- (h : hyps) {struct l} : hyps :=
-  match l with
-  | s :: l' => do_normalize_list l' (S i) (do_normalize i s h)
-  | nil => h
-  end.
-
-Theorem do_normalize_list_valid :
- forall (l : list step) (i : nat), valid_hyps (do_normalize_list l i).
-Proof.
- simple induction l; simpl; unfold valid_hyps;
- [ auto
- | 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) (ep : list Prop) (env : list int) (l : hyps),
- interp_goal ep env (do_normalize_list s 0 l) -> interp_goal ep env l.
-Proof.
- intros; apply valid_goal with (2 := H); apply do_normalize_list_valid.
+     (split_ineq_valid i (execute_omega k1) (execute_omega k2) H1 H2 ep e
+        lp H).
 Qed.
 
-(* \subsubsection{Exécution de la trace} *)
 
-Theorem execute_goal :
- forall (tr : t_omega) (ep : list Prop) (env : list int) (l : hyps),
- interp_list_goal ep env (execute_omega tr l) -> interp_goal ep env l.
-Proof.
- intros; apply (goal_valid (execute_omega tr) (omega_valid tr) ep env l H).
-Qed.
+(** ** Rules for decomposing the hypothesis
 
+   This type allows navigation in the logical constructors that
+   form the predicats of the hypothesis in order to decompose them.
+   This allows in particular to extract one hypothesis from a conjunction.
+   NB: negations are now silently traversed. *)
 
-Theorem append_goal :
- forall (ep : list Prop) (e : list int) (l1 l2 : lhyps),
- interp_list_goal ep e l1 /\ interp_list_goal ep e l2 ->
- interp_list_goal ep e (l1 ++ l2).
-Proof.
- intros ep e; simple induction l1;
- [ simpl; intros l2 (H1, H2); assumption
- | simpl; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ].
-Qed.
-
-(* 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 : list Prop) (e : list int) (p : proposition),
- decidability p = true -> decidable (interp_proposition ep e p).
-Proof.
- simple induction p; simpl; intros;
- [ apply dec_eq
- | apply dec_le
- | left; auto
- | right; unfold not; auto
- | apply dec_not; auto
- | apply dec_ge
- | apply dec_gt
- | apply dec_lt
- | apply dec_ne
- | 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 : list Prop) (env : list int)
- (c : proposition) (l : hyps) {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 : list Prop) (e : list int)
-  (lc : hyps * 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 : list Prop) (e : list int) (l : hyps) (c : proposition),
- (interp_hyps ep e l -> interp_proposition ep e c) -> interp_full ep e (l, c).
-Proof.
- simple induction l; unfold interp_full; simpl;
- [ 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 : hyps * 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 : list Prop) (e : list int) (lc : hyps * proposition),
- interp_goal ep e (to_contradict lc) -> interp_full ep e lc.
-Proof.
- intros ep e lc; case lc; intros l c; simpl;
- pattern (decidability c); apply bool_eq_ind;
- [ simpl; intros H H1; apply interp_full_false; intros H2;
-    apply not_not;
-    [ apply decidable_correct; assumption
-    | unfold not at 1; 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 : hyps) {struct nn} : lhyps :=
-  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 : list Prop) (e : list int) (p : proposition) (l : lhyps),
- interp_proposition ep e p ->
- interp_list_hyps ep e l -> interp_list_hyps ep e (map_cons _ p l).
-Proof.
- simple induction l; simpl; [ 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).
-Proof.
- simple induction n;
- [ unfold valid_list_hyps; simpl; auto
- | unfold valid_list_hyps at 2; intros n1 H ep e lp; case lp;
-    [ simpl; auto
-    | intros p l; case p;
-       try
-        (simpl; intros; apply map_cons_val; simpl; elim H0;
-          auto);
-       [ intro p'; case p';
-          try
-           (simpl; intros; apply map_cons_val; simpl; elim H0;
-             auto);
-          [ simpl; intros p1 (H1, H2);
-             pattern (decidability p1); apply bool_eq_ind;
-             intro H3;
-             [ apply H; simpl; split;
-                [ apply not_not; auto | assumption ]
-             | auto ]
-          | simpl; intros p1 p2 (H1, H2); apply H; simpl;
-             elim not_or with (1 := H1); auto
-          | simpl; intros p1 p2 (H1, H2);
-             pattern (decidability p1); apply bool_eq_ind;
-             intro H3;
-             [ apply append_valid; elim not_and with (2 := H1);
-                [ intro; left; apply H; simpl; auto
-                | intro; right; apply H; simpl; auto
-                | auto ]
-             | auto ] ]
-       | simpl; intros p1 p2 (H1, H2); apply append_valid;
-          (elim H1; intro H3; simpl; [ left | right ]);
-          apply H; simpl; auto
-       | simpl; intros; apply H; simpl; tauto
-       | simpl; intros p1 p2 (H1, H2);
-          pattern (decidability p1); apply bool_eq_ind;
-          intro H3;
-          [ apply append_valid; elim imp_simp with (2 := H1);
-             [ intro H4; left; simpl; apply H; simpl; auto
-             | intro H4; right; simpl; apply H; simpl; auto
-             | auto ]
-          | auto ] ] ] ].
-Qed.
-
-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; split;
- (case p; simpl; 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).
-Proof.
- unfold prop_stable; intros f H ep e p; split;
- (case p; simpl; auto;
-   [ intros t1 t2; elim (H ep e (NeqTerm t1 t2)); simpl;
-      generalize (dec_eq (interp_term e t1) (interp_term e t2));
-      unfold decidable; tauto
-   | intros t1 t2; elim (H ep e (GtTerm t1 t2)); simpl;
-      generalize (dec_gt (interp_term e t1) (interp_term e t2));
-      unfold decidable; rewrite le_lt_iff, <- gt_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl;
-      generalize (dec_lt (interp_term e t1) (interp_term e t2));
-      unfold decidable; rewrite ge_le_iff, le_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl;
-      generalize (dec_gt (interp_term e t1) (interp_term e t2));
-      unfold decidable; repeat rewrite le_lt_iff;
-      repeat rewrite gt_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl;
-      generalize (dec_lt (interp_term e t1) (interp_term e t2));
-      unfold decidable; repeat rewrite ge_le_iff;
-      repeat rewrite le_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (EqTerm t1 t2)); simpl;
-      generalize (dec_eq (interp_term e t1) (interp_term e t2));
-      unfold decidable; tauto ]).
-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;
-       rewrite plus_permute; rewrite plus_opp_r;
-       rewrite plus_0_r; trivial
-    | apply (fun a b => plus_le_reg_r a b (- interp_term e 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; rewrite 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)
-  | P_NOP => fun p : proposition => p
-  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
- | unfold prop_stable; simpl; intros; split; auto ].
-Qed.
+Inductive direction : Set :=
+  | D_left : direction
+  | D_right : direction.
 
-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.
+(** This type allows extracting useful components from hypothesis, either
+   hypothesis generated by splitting a disjonction, or equations.
+   The last constructor indicates how to solve the obtained system
+   via the use of the trace type of Omega [t_omega] *)
 
-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.
+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.
 
-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.
-Proof.
- intros; apply valid_goal with (2 := H); apply normalize_hyps_valid.
-Qed.
+(** Selection of a basic fact inside an hypothesis. *)
 
-Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} :
+Fixpoint extract_hyp_pos (s : list direction) (p : proposition) :
  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
+  match p, s with
+  | Tand x y, D_left :: l => extract_hyp_pos l x
+  | Tand x y, D_right :: l => extract_hyp_pos l y
+  | Tnot x, _ => extract_hyp_neg s x
+  | _, _ => p
   end
 
- with extract_hyp_neg (s : list direction) (p : proposition) {struct s} :
+ with extract_hyp_neg (s : list direction) (p : proposition) :
  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
+  match p, s with
+  | Tor x y, D_left :: l => extract_hyp_neg l x
+  | Tor x y, D_right :: l => extract_hyp_neg l y
+  | Timp x y, D_left :: l =>
+    if decidability x then extract_hyp_pos l x else Tnot p
+  | Timp x y, D_right :: l => extract_hyp_neg l y
+  | Tnot x, _ => if decidability x then extract_hyp_pos s x else Tnot p
+  | _, _ => Tnot p
   end.
 
-Definition co_valid1 (f : proposition -> proposition) :=
-  forall (ep : list Prop) (e : list int) (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).
+ forall s : list direction, valid1 (extract_hyp_pos s).
 Proof.
- unfold valid1, co_valid1; simple induction s;
- [ split;
-    [ simpl; auto
-    | intros ep e p1; case p1; simpl; auto; intro p;
-       pattern (decidability p); apply bool_eq_ind;
-       [ intro H; generalize (decidable_correct ep e p H);
-          unfold decidable; tauto
-       | simpl; auto ] ]
- | intros a s' (H1, H2); simpl in H2; split; intros ep e p; case a; auto;
-    case p; auto; simpl; intros;
-    (apply H1; tauto) ||
-      (apply H2; tauto) ||
-        (pattern (decidability p0); apply bool_eq_ind;
-          [ intro H3; generalize (decidable_correct ep e p0 H3);
-             unfold decidable; intro H4; apply H1;
-             tauto
-          | intro; tauto ]) ].
+ assert (forall p s ep e,
+         (interp_prop ep e p ->
+          interp_prop ep e (extract_hyp_pos s p)) /\
+         (interp_prop ep e (Tnot p) ->
+          interp_prop ep e (extract_hyp_neg s p))).
+ { induction p; destruct s; simpl; auto; split; try destruct d; try easy;
+   intros; (apply IHp || apply IHp1 || apply IHp2 || idtac); simpl; try tauto;
+   destruct decidability eqn:D; auto;
+   apply (decidable_correct ep e) in D; unfold decidable in D;
+   (apply IHp || apply IHp1); tauto. }
+ red. intros. now apply H.
 Qed.
 
-Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
+(** Attempt to shorten error messages if romega goes rogue...
+    NB: [interp_list_goal _ _ BUG = False /\ True]. *)
+Definition BUG : lhyps := nil :: nil.
+
+(** Split and extract in hypotheses *)
+
+Fixpoint decompose_solve (s : e_step) (h : hyps) : lhyps :=
   match s with
   | E_SPLIT i dl s1 s2 =>
       match extract_hyp_pos dl (nth_hyps i h) with
@@ -3053,50 +1759,45 @@ Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
           then
            decompose_solve s1 (Tnot x :: h) ++
            decompose_solve s2 (Tnot y :: h)
-          else h :: nil
+          else BUG
       | Timp x y =>
           if decidability x then
             decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (y :: h)
-          else h::nil
-      | _ => h :: nil
+          else BUG
+      | _ => BUG
       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).
-Proof.
- intro s; apply goal_valid; unfold valid_list_hyps; elim s;
- simpl; intros;
- [ cut (interp_proposition ep e1 (extract_hyp_pos l (nth_hyps n lp)));
-    [ case (extract_hyp_pos l (nth_hyps n lp)); simpl; auto;
-       [ intro p; case p; simpl; auto; intros p1 p2 H2;
-          pattern (decidability p1); apply bool_eq_ind;
-          [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4;
-             apply append_valid; elim H4; intro H5;
-             [ right; apply H0; simpl; tauto
-             | left; apply H; simpl; tauto ]
-          | simpl; auto ]
-       | intros p1 p2 H2; apply append_valid; simpl; elim H2;
-          [ intros H3; left; apply H; simpl; auto
-          | intros H3; right; apply H0; simpl; auto ]
-       | intros p1 p2 H2;
-         pattern (decidability p1); apply bool_eq_ind;
-          [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4;
-             apply append_valid; elim H4; intro H5;
-             [ right; apply H0; simpl; tauto
-             | left; apply H; simpl; tauto ]
-          | simpl; auto ] ]
-    | elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto ]
- | intros; apply H; simpl; 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} *)
+Theorem decompose_solve_valid (s : e_step) :
+ valid_list_goal (decompose_solve s).
+Proof.
+ apply goal_valid. red. induction s; simpl; intros ep e lp H.
+ - assert (H' : interp_prop ep e (extract_hyp_pos l (nth_hyps n lp))).
+   { now apply extract_valid, nth_valid. }
+   destruct extract_hyp_pos; simpl in *; auto.
+   + destruct p; simpl; auto.
+     destruct decidability eqn:D; [ | simpl; auto].
+     apply (decidable_correct ep e) in D.
+     apply append_valid. simpl in *. destruct D.
+     * right. apply IHs2. simpl; auto.
+     * left. apply IHs1. simpl; auto.
+   + apply append_valid. destruct H'.
+     * left. apply IHs1. simpl; auto.
+     * right. apply IHs2. simpl; auto.
+   + destruct decidability eqn:D; [ | simpl; auto].
+     apply (decidable_correct ep e) in D.
+     apply append_valid. destruct D.
+     * right. apply IHs2. simpl; auto.
+     * left. apply IHs1. simpl; auto.
+ - apply IHs; simpl; split; auto.
+   now apply extract_valid, nth_valid.
+ - now apply omega_valid.
+Qed.
+
+(** Reduction of subgoal list by discarding the contradictory subgoals. *)
 
 Definition valid_lhyps (f : lhyps -> lhyps) :=
   forall (ep : list Prop) (e : list int) (lp : lhyps),
@@ -3104,18 +1805,18 @@ Definition valid_lhyps (f : lhyps -> lhyps) :=
 
 Fixpoint reduce_lhyps (lp : lhyps) : lhyps :=
   match lp with
+  | nil => nil
   | (FalseTerm :: nil) :: lp' => reduce_lhyps lp'
-  | x :: lp' => x :: reduce_lhyps lp'
-  | nil => nil (A:=hyps)
+  | x :: lp' => BUG
   end.
 
 Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps.
 Proof.
- unfold valid_lhyps; intros ep e lp; elim lp;
- [ simpl; auto
- | intros a l HR; elim a;
-    [ simpl; tauto
-    | intros a1 l1; case l1; case a1; simpl; try tauto ] ].
+ unfold valid_lhyps; intros ep e lp; elim lp.
+ - simpl; auto.
+ - intros a l HR; elim a.
+    + simpl; tauto.
+    + intros a1 l1; case l1; case a1; simpl; tauto.
 Qed.
 
 Theorem do_reduce_lhyps :
@@ -3127,6 +1828,8 @@ Proof.
  assumption.
 Qed.
 
+(** Pushing the conclusion into the hypotheses. *)
+
 Definition concl_to_hyp (p : proposition) :=
   if decidability p then Tnot p else TrueTerm.
 
@@ -3135,33 +1838,35 @@ Definition do_concl_to_hyp :
   interp_goal envp env (concl_to_hyp c :: l) ->
   interp_goal_concl c envp env l.
 Proof.
- simpl; intros envp env c l; induction l as [| a l Hrecl];
- [ simpl; unfold concl_to_hyp;
-    pattern (decidability c); apply bool_eq_ind;
-    [ intro H; generalize (decidable_correct envp env c H);
-       unfold decidable; simpl; tauto
-    | simpl; intros H1 H2; elim H2; trivial ]
- | simpl; tauto ].
+ induction l; simpl.
+ - unfold concl_to_hyp; simpl.
+   destruct decidability eqn:D; [ | simpl; tauto ].
+   apply (decidable_correct envp env) in D. unfold decidable in D.
+   simpl. tauto.
+ - 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))).
+(** The omega tactic : all steps together *)
+
+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.
 
-(* For now, the above modular construction is instanciated on Z,
-   in order to retrieve the initial ROmega. *)
+(** For now, the above modular construction is instanciated on Z,
+    in order to retrieve the initial ROmega. *)
 
 Module ZOmega := IntOmega(Z_as_Int).
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 8d7ae51fc..a10ce68b4 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -10,10 +10,10 @@ let module_refl_name = "ReflOmegaCore"
 let module_refl_path = ["Coq"; "romega"; module_refl_name]
 
 type result =
-   Kvar of string
- | Kapp of string * Term.constr list
- | Kimp of Term.constr * Term.constr
- | Kufo;;
+  | Kvar of string
+  | Kapp of string * Term.constr list
+  | Kimp of Term.constr * Term.constr
+  | Kufo
 
 let meaningful_submodule = [ "Z"; "N"; "Pos" ]
 
@@ -30,19 +30,17 @@ let string_of_global r =
 let destructurate t =
   let c, args = Term.decompose_app t in
   match Term.kind_of_term c, args with
-    | Term.Const (sp,_), args ->
-	Kapp (string_of_global (Globnames.ConstRef sp), args)
-    | Term.Construct (csp,_) , args ->
-	Kapp (string_of_global (Globnames.ConstructRef csp), args)
-    | Term.Ind (isp,_), args ->
-	Kapp (string_of_global (Globnames.IndRef isp), args)
-    | Term.Var id,[] -> Kvar(Names.Id.to_string id)
-    | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
-    | Term.Prod (Names.Name _,_,_),[] ->
-	CErrors.error "Omega: Not a quantifier-free goal"
-    | _ -> Kufo
-
-exception Destruct
+  | Term.Const (sp,_), args ->
+     Kapp (string_of_global (Globnames.ConstRef sp), args)
+  | Term.Construct (csp,_) , args ->
+     Kapp (string_of_global (Globnames.ConstructRef csp), args)
+  | Term.Ind (isp,_), args ->
+     Kapp (string_of_global (Globnames.IndRef isp), args)
+  | Term.Var id, [] -> Kvar(Names.Id.to_string id)
+  | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
+  | _ -> Kufo
+
+exception DestConstApp
 
 let dest_const_apply t =
   let f,args = Term.decompose_app t in
@@ -51,8 +49,8 @@ let dest_const_apply t =
     | Term.Const (sp,_)      -> Globnames.ConstRef sp
     | Term.Construct (csp,_) -> Globnames.ConstructRef csp
     | Term.Ind (isp,_)       -> Globnames.IndRef isp
-    | _ -> raise Destruct
-  in  Nametab.basename_of_global ref, args
+    | _ -> raise DestConstApp
+  in Nametab.basename_of_global ref, args
 
 let logic_dir = ["Coq";"Logic";"Decidable"]
 
@@ -81,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")
@@ -110,62 +101,17 @@ 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")
+let coq_s_bad_constant = lazy (constant  "O_BAD_CONSTANT")
+let coq_s_divide = lazy (constant  "O_DIVIDE")
 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")
@@ -174,31 +120,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")
@@ -235,8 +156,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
@@ -263,18 +182,40 @@ type parse_rel =
   | Riff of Term.constr * Term.constr
   | Rother
 
-let parse_logic_rel c =
- try match destructurate c with
-   | Kapp("True",[]) -> Rtrue
-   | Kapp("False",[]) -> Rfalse
-   | Kapp("not",[t]) -> Rnot t
-   | Kapp("or",[t1;t2]) -> Ror (t1,t2)
-   | Kapp("and",[t1;t2]) -> Rand (t1,t2)
-   | Kimp(t1,t2) -> Rimp (t1,t2)
-   | Kapp("iff",[t1;t2]) -> Riff (t1,t2)
-   | _ -> Rother
- with e when Logic.catchable_exception e -> Rother
+let parse_logic_rel c = match destructurate c with
+  | Kapp("True",[]) -> Rtrue
+  | Kapp("False",[]) -> Rfalse
+  | Kapp("not",[t]) -> Rnot t
+  | Kapp("or",[t1;t2]) -> Ror (t1,t2)
+  | Kapp("and",[t1;t2]) -> Rand (t1,t2)
+  | Kimp(t1,t2) -> Rimp (t1,t2)
+  | Kapp("iff",[t1;t2]) -> Riff (t1,t2)
+  | _ -> Rother
+
+(* Binary numbers *)
+
+let coq_xH = lazy (bin_constant "xH")
+let coq_xO = lazy (bin_constant "xO")
+let coq_xI = lazy (bin_constant "xI")
+let coq_Z0 = lazy (bin_constant "Z0")
+let coq_Zpos = lazy (bin_constant "Zpos")
+let coq_Zneg = lazy (bin_constant "Zneg")
+let coq_N0 = lazy (bin_constant "N0")
+let coq_Npos = lazy (bin_constant "Npos")
+
+let rec mk_positive n =
+  if Bigint.equal n Bigint.one then Lazy.force coq_xH
+  else
+    let (q,r) = Bigint.euclid n Bigint.two in
+    Term.mkApp
+      ((if Bigint.equal r Bigint.zero
+        then Lazy.force coq_xO else Lazy.force coq_xI),
+       [| mk_positive q |])
 
+let mk_N = function
+  | 0 -> Lazy.force coq_N0
+  | n -> Term.mkApp (Lazy.force coq_Npos,
+                     [| mk_positive (Bigint.of_int n) |])
 
 module type Int = sig
   val typ : Term.constr Lazy.t
@@ -287,7 +228,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
@@ -298,38 +239,29 @@ let mult = lazy (z_constant  "Z.mul")
 let opp = lazy (z_constant "Z.opp")
 let minus = lazy (z_constant "Z.sub")
 
-let coq_xH = lazy (bin_constant "xH")
-let coq_xO = lazy (bin_constant "xO")
-let coq_xI = lazy (bin_constant "xI")
-let coq_Z0 = lazy (bin_constant "Z0")
-let coq_Zpos = lazy (bin_constant "Zpos")
-let coq_Zneg = lazy (bin_constant "Zneg")
-
-let recognize t =
+let recognize_pos t =
   let rec loop t =
     let f,l = dest_const_apply t in
     match Names.Id.to_string f,l with
-       "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
-     | "xO",[t] -> Bigint.mult Bigint.two (loop t)
-     | "xH",[] -> Bigint.one
-     | _ -> failwith "not a number" in
-  let f,l = dest_const_apply t in
-    match Names.Id.to_string f,l with
-        "Zpos",[t] -> loop t
-      | "Zneg",[t] -> Bigint.neg (loop t)
-      | "Z0",[] -> Bigint.zero
-      | _ -> failwith "not a number";;
+    | "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
+    | "xO",[t] -> Bigint.mult Bigint.two (loop t)
+    | "xH",[] -> Bigint.one
+    | _ -> raise DestConstApp
+  in
+  try Some (loop t) with DestConstApp -> None
 
-let rec mk_positive n =
-  if n=Bigint.one then Lazy.force coq_xH
-  else
-    let (q,r) = Bigint.euclid n Bigint.two in
-    Term.mkApp
-      ((if r = Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI),
-       [| mk_positive q |])
+let recognize_Z t =
+  try
+    let f,l = dest_const_apply t in
+    match Names.Id.to_string f,l with
+    | "Zpos",[t] -> recognize_pos t
+    | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos t)
+    | "Z0",[] -> Some Bigint.zero
+    | _ -> None
+  with DestConstApp -> None
 
 let mk_Z n =
-  if n = Bigint.zero then Lazy.force coq_Z0
+  if Bigint.equal n Bigint.zero then Lazy.force coq_Z0
   else if Bigint.is_strictly_pos n then
     Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
   else
@@ -338,38 +270,46 @@ let mk_Z n =
 let mk = mk_Z
 
 let parse_term t =
-  try match destructurate t with
-    | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2)
-    | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2)
-    | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2)
-    | Kapp("Z.opp",[t]) -> Topp t
-    | Kapp("Z.succ",[t]) -> Tsucc t
-    | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
-    | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
-	(try Tnum (recognize t) with e when CErrors.noncritical e -> Tother)
-    | _ -> Tother
-  with e when Logic.catchable_exception e -> Tother
-
-let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c
+  match destructurate t with
+  | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2)
+  | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2)
+  | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2)
+  | Kapp("Z.opp",[t]) -> Topp t
+  | Kapp("Z.succ",[t]) -> Tsucc t
+  | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
+  | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
+     (match recognize_Z t with Some t -> Tnum t | None -> Tother)
+  | _ -> Tother
+
+let pf_nf gl c =
+  EConstr.Unsafe.to_constr
+    (Tacmach.New.pf_apply Tacred.simpl gl (EConstr.of_constr c))
 
 let parse_rel gl t =
-  try match destructurate t with
-    | Kapp("eq",[typ;t1;t2])
-      when destructurate (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2)
-    | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
-    | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
-    | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
-    | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2)
-    | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2)
-    | _ -> parse_logic_rel t
-  with e when Logic.catchable_exception e -> Rother
-
-let is_scalar t =
-  let rec aux t = match destructurate t with
-    | Kapp(("Z.add"|"Z.sub"|"Z.mul"),[t1;t2]) -> aux t1 && aux t2
-    | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t
-    | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
-    | _ -> false in
-  try aux t with e when CErrors.noncritical e -> false
+  match destructurate t with
+  | Kapp("eq",[typ;t1;t2]) ->
+     (match destructurate (pf_nf gl typ) with
+      | Kapp("Z",[]) -> Req (t1,t2)
+      | _ -> Rother)
+  | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
+  | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
+  | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
+  | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2)
+  | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2)
+  | _ -> parse_logic_rel t
+
+let rec get_scalar t =
+  match destructurate t with
+  | 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 ee7ff451a..ca23ed6c4 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,58 +42,16 @@ 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
+val coq_s_bad_constant : Term.constr lazy_t
+val coq_s_divide : Term.constr lazy_t
 val coq_s_not_exact_divide : Term.constr lazy_t
-val coq_s_exact_divide : Term.constr lazy_t
 val coq_s_sum : Term.constr lazy_t
-val coq_s_state : Term.constr lazy_t
-val coq_s_contradiction : Term.constr lazy_t
 val coq_s_merge_eq : Term.constr lazy_t
 val coq_s_split_ineq : Term.constr lazy_t
-val coq_s_constant_nul : Term.constr lazy_t
-val coq_s_negate_contradict : Term.constr lazy_t
-val coq_s_negate_contradict_inv : Term.constr lazy_t
 
 val coq_direction : Term.constr lazy_t
 val coq_d_left : Term.constr lazy_t
 val coq_d_right : Term.constr lazy_t
-val coq_d_mono : Term.constr lazy_t
 
 val coq_e_split : Term.constr lazy_t
 val coq_e_extract : Term.constr lazy_t
@@ -108,19 +60,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 *)
 
@@ -170,7 +115,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/g_romega.ml4 b/plugins/romega/g_romega.ml4
index df7e5cb99..c2d7d5050 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -21,7 +21,7 @@ let eval_tactic name =
   let tac = Tacenv.interp_ltac kn in
   Tacinterp.eval_tactic tac
 
-let romega_tactic l =
+let romega_tactic unsafe l =
   let tacs = List.map
     (function
        | "nat" -> eval_tactic "zify_nat"
@@ -38,15 +38,15 @@ let romega_tactic l =
           we'd better leave as little as possible in the conclusion,
           for an easier decidability argument. *)
        (Tactics.intros)
-       (total_reflexive_omega_tactic))
-
+       (total_reflexive_omega_tactic unsafe))
 
 TACTIC EXTEND romega
-|  [ "romega" ] -> [ romega_tactic [] ]
+|  [ "romega" ] -> [ romega_tactic false [] ]
+|  [ "unsafe_romega" ] -> [ romega_tactic true [] ]
 END
 
 TACTIC EXTEND romega'
 | [ "romega" "with" ne_ident_list(l) ] ->
-    [ romega_tactic (List.map Names.Id.to_string l) ]
-| [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ]
+    [ romega_tactic false (List.map Names.Id.to_string l) ]
+| [ "romega" "with" "*" ] -> [ romega_tactic false ["nat";"positive";"N";"Z"] ]
 END
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index a20589fb4..e56605076 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -13,6 +13,10 @@ open Const_omega
 module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
 
+module Id = Names.Id
+module IntSet = Int.Set
+module IntHtbl = Hashtbl.Make(Int)
+
 (* \section{Useful functions and flags} *)
 (* Especially useful debugging functions *)
 let debug = ref false
@@ -38,13 +42,11 @@ type direction = Left of int | Right of int
 type occ_step = O_left | O_right | O_mono
 type occ_path = occ_step list
 
-let occ_step_eq s1 s2 = match s1, s2 with
-| O_left, O_left | O_right, O_right | O_mono, O_mono -> true
-| _ -> false
-
 (* 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 occurrence = {o_hyp : Names.Id.t; o_path : occ_path}
+type occurrence = {o_hyp : Id.t; o_path : occ_path}
+
+type atom_index = int
 
 (* \subsection{reifiable formulas} *)
 type oformula =
@@ -52,21 +54,22 @@ type oformula =
   | 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
 
-(* Type des prédicats réifiés (fragment de calcul propositionnel. Les
- * quantifications sont externes au langage) *)
+(* Representation of reified predicats (fragment of propositional calculus,
+   no quantifier here). *)
+(* Note : in [Pprop p], the non-reified constr [p] should be closed
+   (it could contains some [Term.Var] but no [Term.Rel]). So no need to
+   lift when breaking or creating arrows. *)
 type oproposition =
-    Pequa of Term.constr * oequation
+    Pequa of Term.constr * oequation (* constr = copy of the Coq formula *)
   | Ptrue
   | Pfalse
   | Pnot of oproposition
@@ -75,19 +78,18 @@ type oproposition =
   | Pimp of int * oproposition * oproposition
   | Pprop of Term.constr
 
-(* Les équations ou propositions atomiques utiles du calcul *)
+(* The equations *)
 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 *)
-    e_depends: direction  list;		(* liste des points de disjonction dont
+    e_depends: direction list;		(* liste des points de disjonction dont
 					   dépend l'accès à l'équation avec la
 					   direction (branche) pour y accéder *)
-    e_omega: afine		(* la fonction normalisée *)
+    e_omega: OmegaSolver.afine (* normalized formula *)
   }
 
 (* \subsection{Proof context}
@@ -104,24 +106,22 @@ type environment = {
   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;
+  real_indices : int IntHtbl.t;
   mutable cnt_connectors : int;
-  equations : (int,oequation) Hashtbl.t;
-  constructors : (int, occurrence) Hashtbl.t
+  equations : oequation IntHtbl.t;
+  constructors : occurrence IntHtbl.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 *)
-(* La liste des dépendances est triée et sans redondance *)
+
 type solution = {
   s_index : int;
-  s_equa_deps : int list;
-  s_trace : action list }
+  s_equa_deps : IntSet.t;
+  s_trace : OmegaSolver.action list }
 
 (* Arbre de solution résolvant complètement un ensemble de systèmes *)
 type solution_tree =
@@ -139,16 +139,35 @@ type context_content =
     CCHyp of occurrence
   | CCEqua of int
 
+(** Some dedicated equality tests *)
+
+let occ_step_eq s1 s2 = match s1, s2 with
+| O_left, O_left | O_right, O_right | O_mono, O_mono -> true
+| _ -> false
+
+let rec oform_eq f f' = match f,f' with
+  | Oint i, Oint i' -> Bigint.equal i i'
+  | Oplus (f1,f2), Oplus (f1',f2')
+  | Omult (f1,f2), Omult (f1',f2')
+  | 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'
+  | _ -> false
+
+let dir_eq d d' = match d, d' with
+  | Left i, Left i' | Right i, Right i' -> Int.equal i i'
+  | _ -> false
+
 (* \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__"
+let id_concl = 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;
+  terms = []; props = []; cnt_connectors = 0;
+  real_indices = IntHtbl.create 7;
+  equations = IntHtbl.create 7;
+  constructors = IntHtbl.create 7;
 }
 
 (* Génération d'un nom d'équation *)
@@ -178,44 +197,22 @@ 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 new_omega_var, rst_omega_var, set_omega_maxvar =
+  let cpt = ref (-1) in
   (function () -> incr cpt; !cpt),
-  (function () -> cpt:=0)
+  (function () -> cpt:=(-1)),
+  (function n -> cpt:=n)
 
 (* 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) *)
-
-let intern_omega env t =
-  begin try List.assoc_f Pervasives.(=) t env.om_vars (* FIXME *)
-  with Not_found ->
-    let v = new_omega_var () in
-    env.om_vars <- (t,v) :: env.om_vars; v
-  end
-
-(* 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
-
-(* 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
-
 (* \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
@@ -231,6 +228,13 @@ let add_reified_atom t env =
 let get_reified_atom env =
   try List.nth env.terms with Invalid_argument _ -> failwith "get_reified_atom"
 
+(** When the omega resolution has created a variable [v], we re-sync
+    the environment with this new variable. To be done in the right order. *)
+
+let set_reified_atom v t env =
+  assert (Int.equal v (List.length env.terms));
+  env.terms <- env.terms @ [t]
+
 (* \subsection{Gestion de l'environnement de proposition pour Omega} *)
 (* ajout d'une proposition *)
 let add_prop env t =
@@ -246,12 +250,11 @@ let get_prop v env =
 (* Ajout d'une equation dans l'environnement de reification *)
 let add_equation env e =
   let id = e.e_omega.id in
-  try let _ = Hashtbl.find env.equations id in ()
-  with Not_found -> Hashtbl.add env.equations id e
+  if IntHtbl.mem env.equations id then () else IntHtbl.add env.equations id e
 
 (* accès a une equation *)
 let get_equation env id =
-  try Hashtbl.find env.equations id
+  try IntHtbl.find env.equations id
   with Not_found as e ->
     Printf.printf "Omega Equation %d non trouvée\n" id; raise e
 
@@ -263,15 +266,14 @@ 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 -> ">="
+  | Gt -> ">" | Lt -> "<" | Neq -> "!="
 
 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
+      Printf.fprintf ch "%a %s %a" oprint t1 (print_comp comp) oprint t2
   | Ptrue -> Printf.fprintf ch "TT"
   | Pfalse -> Printf.fprintf ch "FF"
   | Pnot t -> Printf.fprintf ch "not(%a)" pprint t
@@ -280,38 +282,13 @@ 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 =
+let oformula_of_omega af =
   let rec loop = function
-    | ({v=v; c=n}::r) ->
-	Oplus(Omult(unintern_omega env v,Oint n),loop r)
-    | [] -> Oint af.constant in
+    | ({v=v; c=n}::r) -> Oplus(Omult(Oatom v,Oint n),loop r)
+    | [] -> Oint af.constant
+  in
   loop af.body
 
 let app f v = mkApp(Lazy.force f,v)
@@ -324,7 +301,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 *)
@@ -335,77 +311,59 @@ let coq_of_formula env t =
 (* \subsection{Oformula vers COQ reifié} *)
 
 let reified_of_atom env i =
-  try Hashtbl.find env.real_indices i
+  try IntHtbl.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;
+    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
-  | Oatom i -> app coq_t_var [| mk_nat (reified_of_atom env i) |]
-  | Ominus(t1,t2) ->
-      app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |]
+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) |]
 
 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é} *)
-
-let reified_of_omega env body constant =
-  let coeff_constant =
-    app coq_t_int [| Z.mk constant |] in
-  let mk_coeff {c=c; v=v} t =
-    let coef =
-      app coq_t_mult
-	[| reified_of_formula env (unintern_omega env v);
-	   app coq_t_int [| Z.mk c |] |] in
-    app coq_t_plus [|coef; t |] in
-  List.fold_right mk_coeff body coeff_constant
-
-let reified_of_omega env body c  =
-  try reified_of_omega env body c
-  with reraise -> display_eq display_omega_var (body,c); raise reraise
+let reified_of_eq env (l,r) =
+  app coq_p_eq [| reified_of_formula env l; reified_of_formula env r |]
 
 (* \section{Opérations sur les équations}
 Ces fonctions préparent les traces utilisées par la tactique réfléchie
@@ -415,19 +373,18 @@ pour faire des opérations de normalisation sur les équations.  *)
 (* Extraction des variables d'une équation. *)
 (* Chaque fonction retourne une liste triée sans redondance *)
 
-let (@@) = List.merge_uniq compare
+let (@@) = IntSet.union
 
 let rec vars_of_formula = function
-  | Oint _ -> []
+  | Oint _ -> IntSet.empty
   | 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 _ -> []
+  | Oatom i -> IntSet.singleton i
 
 let rec vars_of_equations = function
-  | [] -> []
+  | [] -> IntSet.empty
   | e::l ->
       (vars_of_formula e.e_left) @@
       (vars_of_formula e.e_right) @@
@@ -439,247 +396,101 @@ let rec vars_of_prop = function
   | Por(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
   | Pand(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
   | Pimp(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
-  | Pprop _ | Ptrue | Pfalse -> []
-
-(* \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] *)
+  | Pprop _ | Ptrue | Pfalse -> IntSet.empty
+
+(* 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.bigint) list;
+    cst : Bigint.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 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
+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 } in
+      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)) EQUA
-    | Neq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) DISE
-    | Leq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oopp o1)) INEQ
-    | Geq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) INEQ
-    | Lt  ->
-        mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o2,Oint negone),Oopp o1))
-	  INEQ
-    | Gt ->
-        mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o1,Oint negone),Oopp o2))
-	  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 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 t env)
 
 and binop env c t1 t2 =
   let t1' = oformula_of_constr env t1 in
@@ -692,7 +503,7 @@ and binprop env (neg2,depends,origin,path)
   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};
+    IntHtbl.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' =
@@ -704,7 +515,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)
 
@@ -719,107 +530,83 @@ 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) ->
-	binprop env ctxt negated negated gl
-	  (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1)
+       (* No lifting here, since Omega only works on closed propositions. *)
+       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 *)
 
+let display_gl env t_concl t_lhyps =
+  Printf.printf "REIFED PROBLEM\n\n";
+  Printf.printf "  CONCL: %a\n" pprint t_concl;
+  List.iter
+    (fun (i,t) -> Printf.printf "  %s: %a\n" (Id.to_string i) pprint t)
+    t_lhyps;
+  print_env_reification env
+
 let reify_gl env gl =
   let concl = Tacmach.New.pf_concl gl in
   let concl = EConstr.Unsafe.to_constr concl in
+  let hyps = Tacmach.New.pf_hyps_types gl in
+  let hyps = List.map (fun (i,t) -> (i,EConstr.Unsafe.to_constr t)) hyps in
   let t_concl =
-    Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in
-  if !debug then begin
-    Printf.printf "REIFED PROBLEM\n\n";
-    Printf.printf "  CONCL: "; pprint stdout t_concl; Printf.printf "\n"
-  end;
-  let rec loop = function
-      (i,t) :: lhyps ->
-        let t = EConstr.Unsafe.to_constr t in
-	let t' = oproposition_of_constr env (false,[],i,[]) gl t in
-	if !debug then begin
-	  Printf.printf "  %s: " (Names.Id.to_string 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.New.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
+    oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl in
+  let t_lhyps =
+    List.map
+      (fun (i,t) -> i,oproposition_of_constr env (false,[],i,[]) gl t)
+      hyps
+  in
+  let () = if !debug then display_gl env t_concl t_lhyps in
+  t_concl, t_lhyps
+
+let rec destruct_pos_hyp eqns = function
+  | Pequa (_,e) -> [e :: eqns]
+  | Ptrue | Pfalse | Pprop _ -> [eqns]
+  | Pnot t -> destruct_neg_hyp eqns t
+  | Por (_,t1,t2) ->
+      let s1 = destruct_pos_hyp eqns t1 in
+      let s2 = destruct_pos_hyp eqns 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
+  | Pand(_,t1,t2) ->
+      List.map_append
+        (fun le1 -> destruct_pos_hyp le1 t2)
+        (destruct_pos_hyp eqns t1)
+  | Pimp(_,t1,t2) ->
+      let s1 = destruct_neg_hyp eqns t1 in
+      let s2 = destruct_pos_hyp eqns 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
+and destruct_neg_hyp eqns = function
+  | Pequa (_,e) -> [e :: eqns]
+  | Ptrue | Pfalse | Pprop _ -> [eqns]
+  | Pnot t -> destruct_pos_hyp eqns t
+  | Pand (_,t1,t2) ->
+      let s1 = destruct_neg_hyp eqns t1 in
+      let s2 = destruct_neg_hyp eqns 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
+      List.map_append
+        (fun le1 -> destruct_neg_hyp le1 t2)
+        (destruct_neg_hyp eqns t1)
   | 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
-	List.cartesian (@) l_syst1 l_syst2
-    | [] -> [[]] in
-  loop syst
+      List.map_append
+        (fun le1 -> destruct_neg_hyp le1 t2)
+        (destruct_pos_hyp eqns t1)
+
+let rec destructurate_hyps = function
+  | [] -> [[]]
+  | (i,t) :: l ->
+     let l_syst1 = destruct_pos_hyp [] t in
+     let l_syst2 = destructurate_hyps l in
+     List.cartesian (@) l_syst1 l_syst2
 
 (* \subsection{Affichage d'un système d'équation} *)
 
@@ -837,7 +624,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;
@@ -846,7 +633,7 @@ let display_systems syst_list =
 	 (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\n"
-      (Names.Id.to_string oformula_eq.e_origin.o_hyp)
+      (Id.to_string oformula_eq.e_origin.o_hyp)
       (if oformula_eq.e_negated then "yes" else "no") in
 
   let display_system syst =
@@ -858,59 +645,61 @@ let display_systems syst_list =
    calcul des hypothèses *)
 
 let rec hyps_used_in_trace = function
+  | [] -> IntSet.empty
   | act :: l ->
-      begin match act with
-	| HYP e -> [e.id] @@ (hyps_used_in_trace l)
-	| 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
-	| STATE action ->
-	    (*i nlle_equa: afine, def: afine, eq_orig: afine, i*)
-            (*i coef: int, var:int                            i*)
-	    action :: variable_stated_in_trace l
-	| SPLIT_INEQ (_,(_,act1),(_,act2)) ->
-	    variable_stated_in_trace act1 @ variable_stated_in_trace act2
-	| _ -> variable_stated_in_trace l
-      end
-  | [] -> []
-;;
-
-let add_stated_equations env tree =
-  (* Il faut trier les variables par ordre d'introduction pour ne pas risquer
-     de définir dans le mauvais ordre *)
-  let stated_equations =
-    let cmpvar x y = Pervasives.(-) x.st_var y.st_var in
-    let rec loop = function
-      | Tree(_,t1,t2) -> List.merge cmpvar (loop t1) (loop t2)
-      | Leaf s -> List.sort cmpvar (variable_stated_in_trace s.s_trace)
-    in 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.st_def in
-    (* Notez que si l'ordre de création des variables n'est pas respecté,
-     * ca va planter *)
+     match act with
+     | HYP e -> IntSet.add e.id (hyps_used_in_trace l)
+     | SPLIT_INEQ (_,(_,act1),(_,act2)) ->
+        hyps_used_in_trace act1 @@ hyps_used_in_trace act2
+     | _ -> hyps_used_in_trace l
+
+(** Retreive variables declared as extra equations during resolution
+    and declare them into the environment.
+    We should consider these variables in their introduction order,
+    otherwise really bad things will happen. *)
+
+let state_cmp x y = Int.compare x.st_var y.st_var
+
+module StateSet =
+  Set.Make (struct type t = state_action let compare = state_cmp end)
+
+let rec stated_in_trace = function
+  | [] -> StateSet.empty
+  | [SPLIT_INEQ (_,(_,t1),(_,t2))] ->
+     StateSet.union (stated_in_trace t1) (stated_in_trace t2)
+  | STATE action :: l -> StateSet.add action (stated_in_trace l)
+  | _ :: l -> stated_in_trace l
+
+let rec stated_in_tree = function
+  | Tree(_,t1,t2) -> StateSet.union (stated_in_tree t1) (stated_in_tree t2)
+  | Leaf s -> stated_in_trace s.s_trace
+
+let digest_stated_equations env tree =
+  let do_equation st (vars,gens,eqns,ids) =
+    (** We turn the definition of [v]
+        - into a reified formula : *)
+    let v_def = oformula_of_omega st.st_def in
+    (** - into a concrete Coq formula
+          (this uses only older vars already in env) : *)
     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 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;
-    (v, term_to_generalize,term_to_reify,st.st_def.id) in
- List.map add_env stated_equations
+    (** We then update the environment *)
+    set_reified_atom st.st_var coq_v env;
+    (** The term we'll introduce *)
+    let term_to_generalize =
+      EConstr.of_constr (app coq_refl_equal [|Lazy.force Z.typ; coq_v|])
+    in
+    (** Its representation as equation (but not reified yet,
+        we lack the proper env to do that). *)
+    let term_to_reify = (v_def,Oatom st.st_var) in
+    (st.st_var::vars,
+     term_to_generalize::gens,
+     term_to_reify::eqns,
+     CCEqua st.st_def.id :: ids)
+  in
+  let (vars,gens,eqns,ids) =
+    StateSet.fold do_equation (stated_in_tree tree) ([],[],[],[])
+  in
+  (List.rev vars, List.rev gens, List.rev eqns, List.rev ids)
 
 (* Calcule la liste des éclatements à réaliser sur les hypothèses
    nécessaires pour extraire une liste d'équations donnée *)
@@ -921,22 +710,22 @@ let add_stated_equations env tree =
    arg, then second arg), unless you know what you're doing. *)
 
 let rec get_eclatement env = function
-    i :: r ->
-      let l = try (get_equation env i).e_depends with Not_found -> [] in
-      List.union Pervasives.(=) (List.rev l) (get_eclatement env r)
   | [] -> []
+  | i :: r ->
+     let l = try (get_equation env i).e_depends with Not_found -> [] in
+     List.union dir_eq (List.rev l) (get_eclatement env r)
 
 let select_smaller l =
-  let comp (_,x) (_,y) = Pervasives.(-) (List.length x) (List.length y) in
+  let comp (_,x) (_,y) = Int.compare (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
     | [] -> []
+    | (x::l) ->
+       if List.mem_f dir_eq x required then select l
+       else if List.mem_f dir_eq (barre x) required then raise Exit
+       else x :: select l
   in
   List.map_filter
     (function (sol, splits) ->
@@ -944,54 +733,51 @@ let filter_compatible_systems required systems =
     systems
 
 let rec equas_of_solution_tree = function
-    Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)
+  | Tree(_,t1,t2) ->
+     (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)
   | Leaf s -> s.s_equa_deps
 
-(* [really_useful_prop] pushes useless props in a new Pprop variable *)
-(* Things get shorter, but may also get wrong, since a Prop is considered
-   to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance
-   Pfalse is decidable. So should not be used on conclusion (??) *)
-
-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.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
+(** [maximize_prop] pushes useless props in a new Pprop atom.
+  The reified formulas get shorter, but be careful with decidabilities.
+  For instance, anything that contains a Pprop is considered to be
+  undecidable in [ReflOmegaCore], whereas a Pfalse for instance at
+  the same spot will lead to a decidable formula.
+  In particular, do not use this function on the conclusion.
+  Even in hypotheses, we could probably build pathological examples
+  that romega won't handle correctly, but they should be pretty rare.
+*)
+
+let maximize_prop equas c =
+  let rec loop c = match c with
+    | Pequa(t,e) -> if IntSet.mem e.e_omega.id equas then c else Pprop t
+    | Pnot t ->
+       (match loop t with
+        | Pprop p -> Pprop (app coq_not [|p|])
+        | t' -> Pnot t')
+    | Por(i,t1,t2) ->
+       (match loop t1, loop t2 with
+        | Pprop p1, Pprop p2 -> Pprop (app coq_or [|p1;p2|])
+        | t1', t2' -> Por(i,t1',t2'))
+    | Pand(i,t1,t2) ->
+       (match loop t1, loop t2 with
+        | Pprop p1, Pprop p2 -> Pprop (app coq_and [|p1;p2|])
+        | t1', t2' -> Pand(i,t1',t2'))
+    | Pimp(i,t1,t2) ->
+       (match loop t1, loop t2 with
+        | Pprop p1, Pprop p2 -> Pprop (Term.mkArrow p1 p2) (* no lift (closed) *)
+        | t1', t2' -> Pimp(i,t1',t2'))
+    | Ptrue -> Pprop (app coq_True [||])
+    | Pfalse -> Pprop (app coq_False [||])
+    | Pprop _ -> c
+  in loop c
 
 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)))
+         t.s_index
+         (String.concat " " (List.map string_of_int
+                                      (IntSet.elements t.s_equa_deps))))
   | Tree(i,t1,t2) ->
       Printf.fprintf ch "S%d(%a,%a)" i
 	display_solution_tree t1 display_solution_tree t2
@@ -1023,7 +809,7 @@ let find_path {o_hyp=id;o_path=p} env =
     | (x1::l1,x2::l2) when occ_step_eq x1 x2 -> loop_path (l1,l2)
     | _ -> None in
   let rec loop_id i = function
-      CCHyp{o_hyp=id';o_path=p'} :: l when Names.Id.equal id id' ->
+      CCHyp{o_hyp=id';o_path=p'} :: l when Id.equal id id' ->
 	begin match loop_path (p',p) with
 	  Some r -> i,r
 	| None -> loop_id (succ i) l
@@ -1034,110 +820,78 @@ let find_path {o_hyp=id;o_path=p} 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)
+    | O_left -> Some (Lazy.force coq_d_left)
+    | O_right -> Some (Lazy.force coq_d_right)
+    | O_mono -> None (* No more [D_mono] constructor now *)
+  in
+  mk_list (Lazy.force coq_direction) (List.map_filter trans l)
 
 
 (* \section{Rejouer l'historique} *)
 
-let get_hyp env_hyp i =
-  try List.index0 Pervasives.(=) (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
-      | CONTRADICTION (e1,e2) :: l ->
-	  let trace = mk_nat (List.length e1.body) in
-	  mkApp (Lazy.force coq_s_contradiction,
-		 [| trace ; mk_nat (get_hyp env_hyp e1.id);
-		    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;
-		    mk_nat (List.length e2.body);
-		    loop env_hyp l; mk_nat (get_hyp env_hyp e1.id) |])
-      | NOT_EXACT_DIVIDE (e1,k) :: l ->
-	  let e2_constant = floor_div e1.constant k in
-	  let d = e1.constant - e2_constant * k in
-	  let e2_body = map_eq_linear (fun c -> c / k) e1.body in
-          mkApp (Lazy.force coq_s_not_exact_divide,
-		 [|Z.mk k; Z.mk d;
-		   reified_of_omega env e2_body e2_constant;
-		   mk_nat (List.length e2_body);
-		   mk_nat (get_hyp env_hyp e1.id)|])
-      | 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;
-		   mk_nat (List.length e2_body);
-		   loop env_hyp l; mk_nat (get_hyp env_hyp e1.id)|])
-      | (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 (List.length e1.body);
-		    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) |])
-      | CONSTANT_NOT_NUL(e,k) :: l ->
-          mkApp (Lazy.force coq_s_constant_not_nul,
-		 [|  mk_nat (get_hyp env_hyp e) |])
-      | CONSTANT_NEG(e,k) :: l ->
-          mkApp (Lazy.force coq_s_constant_neg,
-		 [|  mk_nat (get_hyp env_hyp e) |])
-      | STATE {st_new_eq=new_eq; st_def =def;
-		      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 |])
-      |	HYP _ :: l -> loop env_hyp l
-      |	CONSTANT_NUL e :: l ->
-	  mkApp (Lazy.force coq_s_constant_nul,
-		 [|  mk_nat (get_hyp env_hyp e) |])
-      |	NEGATE_CONTRADICT(e1,e2,true) :: l ->
-	  mkApp (Lazy.force coq_s_negate_contradict,
-		 [|  mk_nat (get_hyp env_hyp e1.id);
-		     mk_nat (get_hyp env_hyp e2.id) |])
-      |	NEGATE_CONTRADICT(e1,e2,false) :: l ->
-	  mkApp (Lazy.force coq_s_negate_contradict_inv,
-		 [|  mk_nat (List.length e2.body);
-		     mk_nat (get_hyp env_hyp e1.id);
-		     mk_nat (get_hyp env_hyp e2.id) |])
-      | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
-	  let i =  get_hyp env_hyp e.id in
-	  let r1 = loop (CCEqua e1 :: env_hyp) l1 in
-	  let r2 = loop (CCEqua e2 :: env_hyp) l2 in
-	  mkApp (Lazy.force coq_s_split_ineq,
-                  [| mk_nat (List.length e.body); mk_nat i; r1 ; r2 |])
-      |	(FORGET_C _ | FORGET _ | FORGET_I _) :: l ->
-	  loop env_hyp l
-      | (WEAKEN  _ ) :: l -> failwith "not_treated"
-      |	[] -> failwith "no contradiction"
-  in loop env_hyp
+let hyp_idx env_hyp i =
+  let rec loop count = function
+    | [] -> failwith (Printf.sprintf "get_hyp %d" i)
+    | CCEqua i' :: _ when Int.equal i i' -> mk_nat count
+    | _ :: l -> loop (succ count) l
+  in loop 0 env_hyp
+
+
+(* We now expand NEGATE_CONTRADICT and CONTRADICTION into
+   a O_SUM followed by a O_BAD_CONSTANT *)
+
+let sum_bad inv i1 i2 =
+  mkApp (Lazy.force coq_s_sum,
+         [| Z.mk Bigint.one; i1;
+            Z.mk (if inv then negone else Bigint.one); i2;
+            mkApp (Lazy.force coq_s_bad_constant, [| mk_nat 0 |])|])
+
+let rec reify_trace env env_hyp = function
+  | CONSTANT_NOT_NUL(e,_) :: []
+  | CONSTANT_NEG(e,_) :: []
+  | CONSTANT_NUL e :: [] ->
+     mkApp (Lazy.force coq_s_bad_constant,[| hyp_idx env_hyp e |])
+  | NEGATE_CONTRADICT(e1,e2,direct) :: [] ->
+     sum_bad direct (hyp_idx env_hyp e1.id) (hyp_idx env_hyp e2.id)
+  | CONTRADICTION (e1,e2) :: [] ->
+     sum_bad false (hyp_idx env_hyp e1.id) (hyp_idx env_hyp e2.id)
+  | NOT_EXACT_DIVIDE (e1,k) :: [] ->
+     mkApp (Lazy.force coq_s_not_exact_divide,
+            [| hyp_idx env_hyp e1.id; Z.mk k |])
+  | DIVIDE_AND_APPROX (e1,_,k,_) :: l
+  | EXACT_DIVIDE (e1,k) :: l ->
+     mkApp (Lazy.force coq_s_divide,
+            [| hyp_idx env_hyp e1.id; Z.mk k;
+               reify_trace env env_hyp l |])
+  | MERGE_EQ(e3,e1,e2) :: l ->
+     mkApp (Lazy.force coq_s_merge_eq,
+            [| hyp_idx env_hyp e1.id; hyp_idx env_hyp e2;
+               reify_trace env (CCEqua e3:: env_hyp) l |])
+  | SUM(e3,(k1,e1),(k2,e2)) :: l ->
+     mkApp (Lazy.force coq_s_sum,
+            [| Z.mk k1; hyp_idx env_hyp e1.id;
+               Z.mk k2; hyp_idx env_hyp e2.id;
+               reify_trace env (CCEqua e3 :: env_hyp) l |])
+  | STATE {st_new_eq; st_def; st_orig; st_coef } :: l ->
+     (* we now produce a [O_SUM] here *)
+     mkApp (Lazy.force coq_s_sum,
+            [| Z.mk Bigint.one; hyp_idx env_hyp st_orig.id;
+               Z.mk st_coef; hyp_idx env_hyp st_def.id;
+               reify_trace env (CCEqua st_new_eq.id :: env_hyp) l |])
+  | HYP _ :: l -> reify_trace env env_hyp l
+  | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: _ ->
+     let r1 = reify_trace env (CCEqua e1 :: env_hyp) l1 in
+     let r2 = reify_trace env (CCEqua e2 :: env_hyp) l2 in
+     mkApp (Lazy.force coq_s_split_ineq,
+            [| hyp_idx env_hyp e.id; r1 ; r2 |])
+  | (FORGET_C _ | FORGET _ | FORGET_I _) :: l -> reify_trace env env_hyp l
+  | WEAKEN  _ :: l -> failwith "not_treated"
+  | _ -> failwith "bad history"
 
 let rec decompose_tree env ctxt = function
    Tree(i,left,right) ->
      let org =
-       try Hashtbl.find env.constructors i
+       try IntHtbl.find env.constructors i
        with Not_found ->
 	 failwith (Printf.sprintf "Cannot find constructor %d" i) in
      let (index,path) = find_path org ctxt in
@@ -1149,22 +903,41 @@ let rec decompose_tree env ctxt = function
 	  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
+      decompose_tree_hyps s.s_trace env ctxt (IntSet.elements s.s_equa_deps)
 and decompose_tree_hyps trace env ctxt = function
-    [] -> app coq_e_solve [| replay_history env ctxt trace |]
+    [] -> app coq_e_solve [| reify_trace env ctxt trace |]
   | (i::l) ->
       let equation =
-        try Hashtbl.find env.equations i
+        try IntHtbl.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.id :: ctxt) l in
-      app coq_e_extract [|mk_nat index;
-			  mk_direction_list full_path;
-			  cont |]
+      app coq_e_extract [|mk_nat index; mk_direction_list path; cont |]
+
+let solve_system env index list_eq =
+  let system = List.map (fun eq -> eq.e_omega) list_eq in
+  let trace =
+    OmegaSolver.simplify_strong
+      (new_omega_eq,new_omega_var,display_omega_var)
+      system
+  in
+  (* Hypotheses used for this solution *)
+  let vars = hyps_used_in_trace trace in
+  let splits = get_eclatement env (IntSet.elements vars) in
+  if !debug then
+    begin
+      Printf.printf "SYSTEME %d\n" index;
+      display_action display_omega_var trace;
+      print_string "\n  Depend :";
+      IntSet.iter (fun i -> Printf.printf " %d" i) vars;
+      print_string "\n  Split points :";
+      List.iter display_depend splits;
+      Printf.printf "\n------------------------------------\n"
+    end;
+  {s_index = index; s_trace = trace; s_equa_deps = vars}, splits
 
 (* \section{La fonction principale} *)
  (* Cette fonction construit la
@@ -1174,143 +947,100 @@ 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 =
-      simplify_strong
-	(new_omega_eq,new_omega_var,display_omega_var)
-	system in
-    (* calcule les hypotheses utilisées pour la solution *)
-    let vars = hyps_used_in_trace trace in
-    let splits = get_eclatement env vars in
-    if !debug then begin
-      Printf.printf "SYSTEME %d\n" index;
-      display_action display_omega_var 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
+let resolution unsafe env (reified_concl,reified_hyps) systems_list =
   if !debug then Printf.printf "\n====================================\n";
-  let all_solutions = List.map solve_system systems_list in
+  let all_solutions = List.mapi (solve_system env) 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 = 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.uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in
-  let l_hyps = id_concl :: List.remove Names.Id.equal id_concl l_hyps' in
-  let useful_hyps =
-    List.map
-      (fun id -> List.assoc_f Names.Id.equal id full_reified_goal) l_hyps
+  (** Collect all hypotheses used in the solution tree *)
+  let useful_equa_ids = equas_of_solution_tree solution_tree in
+  let equations = List.map (get_equation env) (IntSet.elements useful_equa_ids)
   in
-  let useful_vars =
-    let really_useful_vars = vars_of_equations equations in
-    let concl_vars =
-      vars_of_prop (List.assoc_f Names.Id.equal id_concl full_reified_goal)
-    in
-    really_useful_vars @@ concl_vars
+  let hyps_of_eqns =
+    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 useful_hyptypes =
+    List.map (fun id -> List.assoc_f Id.equal id reified_hyps) useful_hypnames
+  in
+  let useful_vars = vars_of_equations equations @@ vars_of_prop reified_concl
+  in
+
+  (** Parts coming from equations introduced by omega: *)
+  let stated_vars, l_generalize_arg, to_reify_stated, hyp_stated_vars =
+    digest_stated_equations env solution_tree
   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,_,_) -> EConstr.of_constr 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 (et de la conclusion)
-     - les nouvelles variables declarées durant les preuves *)
-  let all_vars_env = useful_vars @ stated_vars in
-  let basic_env =
+  (** The final variables are either coming from:
+     - useful hypotheses (and conclusion)
+     - equations introduced during resolution *)
+  let all_vars_env = (IntSet.elements useful_vars) @ stated_vars
+  in
+  (** We prepare the renumbering from all variables to useful ones.
+      Since [all_var_env] is sorted, this renumbering will preserve
+      order: this way, the equations in ReflOmegaCore will have
+      the same normal forms as here. *)
+  let reduced_term_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 (succ i) l
-      |	[] -> [] in
-    loop 0 all_vars_env in
-  let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in
-  (* On peut maintenant généraliser le but : env est a jour *)
-  let l_reified_stated =
-     List.map (fun (_,_,(l,r),_) ->
-                 app coq_p_eq [| reified_of_formula env l;
-                                 reified_of_formula env r |])
-              to_introduce in
-  let reified_concl =
-    match useful_hyps with
-      (Pnot p) :: _ -> reified_of_proposition env p
-    | _ ->  reified_of_proposition env Pfalse in
+      | [] -> []
+      | var :: l ->
+         let t = get_reified_atom env var in
+         IntHtbl.add env.real_indices var i; t :: loop (succ i) l
+    in
+    mk_list (Lazy.force Z.typ) (loop 0 all_vars_env)
+  in
+  (** The environment [env] (and especially [env.real_indices]) is now
+      ready for the coming reifications: *)
+  let l_reified_stated = List.map (reified_of_eq env) to_reify_stated in
+  let reified_concl = reified_of_proposition env reified_concl 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
+    List.map
+      (fun p -> reified_of_proposition env (maximize_prop useful_equa_ids p))
+      useful_hyptypes
+  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 =
     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 Names.Id.equal e.e_origin.o_hyp l_hyps 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;reduced_term_env;reified_goal|]
+  in
   let initial_context =
-    List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) (List.tl l_hyps) in
+    List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) useful_hypnames 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 EConstr.mkVar (List.tl l_hyps)) >>
-  Tactics.change_concl reified >>
-  Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
+    (l_generalize_arg @ List.map EConstr.mkVar useful_hypnames) >>
+  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:
-   - Normalisation without VM:
-      Tactics.normalise_in_concl
-   - Skip the conversion check and rely directly on the QED:
-      Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >>
-  i*)
+  (if unsafe then
+     (* Trust the produced term. Faster, but might fail later at Qed.
+        Also handy when debugging, e.g. via a Show Proof after romega. *)
+     Tactics.convert_concl_no_check
+       (EConstr.of_constr (Lazy.force coq_True)) Term.VMcast
+   else
+     Tactics.normalise_vm_in_concl) >>
   Tactics.apply (EConstr.of_constr (Lazy.force coq_I))
 
-let total_reflexive_omega_tactic =
+let total_reflexive_omega_tactic unsafe =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
   rst_omega_eq ();
   rst_omega_var ();
   try
   let env = new_environment () in
-  let full_reified_goal = reify_gl env gl in
+  let (concl,hyps) as reified_goal = reify_gl env gl in
+  (* Register all atom indexes created during reification as omega vars *)
+  set_omega_maxvar (pred (List.length env.terms));
+  let full_reified_goal = (id_concl,Pnot concl) :: hyps in
   let systems_list = destructurate_hyps full_reified_goal in
   if !debug then display_systems systems_list;
-  resolution env full_reified_goal systems_list
+  resolution unsafe env reified_goal systems_list
   with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system"
   end }
-
-(*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
-
-
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
index 1348bb623..42730f2e1 100644
--- a/test-suite/success/ROmega0.v
+++ b/test-suite/success/ROmega0.v
@@ -135,11 +135,13 @@ Qed.
 (* Magaud #240 *)
 
 Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+Proof.
 intros.
 romega.
 Qed.
 
 Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+Proof.
 intros x y.
 romega.
 Qed.
@@ -147,6 +149,20 @@ Qed.
 (* Besson #1298 *)
 
 Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False.
+Proof.
 intros.
 romega.
 Qed.
+
+(* Letouzey, May 2017 *)
+
+Lemma test_romega10 : forall x a a' b b',
+ a' <= b ->
+ a <= b' ->
+ b < b' ->
+ a < a' ->
+ a <= x < b' <-> a <= x < b \/ a' <= x < b'.
+Proof.
+ intros.
+ romega.
+Qed.