Imported Upstream version 8.8.2upstream/8.8.2

7 files changed, 1791 insertions, 3424 deletions

diff --git a/plugins/romega/ROmega.v b/plugins/romega/ROmega.v
index 3ddb6bed..657aae90 100644
--- a/plugins/romega/ROmega.v
+++ b/plugins/romega/ROmega.v
@@ -11,4 +11,4 @@ Require Export Setoid.
 Require Export PreOmega.
 Require Export ZArith_base.
 Require Import OmegaPlugin.
-Declare ML Module "romega_plugin".
\ No newline at end of file
+Declare ML Module "romega_plugin".
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 187601fc..51b99b99 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -10,18 +10,20 @@
 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.
 
-  Parameter zero : t.
-  Parameter one : t.
-  Parameter plus : t -> t -> t.
-  Parameter opp : t -> t.
-  Parameter minus : t -> t -> t.
-  Parameter mult : t -> t -> t.
+  Bind Scope Int_scope with t.
+
+  Parameter Inline zero : t.
+  Parameter Inline one : t.
+  Parameter Inline plus : t -> t -> t.
+  Parameter Inline opp : t -> t.
+  Parameter Inline minus : t -> t -> t.
+  Parameter Inline mult : t -> t -> t.
 
   Notation "0" := zero : Int_scope.
   Notation "1" := one : Int_scope.
@@ -32,15 +34,15 @@ 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.
-  Parameter ge : t -> t -> Prop.
-  Parameter gt : t -> t -> Prop.
+  Parameter Inline le : t -> t -> Prop.
+  Parameter Inline lt : t -> t -> Prop.
+  Parameter Inline ge : t -> t -> Prop.
+  Parameter Inline gt : t -> t -> Prop.
   Notation "x <= y" := (le x y): Int_scope.
   Notation "x < y" := (lt x y) : Int_scope.
   Notation "x >= y" := (ge x y) : Int_scope.
@@ -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 4935fe4b..ad3afafd 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -6,14 +6,16 @@
 
  *************************************************************************)
 
+open Names
+
 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 * EConstr.t list
+  | Kimp of EConstr.t * EConstr.t
+  | Kufo
 
 let meaningful_submodule = [ "Z"; "N"; "Pos" ]
 
@@ -27,32 +29,32 @@ let string_of_global r =
   in
   prefix^(Names.Id.to_string (Nametab.basename_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
-
-let dest_const_apply t =
-  let f,args = Term.decompose_app t in
+let destructurate sigma t =
+  let c, args = EConstr.decompose_app sigma t in
+  let open Constr in
+  match EConstr.kind sigma c, args with
+  | Const (sp,_), args ->
+     Kapp (string_of_global (Globnames.ConstRef sp), args)
+  | Construct (csp,_) , args ->
+     Kapp (string_of_global (Globnames.ConstructRef csp), args)
+  | Ind (isp,_), args ->
+     Kapp (string_of_global (Globnames.IndRef isp), args)
+  | Var id, [] -> Kvar(Names.Id.to_string id)
+  | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
+  | _ -> Kufo
+
+exception DestConstApp
+
+let dest_const_apply sigma t =
+  let open Constr in
+  let f,args = EConstr.decompose_app sigma t in
   let ref =
-  match Term.kind_of_term f with
-    | 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
+  match EConstr.kind sigma f with
+    | Const (sp,_)      -> Globnames.ConstRef sp
+    | Construct (csp,_) -> Globnames.ConstructRef csp
+    | Ind (isp,_)       -> Globnames.IndRef isp
+    | _ -> raise DestConstApp
+  in Nametab.basename_of_global ref, args
 
 let logic_dir = ["Coq";"Logic";"Decidable"]
 
@@ -65,13 +67,25 @@ let coq_modules =
 let bin_module = [["Coq";"Numbers";"BinNums"]]
 let z_module = [["Coq";"ZArith";"BinInt"]]
 
-let init_constant = Coqlib.gen_constant_in_modules "Omega" Coqlib.init_modules
-let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules
-let z_constant = Coqlib.gen_constant_in_modules "Omega" z_module
-let bin_constant = Coqlib.gen_constant_in_modules "Omega" bin_module
+let init_constant x =
+  EConstr.of_constr @@
+  Universes.constr_of_global @@
+  Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x
+let constant x =
+  EConstr.of_constr @@
+  Universes.constr_of_global @@
+  Coqlib.gen_reference_in_modules "Omega" coq_modules x
+let z_constant x =
+  EConstr.of_constr @@
+  Universes.constr_of_global @@
+  Coqlib.gen_reference_in_modules "Omega" z_module x
+let bin_constant x =
+  EConstr.of_constr @@
+  Universes.constr_of_global @@
+  Coqlib.gen_reference_in_modules "Omega" bin_module x
 
 (* Logic *)
-let coq_refl_equal = lazy(init_constant  "eq_refl")
+let coq_refl_equal = lazy(init_constant "eq_refl")
 let coq_and = lazy(init_constant "and")
 let coq_not = lazy(init_constant "not")
 let coq_or = lazy(init_constant "or")
@@ -81,13 +95,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 +117,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 +136,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")
@@ -206,168 +143,190 @@ let coq_O = lazy(init_constant "O")
 
 let rec mk_nat = function
   | 0 -> Lazy.force coq_O
-  | n -> Term.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |])
+  | n -> EConstr.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |])
 
 (* Lists *)
 
-let mkListConst c = 
-  let r = 
-    Coqlib.gen_reference "" ["Init";"Datatypes"] c
-  in 
-  let inst = 
-    if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|]
-    else fun _ -> Univ.Instance.empty
+let mkListConst c =
+  let r =
+    Coqlib.coq_reference "" ["Init";"Datatypes"] c
+  in
+  let inst =
+    if Global.is_polymorphic r then
+      fun u -> EConstr.EInstance.make (Univ.Instance.of_array [|u|])
+    else
+      fun _ -> EConstr.EInstance.empty
   in
-    fun u -> Term.mkConstructU (Globnames.destConstructRef r, inst u)
+    fun u -> EConstr.mkConstructU (Globnames.destConstructRef r, inst u)
 
-let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|])
-let coq_nil univ typ =  Term.mkApp (mkListConst "nil" univ, [|typ|])
+let coq_cons univ typ = EConstr.mkApp (mkListConst "cons" univ, [|typ|])
+let coq_nil univ typ =  EConstr.mkApp (mkListConst "nil" univ, [|typ|])
 
 let mk_list univ typ l =
   let rec loop = function
     | [] -> coq_nil univ typ
     | (step :: l) ->
-	Term.mkApp (coq_cons univ typ, [| step; loop l |]) in
+       EConstr.mkApp (coq_cons univ typ, [| step; loop l |]) in
   loop l
 
-let mk_plist = 
-  let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in
-    fun l -> mk_list type1lev Term.mkProp l
+let mk_plist =
+  let type1lev = Universes.new_univ_level () in
+  fun l -> mk_list type1lev EConstr.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
-  | Tmult of Term.constr * Term.constr
-  | Tminus of Term.constr * Term.constr
-  | Topp of Term.constr
-  | Tsucc of Term.constr
+  | Tplus of EConstr.t * EConstr.t
+  | Tmult of EConstr.t * EConstr.t
+  | Tminus of EConstr.t * EConstr.t
+  | Topp of EConstr.t
+  | Tsucc of EConstr.t
   | Tnum of Bigint.bigint
   | Tother
 
 type parse_rel =
-  | Req of Term.constr * Term.constr
-  | Rne of Term.constr * Term.constr
-  | Rlt of Term.constr * Term.constr
-  | Rle of Term.constr * Term.constr
-  | Rgt of Term.constr * Term.constr
-  | Rge of Term.constr * Term.constr
+  | Req of EConstr.t * EConstr.t
+  | Rne of EConstr.t * EConstr.t
+  | Rlt of EConstr.t * EConstr.t
+  | Rle of EConstr.t * EConstr.t
+  | Rgt of EConstr.t * EConstr.t
+  | Rge of EConstr.t * EConstr.t
   | Rtrue
   | Rfalse
-  | Rnot of Term.constr
-  | Ror of Term.constr * Term.constr
-  | Rand of Term.constr * Term.constr
-  | Rimp of Term.constr * Term.constr
-  | Riff of Term.constr * Term.constr
+  | Rnot of EConstr.t
+  | Ror of EConstr.t * EConstr.t
+  | Rand of EConstr.t * EConstr.t
+  | Rimp of EConstr.t * EConstr.t
+  | Riff of EConstr.t * EConstr.t
   | 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 sigma c = match destructurate sigma 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_Z = lazy (bin_constant "Z")
+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
+    EConstr.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 -> EConstr.mkApp (Lazy.force coq_Npos,
+                     [| mk_positive (Bigint.of_int n) |])
 
 module type Int = sig
-  val typ : Term.constr Lazy.t
-  val plus : Term.constr Lazy.t
-  val mult : Term.constr Lazy.t
-  val opp : Term.constr Lazy.t
-  val minus : Term.constr Lazy.t
-
-  val mk : Bigint.bigint -> Term.constr
-  val parse_term : Term.constr -> parse_term
-  val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
+  val typ : EConstr.t Lazy.t
+  val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool
+  val plus : EConstr.t Lazy.t
+  val mult : EConstr.t Lazy.t
+  val opp : EConstr.t Lazy.t
+  val minus : EConstr.t Lazy.t
+
+  val mk : Bigint.bigint -> EConstr.t
+  val parse_term : Evd.evar_map -> EConstr.t -> parse_term
+  val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel
   (* check whether t is built only with numbers and + * - *)
-  val is_scalar : Term.constr -> bool
+  val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option
 end
 
 module Z : Int = struct
 
-let typ = lazy (bin_constant "Z")
+let typ = coq_Z
 let plus = lazy (z_constant "Z.add")
 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 sigma 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";;
-
-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 f,l = dest_const_apply sigma t in
+    match 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
+    | _ -> raise DestConstApp
+  in
+  try Some (loop t) with DestConstApp -> None
+
+let recognize_Z sigma t =
+  try
+    let f,l = dest_const_apply sigma t in
+    match Id.to_string f,l with
+    | "Zpos",[t] -> recognize_pos sigma t
+    | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos sigma 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 |])
+    EConstr.mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
   else
-    Term.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |])
+    EConstr.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg 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 parse_term sigma t =
+  match destructurate sigma 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 sigma t with Some t -> Tnum t | None -> Tother)
+  | _ -> Tother
+
+let is_int_typ gl t =
+  Tacmach.New.pf_apply Reductionops.is_conv gl t (Lazy.force coq_Z)
 
 let parse_rel gl t =
-  try match destructurate t with
-    | Kapp("eq",[typ;t1;t2])
-      when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2)
-    | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
-    | Kapp("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
+  let sigma = Proofview.Goal.sigma gl in
+  match destructurate sigma t with
+  | Kapp("eq",[typ;t1;t2]) when is_int_typ gl typ -> 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 sigma t
+
+let rec get_scalar sigma t =
+  match destructurate sigma t with
+  | Kapp("Z.add", [t1;t2]) ->
+     Option.lift2 Bigint.add (get_scalar sigma t1) (get_scalar sigma t2)
+  | Kapp ("Z.sub",[t1;t2]) ->
+     Option.lift2 Bigint.sub (get_scalar sigma t1) (get_scalar sigma t2)
+  | Kapp ("Z.mul",[t1;t2]) ->
+     Option.lift2 Bigint.mult (get_scalar sigma t1) (get_scalar sigma t2)
+  | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar sigma t)
+  | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar sigma t)
+  | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar sigma t)
+  | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z sigma t
+  | _ -> None
 
 end
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index af50ea0f..64668df0 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -10,167 +10,114 @@
 (** Coq objects used in romega *)
 
 (* from Logic *)
-val coq_refl_equal : Term.constr lazy_t
-val coq_and : Term.constr lazy_t
-val coq_not : Term.constr lazy_t
-val coq_or : Term.constr lazy_t
-val coq_True : Term.constr lazy_t
-val coq_False : Term.constr lazy_t
-val coq_I : Term.constr lazy_t
+val coq_refl_equal : EConstr.t lazy_t
+val coq_and : EConstr.t lazy_t
+val coq_not : EConstr.t lazy_t
+val coq_or : EConstr.t lazy_t
+val coq_True : EConstr.t lazy_t
+val coq_False : EConstr.t lazy_t
+val coq_I : EConstr.t 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
-val coq_t_mult : Term.constr lazy_t
-val coq_t_opp : Term.constr lazy_t
-val coq_t_minus : Term.constr lazy_t
-val coq_t_var : Term.constr lazy_t
-
-val coq_proposition : Term.constr lazy_t
-val coq_p_eq : Term.constr lazy_t
-val coq_p_leq : Term.constr lazy_t
-val coq_p_geq : Term.constr lazy_t
-val coq_p_lt : Term.constr lazy_t
-val coq_p_gt : Term.constr lazy_t
-val coq_p_neq : Term.constr lazy_t
-val coq_p_true : Term.constr lazy_t
-val coq_p_false : Term.constr lazy_t
-val coq_p_not : Term.constr lazy_t
-val coq_p_or : Term.constr lazy_t
-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_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
-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 coq_t_int : EConstr.t lazy_t
+val coq_t_plus : EConstr.t lazy_t
+val coq_t_mult : EConstr.t lazy_t
+val coq_t_opp : EConstr.t lazy_t
+val coq_t_minus : EConstr.t lazy_t
+val coq_t_var : EConstr.t lazy_t
+
+val coq_proposition : EConstr.t lazy_t
+val coq_p_eq : EConstr.t lazy_t
+val coq_p_leq : EConstr.t lazy_t
+val coq_p_geq : EConstr.t lazy_t
+val coq_p_lt : EConstr.t lazy_t
+val coq_p_gt : EConstr.t lazy_t
+val coq_p_neq : EConstr.t lazy_t
+val coq_p_true : EConstr.t lazy_t
+val coq_p_false : EConstr.t lazy_t
+val coq_p_not : EConstr.t lazy_t
+val coq_p_or : EConstr.t lazy_t
+val coq_p_and : EConstr.t lazy_t
+val coq_p_imp : EConstr.t lazy_t
+val coq_p_prop : EConstr.t lazy_t
+
+val coq_s_bad_constant : EConstr.t lazy_t
+val coq_s_divide : EConstr.t lazy_t
+val coq_s_not_exact_divide : EConstr.t lazy_t
+val coq_s_sum : EConstr.t lazy_t
+val coq_s_merge_eq : EConstr.t lazy_t
+val coq_s_split_ineq : EConstr.t lazy_t
+
+val coq_direction : EConstr.t lazy_t
+val coq_d_left : EConstr.t lazy_t
+val coq_d_right : EConstr.t lazy_t
+
+val coq_e_split : EConstr.t lazy_t
+val coq_e_extract : EConstr.t lazy_t
+val coq_e_solve : EConstr.t lazy_t
+
+val coq_interp_sequent : EConstr.t lazy_t
+val coq_do_omega : EConstr.t lazy_t
+
+val mk_nat : int -> EConstr.t
+val mk_N : int -> EConstr.t
+
 (** 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
+val mk_list : EConstr.t -> EConstr.t list -> EConstr.t
+val mk_plist : EConstr.types list -> EConstr.types
 
 (** Analyzing a coq term *)
 
 (* The generic result shape of the analysis of a term.
    One-level depth, except when a number is found *)
 type parse_term =
-    Tplus of Term.constr * Term.constr
-  | Tmult of Term.constr * Term.constr
-  | Tminus of Term.constr * Term.constr
-  | Topp of Term.constr
-  | Tsucc of Term.constr
+    Tplus of EConstr.t * EConstr.t
+  | Tmult of EConstr.t * EConstr.t
+  | Tminus of EConstr.t * EConstr.t
+  | Topp of EConstr.t
+  | Tsucc of EConstr.t
   | Tnum of Bigint.bigint
   | Tother
 
 (* The generic result shape of the analysis of a relation.
    One-level depth. *)
 type parse_rel =
-    Req of Term.constr * Term.constr
-  | Rne of Term.constr * Term.constr
-  | Rlt of Term.constr * Term.constr
-  | Rle of Term.constr * Term.constr
-  | Rgt of Term.constr * Term.constr
-  | Rge of Term.constr * Term.constr
+    Req of EConstr.t * EConstr.t
+  | Rne of EConstr.t * EConstr.t
+  | Rlt of EConstr.t * EConstr.t
+  | Rle of EConstr.t * EConstr.t
+  | Rgt of EConstr.t * EConstr.t
+  | Rge of EConstr.t * EConstr.t
   | Rtrue
   | Rfalse
-  | Rnot of Term.constr
-  | Ror of Term.constr * Term.constr
-  | Rand of Term.constr * Term.constr
-  | Rimp of Term.constr * Term.constr
-  | Riff of Term.constr * Term.constr
+  | Rnot of EConstr.t
+  | Ror of EConstr.t * EConstr.t
+  | Rand of EConstr.t * EConstr.t
+  | Rimp of EConstr.t * EConstr.t
+  | Riff of EConstr.t * EConstr.t
   | Rother
 
 (* A module factorizing what we should now about the number representation *)
 module type Int =
   sig
     (* the coq type of the numbers *)
-    val typ : Term.constr Lazy.t
+    val typ : EConstr.t Lazy.t
+    (* Is a constr expands to the type of these numbers *)
+    val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool
     (* the operations on the numbers *)
-    val plus : Term.constr Lazy.t
-    val mult : Term.constr Lazy.t
-    val opp : Term.constr Lazy.t
-    val minus : Term.constr Lazy.t
+    val plus : EConstr.t Lazy.t
+    val mult : EConstr.t Lazy.t
+    val opp : EConstr.t Lazy.t
+    val minus : EConstr.t Lazy.t
     (* building a coq number *)
-    val mk : Bigint.bigint -> Term.constr
+    val mk : Bigint.bigint -> EConstr.t
     (* parsing a term (one level, except if a number is found) *)
-    val parse_term : Term.constr -> parse_term
+    val parse_term : Evd.evar_map -> EConstr.t -> parse_term
     (* parsing a relation expression, including = < <= >= > *)
-    val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
+    val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel
     (* Is a particular term only made of numbers and + * - ? *)
-    val is_scalar : Term.constr -> bool
+    val get_scalar : Evd.evar_map -> EConstr.t -> 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 830dc54d..5b77d08d 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -6,28 +6,28 @@
 
  *************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
 
 DECLARE PLUGIN "romega_plugin"
 
+open Ltac_plugin
 open Names
 open Refl_omega
-open Constrarg
+open Stdarg
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
-  let kn = KerName.make2 (MPfile dp) (Label.make name) in
+  let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in
   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"
        | "positive" -> eval_tactic "zify_positive"
        | "N" -> eval_tactic "zify_N"
        | "Z" -> eval_tactic "zify_op"
-       | s -> CErrors.error ("No ROmega knowledge base for type "^s))
+       | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s)))
     (Util.List.sort_uniquize String.compare l)
   in
   Tacticals.New.tclTHEN
@@ -37,15 +37,15 @@ let romega_tactic l =
           we'd better leave as little as possible in the conclusion,
           for an easier decidability argument. *)
        (Tactics.intros)
-       (Proofview.V82.tactic 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 ba882e39..d1824978 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -12,19 +12,20 @@ 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
 
-let show_goal gl =
-  if !debug then (); Tacticals.tclIDTAC gl
+let show_goal = Tacticals.New.tclIDTAC
 
 let pp i = print_int i; print_newline (); flush stdout
 
 (* More readable than the prefix notation *)
-let (>>) = Tacticals.tclTHEN
-
-let mkApp = Term.mkApp
+let (>>) = Tacticals.New.tclTHEN
 
 (* \section{Types}
   \subsection{How to walk in a term}
@@ -38,13 +39,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,42 +51,42 @@ 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 EConstr.t * oequation (* constr = copy of the Coq formula *)
   | Ptrue
   | Pfalse
   | Pnot of oproposition
   | Por of int * oproposition * oproposition
   | Pand of int * oproposition * oproposition
   | Pimp of int * oproposition * oproposition
-  | Pprop of Term.constr
+  | Pprop of EConstr.t
 
-(* 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}
@@ -101,27 +100,25 @@ and oequation = {
 
 type environment = {
   (* La liste des termes non reifies constituant l'environnement global *)
-  mutable terms : Term.constr list;
+  mutable terms : EConstr.t list;
   (* La meme chose pour les propositions *)
-  mutable props : Term.constr list;
-  (* Les variables introduites par omega *)
-  mutable om_vars : (oformula * int) list;
+  mutable props : EConstr.t 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 +136,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 *)
@@ -166,8 +182,9 @@ let print_env_reification env =
   let rec loop c i = function
       [] ->  str "  ===============================\n\n"
     | t :: l ->
+      let sigma, env = Pfedit.get_current_context () in
       let s = Printf.sprintf "(%c%02d)" c i in
-      spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++
+      spc () ++ str s ++ str " := " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++
       loop c (succ i) l
   in
   let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in
@@ -178,52 +195,30 @@ 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
    l'environnement initial contenant tout. Il faudra le réduire après
    calcul des variables utiles. *)
 
-let add_reified_atom t env =
-  try List.index0 Term.eq_constr t env.terms
+let add_reified_atom sigma t env =
+  try List.index0 (EConstr.eq_constr sigma) t env.terms
   with Not_found ->
     let i = List.length env.terms in
     env.terms <- env.terms @ [t]; i
@@ -231,10 +226,17 @@ 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 =
-  try List.index0 Term.eq_constr t env.props
+let add_prop sigma env t =
+  try List.index0 (EConstr.eq_constr sigma) t env.props
   with Not_found ->
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
@@ -246,12 +248,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 +264,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,41 +280,16 @@ 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)
+let app f v = EConstr.mkApp(Lazy.force f,v)
 
 (* \subsection{Oformula vers COQ reel} *)
 
@@ -324,7 +299,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 +309,60 @@ 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 sigma 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 |]
-  | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |]
-
-let reified_of_proposition env f =
-  try reified_of_proposition env f
+  | Pnot t -> app coq_p_not [| reified_of_oprop sigma env t |]
+  | Por (_,t1,t2) | Pand (_,t1,t2) | Pimp (_,t1,t2) ->
+     reified_conn t
+      [| reified_of_oprop sigma env t1; reified_of_oprop sigma env t2 |]
+  | Pprop t -> app coq_p_prop [| mk_nat (add_prop sigma env t) |]
+
+let reified_of_proposition sigma env f =
+  try reified_of_oprop sigma 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 +372,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,385 +395,226 @@ 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
+  | 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 }
+
 
-(* \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] *)
 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 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
-    | Topp t -> Oopp(oformula_of_constr env t)
-    | Tsucc t -> Oplus(oformula_of_constr env t, Oint one)
+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 sigma env t =
+  match Z.parse_term sigma t with
+    | Tplus (t1,t2) -> binop sigma env (fun x y -> Oplus(x,y)) t1 t2
+    | Tminus (t1,t2) -> binop sigma env (fun x y -> Ominus(x,y)) t1 t2
+    | Tmult (t1,t2) ->
+       (match Z.get_scalar sigma t1 with
+        | Some n -> Omult (Oint n,oformula_of_constr sigma env t2)
+        | None ->
+           match Z.get_scalar sigma t2 with
+           | Some n -> Omult (oformula_of_constr sigma env t1, Oint n)
+           | None -> Oatom (add_reified_atom sigma t env))
+    | Topp t -> Oopp(oformula_of_constr sigma env t)
+    | Tsucc t -> Oplus(oformula_of_constr sigma env t, Oint one)
     | Tnum n -> Oint n
-    | _ -> Oatom (add_reified_atom t env)
+    | Tother -> Oatom (add_reified_atom sigma t env)
 
-and binop env c t1 t2 =
-  let t1' = oformula_of_constr env t1 in
-  let t2' = oformula_of_constr env t2 in
+and binop sigma env c t1 t2 =
+  let t1' = oformula_of_constr sigma env t1 in
+  let t2' = oformula_of_constr sigma env t2 in
   c t1' t2'
 
-and binprop env (neg2,depends,origin,path)
+and binprop sigma env (neg2,depends,origin,path)
              add_to_depends neg1 gl c t1 t2 =
   let i = new_connector_id env in
   let depends1 = if add_to_depends then Left i::depends else depends in
   let depends2 = if add_to_depends then Right i::depends else depends in
   if add_to_depends then
-    Hashtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path};
+    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
+    oproposition_of_constr sigma env (neg1,depends1,origin,O_left::path) gl t1 in
   let t2' =
-    oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in
+    oproposition_of_constr sigma env (neg2,depends2,origin,O_right::path) gl t2 in
   (* On numérote le connecteur dans l'environnement. *)
   c i t1' t2'
 
-and mk_equation env ctxt c connector t1 t2 =
-  let t1' = oformula_of_constr env t1 in
-  let t2' = oformula_of_constr env t2 in
+and mk_equation sigma env ctxt c connector t1 t2 =
+  let t1' = oformula_of_constr sigma env t1 in
+  let t2' = oformula_of_constr sigma 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)
 
-and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
+and oproposition_of_constr sigma env ((negated,depends,origin,path) as ctxt) gl c =
   match Z.parse_rel gl c with
-    | Req (t1,t2) -> mk_equation env ctxt c Eq t1 t2
-    | Rne (t1,t2) -> mk_equation env ctxt c Neq t1 t2
-    | Rle (t1,t2) -> mk_equation env ctxt c Leq t1 t2
-    | Rlt (t1,t2) -> mk_equation env ctxt c Lt t1 t2
-    | Rge (t1,t2) -> mk_equation env ctxt c Geq t1 t2
-    | Rgt (t1,t2) -> mk_equation env ctxt c Gt t1 t2
+    | Req (t1,t2) -> mk_equation sigma env ctxt c Eq t1 t2
+    | Rne (t1,t2) -> mk_equation sigma env ctxt c Neq t1 t2
+    | Rle (t1,t2) -> mk_equation sigma env ctxt c Leq t1 t2
+    | Rlt (t1,t2) -> mk_equation sigma env ctxt c Lt t1 t2
+    | Rge (t1,t2) -> mk_equation sigma env ctxt c Geq t1 t2
+    | Rgt (t1,t2) -> mk_equation sigma env ctxt c Gt t1 t2
     | 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 sigma env ctxt' gl t)
+    | Ror (t1,t2) -> binprop sigma env ctxt (not negated) negated gl mkPor t1 t2
+    | Rand (t1,t2) -> binprop sigma 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 sigma 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 sigma env ctxt negated negated gl mkPand
+         (EConstr.mkArrow t1 t2) (EConstr.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
+
+type defined = Defined | Assumed
+
+let reify_hyp sigma env gl i =
+  let open Context.Named.Declaration in
+  let ctxt = (false,[],i,[]) in
+  match Tacmach.New.pf_get_hyp i gl with
+  | LocalDef (_,d,t) when Z.is_int_typ gl t ->
+     let dummy = Lazy.force coq_True in
+     let p = mk_equation sigma env ctxt dummy Eq (EConstr.mkVar i) d in
+     i,Defined,p
+  | LocalDef (_,_,t) | LocalAssum (_,t) ->
+     let p = oproposition_of_constr sigma env ctxt gl t in
+     i,Assumed,p
+
 let reify_gl env gl =
-  let concl = Tacmach.pf_concl gl in
-  let t_concl =
-    Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in
-  if !debug then begin
-    Printf.printf "REIFED PROBLEM\n\n";
-    Printf.printf "  CONCL: "; pprint stdout t_concl; Printf.printf "\n"
-  end;
-  let rec loop = function
-      (i,t) :: lhyps ->
-	let t' = oproposition_of_constr env (false,[],i,[]) gl t in
-	if !debug then begin
-	  Printf.printf "  %s: " (Names.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.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
+  let sigma = Proofview.Goal.sigma gl in
+  let concl = Tacmach.New.pf_concl gl in
+  let hyps = Tacmach.New.pf_ids_of_hyps gl in
+  let ctxt_concl = (true,[],id_concl,[O_mono]) in
+  let t_concl = oproposition_of_constr sigma env ctxt_concl gl concl in
+  let t_lhyps = List.map (reify_hyp sigma env gl) 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} *)
 
@@ -835,7 +632,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;
@@ -844,7 +641,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 =
@@ -856,59 +653,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 mk_refl t = app coq_refl_equal [|Lazy.force Z.typ; t|]
+
+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 = mk_refl 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 *)
@@ -919,22 +718,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) ->
@@ -942,54 +741,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 (EConstr.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
@@ -1021,7 +817,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
@@ -1032,110 +828,81 @@ 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 =
+  let open EConstr in
+  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 =
+  let open EConstr in
+  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
@@ -1147,22 +914,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
@@ -1172,141 +958,113 @@ 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 sigma 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 and variables used in the solution tree *)
+  let useful_equa_ids = equas_of_solution_tree solution_tree in
+  let useful_hypnames, useful_vars =
+    IntSet.fold
+      (fun i (hyps,vars) ->
+        let e = get_equation env i in
+        Id.Set.add e.e_origin.o_hyp hyps,
+        vars_of_equations [e] @@ vars)
+      useful_equa_ids
+      (Id.Set.empty, vars_of_prop reified_concl)
   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 useful_hypnames =
+    Id.Set.elements (Id.Set.remove id_concl useful_hypnames)
+  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
+  (** 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
-  (* variables a introduire *)
-  let to_introduce = add_stated_equations env solution_tree in
-  let stated_vars =  List.map (fun (v,_,_,_) -> v) to_introduce in
-  let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in
-  let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in
-  (* L'environnement de base se construit en deux morceaux :
-     - les variables des équations utiles (et de la conclusion)
-     - les nouvelles variables declarées durant les preuves *)
-  let all_vars_env = useful_vars @ stated_vars in
-  let basic_env =
+  (** 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 sigma 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 id ->
+        match Id.Map.find id reified_hyps with
+        | Defined,p ->
+           reified_of_proposition sigma env p, mk_refl (EConstr.mkVar id)
+        | Assumed,p ->
+           reified_of_proposition sigma env (maximize_prop useful_equa_ids p),
+           EConstr.mkVar id
+        | exception Not_found -> assert false)
+      useful_hypnames
+  in
+  let l_reified_terms, l_reified_hypnames = List.split l_reified_terms 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 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 mk_occ id = {o_hyp=id;o_path=[]} in
   let initial_context =
-    List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) (List.tl l_hyps) in
+    List.map (fun id -> CCHyp (mk_occ id)) useful_hypnames in
   let context =
-    CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
+    CCHyp (mk_occ id_concl) :: hyp_stated_vars @ initial_context in
   let decompose_tactic = decompose_tree env context solution_tree in
 
-  Proofview.V82.of_tactic (Tactics.generalize
-    (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >>
-  Proofview.V82.of_tactic (Tactics.change_concl reified) >>
-  Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
+  Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >>
+  Tactics.convert_concl_no_check reified Term.DEFAULTcast >>
+  Tactics.apply (app coq_do_omega [|decompose_tactic|]) >>
   show_goal >>
-  Proofview.V82.of_tactic (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*)
-  Proofview.V82.of_tactic (Tactics.apply (Lazy.force coq_I))
-
-let total_reflexive_omega_tactic gl =
+  (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 (Lazy.force coq_True) Term.VMcast
+   else
+     Tactics.normalise_vm_in_concl) >>
+  Tactics.apply (Lazy.force coq_I)
+
+let total_reflexive_omega_tactic unsafe =
+  Proofview.Goal.nf_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) = 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,Assumed,Pnot concl) :: hyps in
   let systems_list = destructurate_hyps full_reified_goal in
+  let hyps =
+    List.fold_left (fun s (id,d,p) -> Id.Map.add id (d,p) s) Id.Map.empty hyps
+  in
   if !debug then display_systems systems_list;
-  resolution env full_reified_goal systems_list gl
-  with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system"
-
-
-(*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
-
+  let sigma = Proofview.Goal.sigma gl in
+  resolution unsafe sigma env (concl,hyps) systems_list
+  with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system")
+  end
 
diff --git a/plugins/romega/vo.itarget b/plugins/romega/vo.itarget
deleted file mode 100644
index f7a3c41c..00000000
--- a/plugins/romega/vo.itarget
+++ /dev/null
@@ -1,2 +0,0 @@
-ReflOmegaCore.vo
-ROmega.vo