Imported Upstream snapshot 8.3~beta0+13298

9 files changed, 3411 insertions, 0 deletions

diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
new file mode 100644
index 00000000..30b94571
--- /dev/null
+++ b/plugins/omega/Omega.v
@@ -0,0 +1,59 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(**************************************************************************)
+(*                                                                        *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
+(*                                                                        *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* $Id$ *)
+
+(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
+Require Export ZArith_base.
+Require Export OmegaLemmas.
+Require Export PreOmega.
+Declare ML Module "omega_plugin".
+
+Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
+  Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
+  Zmult_plus_distr_r: zarith.
+
+Require Export Zhints.
+
+(*
+(* The constant minus is required in coq_omega.ml *)
+Require Minus.
+*)
+
+Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith.
+Hint Extern 10 (_ <= _) => abstract omega: zarith.
+Hint Extern 10 (_ < _) => abstract omega: zarith.
+Hint Extern 10 (_ >= _) => abstract omega: zarith.
+Hint Extern 10 (_ > _) => abstract omega: zarith.
+
+Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith.
+Hint Extern 10 (~ _ <= _) => abstract omega: zarith.
+Hint Extern 10 (~ _ < _) => abstract omega: zarith.
+Hint Extern 10 (~ _ >= _) => abstract omega: zarith.
+Hint Extern 10 (~ _ > _) => abstract omega: zarith.
+
+Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith.
+Hint Extern 10 (_ <= _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ < _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ >= _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ > _)%Z => abstract omega: zarith.
+
+Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith.
+
+Hint Extern 10 False => abstract omega: zarith.
\ No newline at end of file
diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
new file mode 100644
index 00000000..56a854d6
--- /dev/null
+++ b/plugins/omega/OmegaLemmas.v
@@ -0,0 +1,302 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+Require Import ZArith_base.
+Open Local Scope Z_scope.
+
+(** Factorization lemmas *)
+
+Theorem Zred_factor0 : forall n:Z, n = n * 1.
+  intro x; rewrite (Zmult_1_r x); reflexivity.
+Qed.
+
+Theorem Zred_factor1 : forall n:Z, n + n = n * 2.
+Proof.
+  exact Zplus_diag_eq_mult_2.
+Qed.
+
+Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m).
+Proof.
+  intros x y; pattern x at 1 in |- *; rewrite <- (Zmult_1_r x);
+    rewrite <- Zmult_plus_distr_r; trivial with arith.
+Qed.
+
+Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m).
+Proof.
+  intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x);
+    rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm;
+      trivial with arith.
+Qed.
+
+Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p).
+Proof.
+  intros x y z; symmetry  in |- *; apply Zmult_plus_distr_r.
+Qed.
+
+Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m.
+Proof.
+  intros x y; rewrite <- Zmult_0_r_reverse; auto with arith.
+Qed.
+
+Theorem Zred_factor6 : forall n:Z, n = n + 0.
+Proof.
+  intro; rewrite Zplus_0_r; trivial with arith.
+Qed.
+
+(** Other specific variants of theorems dedicated for the Omega tactic *)
+
+Lemma new_var : forall x : Z, exists y : Z, x = y.
+intros x; exists x; trivial with arith.
+Qed.
+
+Lemma OMEGA1 : forall x y : Z, x = y -> 0 <= x -> 0 <= y.
+intros x y H; rewrite H; auto with arith.
+Qed.
+
+Lemma OMEGA2 : forall x y : Z, 0 <= x -> 0 <= y -> 0 <= x + y.
+exact Zplus_le_0_compat.
+Qed.
+
+Lemma OMEGA3 : forall x y k : Z, k > 0 -> x = y * k -> x = 0 -> y = 0.
+
+intros x y k H1 H2 H3; apply (Zmult_integral_l k);
+ [ unfold not in |- *; intros H4; absurd (k > 0);
+    [ rewrite H4; unfold Zgt in |- *; simpl in |- *; discriminate
+    | assumption ]
+ | rewrite <- H2; assumption ].
+Qed.
+
+Lemma OMEGA4 : forall x y z : Z, x > 0 -> y > x -> z * y + x <> 0.
+
+unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0);
+ [ intros H4; cut (0 <= z * y + x);
+    [ intros H5; generalize (Zmult_le_approx y z x H4 H2 H5); intros H6;
+       absurd (z * y + x > 0);
+       [ rewrite H3; unfold Zgt in |- *; simpl in |- *; discriminate
+       | apply Zle_gt_trans with x;
+          [ pattern x at 1 in |- *; rewrite <- (Zplus_0_l x);
+             apply Zplus_le_compat_r; rewrite Zmult_comm;
+             generalize H4; unfold Zgt in |- *; case y;
+             [ simpl in |- *; intros H7; discriminate H7
+             | intros p H7; rewrite <- (Zmult_0_r (Zpos p));
+                unfold Zle in |- *; rewrite Zcompare_mult_compat;
+                exact H6
+             | simpl in |- *; intros p H7; discriminate H7 ]
+          | assumption ] ]
+    | rewrite H3; unfold Zle in |- *; simpl in |- *; discriminate ]
+ | apply Zgt_trans with x; [ assumption | assumption ] ].
+Qed.
+
+Lemma OMEGA5 : forall x y z : Z, x = 0 -> y = 0 -> x + y * z = 0.
+
+intros x y z H1 H2; rewrite H1; rewrite H2; simpl in |- *; trivial with arith.
+Qed.
+
+Lemma OMEGA6 : forall x y z : Z, 0 <= x -> y = 0 -> 0 <= x + y * z.
+
+intros x y z H1 H2; rewrite H2; simpl in |- *; rewrite Zplus_0_r; assumption.
+Qed.
+
+Lemma OMEGA7 :
+ forall x y z t : Z, z > 0 -> t > 0 -> 0 <= x -> 0 <= y -> 0 <= x * z + y * t.
+
+intros x y z t H1 H2 H3 H4; rewrite <- (Zplus_0_l 0); apply Zplus_le_compat;
+ apply Zmult_gt_0_le_0_compat; assumption.
+Qed.
+
+Lemma OMEGA8 : forall x y : Z, 0 <= x -> 0 <= y -> x = - y -> x = 0.
+
+intros x y H1 H2 H3; elim (Zle_lt_or_eq 0 x H1);
+ [ intros H4; absurd (0 < x);
+    [ change (0 >= x) in |- *; apply Zle_ge; apply Zplus_le_reg_l with y;
+       rewrite H3; rewrite Zplus_opp_r; rewrite Zplus_0_r;
+       assumption
+    | assumption ]
+ | intros H4; rewrite H4; trivial with arith ].
+Qed.
+
+Lemma OMEGA9 : forall x y z t : Z, y = 0 -> x = z -> y + (- x + z) * t = 0.
+
+intros x y z t H1 H2; rewrite H2; rewrite Zplus_opp_l; rewrite Zmult_0_l;
+ rewrite Zplus_0_r; assumption.
+Qed.
+
+Lemma OMEGA10 :
+ forall v c1 c2 l1 l2 k1 k2 : Z,
+ (v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
+ v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ rewrite (Zplus_permute (l1 * k1) (v * c2 * k2)); trivial with arith.
+Qed.
+
+Lemma OMEGA11 :
+ forall v1 c1 l1 l2 k1 : Z,
+ (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ trivial with arith.
+Qed.
+
+Lemma OMEGA12 :
+ forall v2 c2 l1 l2 k2 : Z,
+ l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ rewrite Zplus_permute; trivial with arith.
+Qed.
+
+Lemma OMEGA13 :
+ forall (v l1 l2 : Z) (x : positive),
+ v * Zpos x + l1 + (v * Zneg x + l2) = l1 + l2.
+
+intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zpos x) l1);
+ rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r;
+ rewrite <- Zopp_neg; rewrite (Zplus_comm (- Zneg x) (Zneg x));
+ rewrite Zplus_opp_r; rewrite Zmult_0_r; rewrite Zplus_0_r;
+ trivial with arith.
+Qed.
+
+Lemma OMEGA14 :
+ forall (v l1 l2 : Z) (x : positive),
+ v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2.
+
+intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zneg x) l1);
+ rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r;
+ rewrite <- Zopp_neg; rewrite Zplus_opp_r; rewrite Zmult_0_r;
+ rewrite Zplus_0_r; trivial with arith.
+Qed.
+Lemma OMEGA15 :
+ forall v c1 c2 l1 l2 k2 : Z,
+ v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ rewrite (Zplus_permute l1 (v * c2 * k2)); trivial with arith.
+Qed.
+
+Lemma OMEGA16 : forall v c l k : Z, (v * c + l) * k = v * (c * k) + l * k.
+
+intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
+ repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
+ trivial with arith.
+Qed.
+
+Lemma OMEGA17 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
+
+unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1;
+ apply Zplus_reg_l with (y * z); rewrite Zplus_comm;
+ rewrite H3; rewrite H2; auto with arith.
+Qed.
+
+Lemma OMEGA18 : forall x y k : Z, x = y * k -> Zne x 0 -> Zne y 0.
+
+unfold Zne, not in |- *; intros x y k H1 H2 H3; apply H2; rewrite H1;
+ rewrite H3; auto with arith.
+Qed.
+
+Lemma OMEGA19 : forall x : Z, Zne x 0 -> 0 <= x + -1 \/ 0 <= x * -1 + -1.
+
+unfold Zne in |- *; intros x H; elim (Zle_or_lt 0 x);
+ [ intros H1; elim Zle_lt_or_eq with (1 := H1);
+    [ intros H2; left; change (0 <= Zpred x) in |- *; apply Zsucc_le_reg;
+       rewrite <- Zsucc_pred; apply Zlt_le_succ; assumption
+    | intros H2; absurd (x = 0); auto with arith ]
+ | intros H1; right; rewrite <- Zopp_eq_mult_neg_1; rewrite Zplus_comm;
+    apply Zle_left; apply Zsucc_le_reg; simpl in |- *;
+    apply Zlt_le_succ; auto with arith ].
+Qed.
+
+Lemma OMEGA20 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
+
+unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1; rewrite H2 in H3;
+ simpl in H3; rewrite Zplus_0_r in H3; trivial with arith.
+Qed.
+
+Definition fast_Zplus_comm (x y : Z) (P : Z -> Prop)
+  (H : P (y + x)) := eq_ind_r P H (Zplus_comm x y).
+
+Definition fast_Zplus_assoc_reverse (n m p : Z) (P : Z -> Prop)
+  (H : P (n + (m + p))) := eq_ind_r P H (Zplus_assoc_reverse n m p).
+
+Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop)
+  (H : P (n + m + p)) := eq_ind_r P H (Zplus_assoc n m p).
+
+Definition fast_Zplus_permute (n m p : Z) (P : Z -> Prop)
+  (H : P (m + (n + p))) := eq_ind_r P H (Zplus_permute n m p).
+
+Definition fast_OMEGA10 (v c1 c2 l1 l2 k1 k2 : Z) (P : Z -> Prop)
+  (H : P (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))) :=
+  eq_ind_r P H (OMEGA10 v c1 c2 l1 l2 k1 k2).
+
+Definition fast_OMEGA11 (v1 c1 l1 l2 k1 : Z) (P : Z -> Prop)
+  (H : P (v1 * (c1 * k1) + (l1 * k1 + l2))) :=
+  eq_ind_r P H (OMEGA11 v1 c1 l1 l2 k1).
+Definition fast_OMEGA12 (v2 c2 l1 l2 k2 : Z) (P : Z -> Prop)
+  (H : P (v2 * (c2 * k2) + (l1 + l2 * k2))) :=
+  eq_ind_r P H (OMEGA12 v2 c2 l1 l2 k2).
+
+Definition fast_OMEGA15 (v c1 c2 l1 l2 k2 : Z) (P : Z -> Prop)
+  (H : P (v * (c1 + c2 * k2) + (l1 + l2 * k2))) :=
+  eq_ind_r P H (OMEGA15 v c1 c2 l1 l2 k2).
+Definition fast_OMEGA16 (v c l k : Z) (P : Z -> Prop)
+  (H : P (v * (c * k) + l * k)) := eq_ind_r P H (OMEGA16 v c l k).
+
+Definition fast_OMEGA13 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
+  (H : P (l1 + l2)) := eq_ind_r P H (OMEGA13 v l1 l2 x).
+
+Definition fast_OMEGA14 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
+  (H : P (l1 + l2)) := eq_ind_r P H (OMEGA14 v l1 l2 x).
+Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop)
+  (H : P (x * 1)) := eq_ind_r P H (Zred_factor0 x).
+
+Definition fast_Zopp_eq_mult_neg_1 (x : Z) (P : Z -> Prop)
+  (H : P (x * -1)) := eq_ind_r P H (Zopp_eq_mult_neg_1 x).
+
+Definition fast_Zmult_comm (x y : Z) (P : Z -> Prop)
+  (H : P (y * x)) := eq_ind_r P H (Zmult_comm x y).
+
+Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop)
+  (H : P (- x + - y)) := eq_ind_r P H (Zopp_plus_distr x y).
+
+Definition fast_Zopp_involutive (x : Z) (P : Z -> Prop) (H : P x) :=
+  eq_ind_r P H (Zopp_involutive x).
+
+Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop)
+  (H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y).
+
+Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop)
+  (H : P (n * p + m * p)) := eq_ind_r P H (Zmult_plus_distr_l n m p).
+Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop)
+  (H : P (x * - y)) := eq_ind_r P H (Zmult_opp_comm x y).
+
+Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop)
+  (H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p).
+
+Definition fast_Zred_factor1 (x : Z) (P : Z -> Prop)
+  (H : P (x * 2)) := eq_ind_r P H (Zred_factor1 x).
+
+Definition fast_Zred_factor2 (x y : Z) (P : Z -> Prop)
+  (H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor2 x y).
+
+Definition fast_Zred_factor3 (x y : Z) (P : Z -> Prop)
+  (H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor3 x y).
+
+Definition fast_Zred_factor4 (x y z : Z) (P : Z -> Prop)
+  (H : P (x * (y + z))) := eq_ind_r P H (Zred_factor4 x y z).
+
+Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop)
+  (H : P y) := eq_ind_r P H (Zred_factor5 x y).
+
+Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop)
+  (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
new file mode 100644
index 00000000..21535f0d
--- /dev/null
+++ b/plugins/omega/OmegaPlugin.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+Declare ML Module "omega_plugin".
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
new file mode 100644
index 00000000..a5a085a9
--- /dev/null
+++ b/plugins/omega/PreOmega.v
@@ -0,0 +1,445 @@
+Require Import Arith Max Min ZArith_base NArith Nnat.
+
+Open Local Scope Z_scope.
+
+
+(** * zify: the Z-ification tactic *)
+
+(* This tactic searches for nat and N and positive elements in the goal and
+   translates everything into Z. It is meant as a pre-processor for
+   (r)omega; for instance a positivity hypothesis is added whenever
+     - a multiplication is encountered
+     - an atom is encountered (that is a variable or an unknown construct)
+
+   Recognized relations (can be handled as deeply as allowed by setoid rewrite):
+     - { eq, le, lt, ge, gt } on { Z, positive, N, nat }
+
+   Recognized operations:
+     - on Z: Zmin, Zmax, Zabs, Zsgn are translated in term of <= < =
+     - on nat: + * - S O pred min max nat_of_P nat_of_N Zabs_nat
+     - on positive: Zneg Zpos xI xO xH + * - Psucc Ppred Pmin Pmax P_of_succ_nat
+     - on N: N0 Npos + * - Nsucc Nmin Nmax N_of_nat Zabs_N
+*)
+
+
+
+
+(** I) translation of Zmax, Zmin, Zabs, Zsgn into recognized equations *)
+
+Ltac zify_unop_core t thm a :=
+ (* Let's introduce the specification theorem for t *)
+ let H:= fresh "H" in assert (H:=thm a);
+ (* Then we replace (t a) everywhere with a fresh variable *)
+ let z := fresh "z" in set (z:=t a) in *; clearbody z.
+
+Ltac zify_unop_var_or_term t thm a :=
+ (* If a is a variable, no need for aliasing *)
+ let za := fresh "z" in
+ (rename a into za; rename za into a; zify_unop_core t thm a) ||
+ (* Otherwise, a is a complex term: we alias it. *)
+ (remember a as za; zify_unop_core t thm za).
+
+Ltac zify_unop t thm a :=
+ (* if a is a scalar, we can simply reduce the unop *)
+ let isz := isZcst a in
+ match isz with
+  | true => simpl (t a) in *
+  | _ => zify_unop_var_or_term t thm a
+ end.
+
+Ltac zify_unop_nored t thm a :=
+ (* in this version, we don't try to reduce the unop (that can be (Zplus x)) *)
+ let isz := isZcst a in
+ match isz with
+  | true => zify_unop_core t thm a
+  | _ => zify_unop_var_or_term t thm a
+ end.
+
+Ltac zify_binop t thm a b:=
+ (* works as zify_unop, except that we should be careful when
+    dealing with b, since it can be equal to a *)
+ let isza := isZcst a in
+ match isza with
+   | true => zify_unop (t a) (thm a) b
+   | _ =>
+       let za := fresh "z" in
+       (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) ||
+       (remember a as za; match goal with
+         | H : za = b |- _ => zify_unop_nored (t za) (thm za) za
+         | _ => zify_unop_nored (t za) (thm za) b
+        end)
+ end.
+
+Ltac zify_op_1 :=
+  match goal with
+   | |- context [ Zmax ?a ?b ] => zify_binop Zmax Zmax_spec a b
+   | H : context [ Zmax ?a ?b ] |- _ => zify_binop Zmax Zmax_spec a b
+   | |- context [ Zmin ?a ?b ] => zify_binop Zmin Zmin_spec a b
+   | H : context [ Zmin ?a ?b ] |- _ => zify_binop Zmin Zmin_spec a b
+   | |- context [ Zsgn ?a ] => zify_unop Zsgn Zsgn_spec a
+   | H : context [ Zsgn ?a ] |- _ => zify_unop Zsgn Zsgn_spec a
+   | |- context [ Zabs ?a ] => zify_unop Zabs Zabs_spec a
+   | H : context [ Zabs ?a ] |- _ => zify_unop Zabs Zabs_spec a
+  end.
+
+Ltac zify_op := repeat zify_op_1.
+
+
+
+
+
+(** II) Conversion from nat to Z *)
+
+
+Definition Z_of_nat' := Z_of_nat.
+
+Ltac hide_Z_of_nat t :=
+  let z := fresh "z" in set (z:=Z_of_nat t) in *;
+  change Z_of_nat with Z_of_nat' in z;
+  unfold z in *; clear z.
+
+Ltac zify_nat_rel :=
+ match goal with
+  (* I: equalities *)
+  | H : (@eq nat ?a ?b) |- _ => generalize (inj_eq _ _ H); clear H; intro H
+  | |- (@eq nat ?a ?b) => apply (inj_eq_rev a b)
+  | H : context [ @eq nat ?a ?b ] |- _ => rewrite (inj_eq_iff a b) in H
+  | |- context [ @eq nat ?a ?b ] =>       rewrite (inj_eq_iff a b)
+  (* II: less than *)
+  | H : (lt ?a ?b) |- _ => generalize (inj_lt _ _ H); clear H; intro H
+  | |- (lt ?a ?b) => apply (inj_lt_rev a b)
+  | H : context [ lt ?a ?b ] |- _ => rewrite (inj_lt_iff a b) in H
+  | |- context [ lt ?a ?b ] =>       rewrite (inj_lt_iff a b)
+  (* III: less or equal *)
+  | H : (le ?a ?b) |- _ => generalize (inj_le _ _ H); clear H; intro H
+  | |- (le ?a ?b) => apply (inj_le_rev a b)
+  | H : context [ le ?a ?b ] |- _ => rewrite (inj_le_iff a b) in H
+  | |- context [ le ?a ?b ] =>       rewrite (inj_le_iff a b)
+  (* IV: greater than *)
+  | H : (gt ?a ?b) |- _ => generalize (inj_gt _ _ H); clear H; intro H
+  | |- (gt ?a ?b) => apply (inj_gt_rev a b)
+  | H : context [ gt ?a ?b ] |- _ => rewrite (inj_gt_iff a b) in H
+  | |- context [ gt ?a ?b ] =>       rewrite (inj_gt_iff a b)
+  (* V: greater or equal *)
+  | H : (ge ?a ?b) |- _ => generalize (inj_ge _ _ H); clear H; intro H
+  | |- (ge ?a ?b) => apply (inj_ge_rev a b)
+  | H : context [ ge ?a ?b ] |- _ => rewrite (inj_ge_iff a b) in H
+  | |- context [ ge ?a ?b ] =>       rewrite (inj_ge_iff a b)
+ end.
+
+Ltac zify_nat_op :=
+ match goal with
+  (* misc type conversions: positive/N/Z to nat *)
+  | H : context [ Z_of_nat (nat_of_P ?a) ] |- _ => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a) in H
+  | |- context [ Z_of_nat (nat_of_P ?a) ] => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a)
+  | H : context [ Z_of_nat (nat_of_N ?a) ] |- _ => rewrite (Z_of_nat_of_N a) in H
+  | |- context [ Z_of_nat (nat_of_N ?a) ] => rewrite (Z_of_nat_of_N a)
+  | H : context [ Z_of_nat (Zabs_nat ?a) ] |- _ => rewrite (inj_Zabs_nat a) in H
+  | |- context [ Z_of_nat (Zabs_nat ?a) ] => rewrite (inj_Zabs_nat a)
+
+  (* plus -> Zplus *)
+  | H : context [ Z_of_nat (plus ?a ?b) ] |- _ => rewrite (inj_plus a b) in H
+  | |- context [ Z_of_nat (plus ?a ?b) ] => rewrite (inj_plus a b)
+
+  (* min -> Zmin *)
+  | H : context [ Z_of_nat (min ?a ?b) ] |- _ => rewrite (inj_min a b) in H
+  | |- context [ Z_of_nat (min ?a ?b) ] => rewrite (inj_min a b)
+
+  (* max -> Zmax *)
+  | H : context [ Z_of_nat (max ?a ?b) ] |- _ => rewrite (inj_max a b) in H
+  | |- context [ Z_of_nat (max ?a ?b) ] => rewrite (inj_max a b)
+
+  (* minus -> Zmax (Zminus ... ...) 0 *)
+  | H : context [ Z_of_nat (minus ?a ?b) ] |- _ => rewrite (inj_minus a b) in H
+  | |- context [ Z_of_nat (minus ?a ?b) ] => rewrite (inj_minus a b)
+
+  (* pred -> minus ... -1 -> Zmax (Zminus ... -1) 0 *)
+  | H : context [ Z_of_nat (pred ?a) ] |- _ => rewrite (pred_of_minus a) in H
+  | |- context [ Z_of_nat (pred ?a) ] => rewrite (pred_of_minus a)
+
+  (* mult -> Zmult and a positivity hypothesis *)
+  | H : context [ Z_of_nat (mult ?a ?b) ] |- _ =>
+        let H:= fresh "H" in
+        assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+  | |- context [ Z_of_nat (mult ?a ?b) ] =>
+        let H:= fresh "H" in
+        assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+
+  (* O -> Z0 *)
+  | H : context [ Z_of_nat O ] |- _ => simpl (Z_of_nat O) in H
+  | |- context [ Z_of_nat O ] => simpl (Z_of_nat O)
+
+  (* S -> number or Zsucc *)
+  | H : context [ Z_of_nat (S ?a) ] |- _ =>
+     let isnat := isnatcst a in
+     match isnat with
+      | true => simpl (Z_of_nat (S a)) in H
+      | _ => rewrite (inj_S a) in H
+     end
+  | |- context [ Z_of_nat (S ?a) ] =>
+     let isnat := isnatcst a in
+     match isnat with
+      | true => simpl (Z_of_nat (S a))
+      | _ => rewrite (inj_S a)
+     end
+
+  (* atoms of type nat : we add a positivity condition (if not already there) *)
+  | H : context [ Z_of_nat ?a ] |- _ =>
+        match goal with
+          | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a
+          | H' : 0 <= Z_of_nat' a |- _ => fail
+          | _ => let H:= fresh "H" in
+                 assert (H:=Zle_0_nat a); hide_Z_of_nat a
+        end
+  | |- context [ Z_of_nat ?a ] =>
+        match goal with
+          | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a
+          | H' : 0 <= Z_of_nat' a |- _ => fail
+          | _ => let H:= fresh "H" in
+                 assert (H:=Zle_0_nat a); hide_Z_of_nat a
+        end
+ end.
+
+Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *.
+
+
+
+
+(* III) conversion from positive to Z *)
+
+Definition Zpos' := Zpos.
+Definition Zneg' := Zneg.
+
+Ltac hide_Zpos t :=
+  let z := fresh "z" in set (z:=Zpos t) in *;
+  change Zpos with Zpos' in z;
+  unfold z in *; clear z.
+
+Ltac zify_positive_rel :=
+ match goal with
+  (* I: equalities *)
+  | H : (@eq positive ?a ?b) |- _ => generalize (Zpos_eq _ _ H); clear H; intro H
+  | |- (@eq positive ?a ?b) => apply (Zpos_eq_rev a b)
+  | H : context [ @eq positive ?a ?b ] |- _ => rewrite (Zpos_eq_iff a b) in H
+  | |- context [ @eq positive ?a ?b ] =>       rewrite (Zpos_eq_iff a b)
+  (* II: less than *)
+  | H : context [ (?a<?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H
+  | |- context [ (?a<?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b)
+  (* III: less or equal *)
+  | H : context [ (?a<=?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H
+  | |- context [ (?a<=?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b)
+  (* IV: greater than *)
+  | H : context [ (?a>?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H
+  | |- context [ (?a>?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b)
+  (* V: greater or equal *)
+  | H : context [ (?a>=?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H
+  | |- context [ (?a>=?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b)
+ end.
+
+Ltac zify_positive_op :=
+ match goal with
+  (* Zneg -> -Zpos (except for numbers) *)
+  | H : context [ Zneg ?a ] |- _ =>
+     let isp := isPcst a in
+     match isp with
+      | true => change (Zneg a) with (Zneg' a) in H
+      | _ => change (Zneg a) with (- Zpos a) in H
+     end
+  | |- context [ Zneg ?a ] =>
+     let isp := isPcst a in
+     match isp with
+      | true => change (Zneg a) with (Zneg' a)
+      | _ => change (Zneg a) with (- Zpos a)
+     end
+
+  (* misc type conversions: nat to positive *)
+  | H : context [ Zpos (P_of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H
+  | |- context [ Zpos (P_of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a)
+
+  (* Pplus -> Zplus *)
+  | H : context [ Zpos (Pplus ?a ?b) ] |- _ => change (Zpos (Pplus a b)) with (Zplus (Zpos a) (Zpos b)) in H
+  | |- context [ Zpos (Pplus ?a ?b) ] => change (Zpos (Pplus a b)) with (Zplus (Zpos a) (Zpos b))
+
+  (* Pmin -> Zmin *)
+  | H : context [ Zpos (Pmin ?a ?b) ] |- _ => rewrite (Zpos_min a b) in H
+  | |- context [ Zpos (Pmin ?a ?b) ] => rewrite (Zpos_min a b)
+
+  (* Pmax -> Zmax *)
+  | H : context [ Zpos (Pmax ?a ?b) ] |- _ => rewrite (Zpos_max a b) in H
+  | |- context [ Zpos (Pmax ?a ?b) ] => rewrite (Zpos_max a b)
+
+  (* Pminus -> Zmax 1 (Zminus ... ...) *)
+  | H : context [ Zpos (Pminus ?a ?b) ] |- _ => rewrite (Zpos_minus a b) in H
+  | |- context [ Zpos (Pminus ?a ?b) ] => rewrite (Zpos_minus a b)
+
+  (* Psucc -> Zsucc *)
+  | H : context [ Zpos (Psucc ?a) ] |- _ => rewrite (Zpos_succ_morphism a) in H
+  | |- context [ Zpos (Psucc ?a) ] => rewrite (Zpos_succ_morphism a)
+
+  (* Ppred -> Pminus ... -1 -> Zmax 1 (Zminus ... - 1) *)
+  | H : context [ Zpos (Ppred ?a) ] |- _ => rewrite (Ppred_minus a) in H
+  | |- context [ Zpos (Ppred ?a) ] => rewrite (Ppred_minus a)
+
+  (* Pmult -> Zmult and a positivity hypothesis *)
+  | H : context [ Zpos (Pmult ?a ?b) ] |- _ =>
+        let H:= fresh "H" in
+        assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+  | |- context [ Zpos (Pmult ?a ?b) ] =>
+        let H:= fresh "H" in
+        assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+
+  (* xO *)
+  | H : context [ Zpos (xO ?a) ] |- _ =>
+     let isp := isPcst a in
+     match isp with
+      | true => change (Zpos (xO a)) with (Zpos' (xO a)) in H
+      | _ => rewrite (Zpos_xO a) in H
+     end
+  | |- context [ Zpos (xO ?a) ] =>
+     let isp := isPcst a in
+     match isp with
+      | true => change (Zpos (xO a)) with (Zpos' (xO a))
+      | _ => rewrite (Zpos_xO a)
+     end
+  (* xI *)
+  | H : context [ Zpos (xI ?a) ] |- _ =>
+     let isp := isPcst a in
+     match isp with
+      | true => change (Zpos (xI a)) with (Zpos' (xI a)) in H
+      | _ => rewrite (Zpos_xI a) in H
+     end
+  | |- context [ Zpos (xI ?a) ] =>
+     let isp := isPcst a in
+     match isp with
+      | true => change (Zpos (xI a)) with (Zpos' (xI a))
+      | _ => rewrite (Zpos_xI a)
+     end
+
+  (* xI : nothing to do, just prevent adding a useless positivity condition *)
+  | H : context [ Zpos xH ] |- _ => hide_Zpos xH
+  | |- context [ Zpos xH ] => hide_Zpos xH
+
+  (* atoms of type positive : we add a positivity condition (if not already there) *)
+  | H : context [ Zpos ?a ] |- _ =>
+        match goal with
+         | H' : Zpos a > 0 |- _ => hide_Zpos a
+         | H' : Zpos' a > 0 |- _ => fail
+         | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a
+        end
+  | |- context [ Zpos ?a ] =>
+        match goal with
+         | H' : Zpos a > 0 |- _ => hide_Zpos a
+         | H' : Zpos' a > 0 |- _ => fail
+         | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a
+        end
+ end.
+
+Ltac zify_positive :=
+ repeat zify_positive_rel; repeat zify_positive_op; unfold Zpos',Zneg' in *.
+
+
+
+
+
+(* IV) conversion from N to Z *)
+
+Definition Z_of_N' := Z_of_N.
+
+Ltac hide_Z_of_N t :=
+  let z := fresh "z" in set (z:=Z_of_N t) in *;
+  change Z_of_N with Z_of_N' in z;
+  unfold z in *; clear z.
+
+Ltac zify_N_rel :=
+ match goal with
+  (* I: equalities *)
+  | H : (@eq N ?a ?b) |- _ => generalize (Z_of_N_eq _ _ H); clear H; intro H
+  | |- (@eq N ?a ?b) => apply (Z_of_N_eq_rev a b)
+  | H : context [ @eq N ?a ?b ] |- _ => rewrite (Z_of_N_eq_iff a b) in H
+  | |- context [ @eq N ?a ?b ] =>       rewrite (Z_of_N_eq_iff a b)
+  (* II: less than *)
+  | H : (?a<?b)%N |- _ => generalize (Z_of_N_lt _ _ H); clear H; intro H
+  | |- (?a<?b)%N => apply (Z_of_N_lt_rev a b)
+  | H : context [ (?a<?b)%N ] |- _ => rewrite (Z_of_N_lt_iff a b) in H
+  | |- context [ (?a<?b)%N ] =>       rewrite (Z_of_N_lt_iff a b)
+  (* III: less or equal *)
+  | H : (?a<=?b)%N |- _ => generalize (Z_of_N_le _ _ H); clear H; intro H
+  | |- (?a<=?b)%N => apply (Z_of_N_le_rev a b)
+  | H : context [ (?a<=?b)%N ] |- _ => rewrite (Z_of_N_le_iff a b) in H
+  | |- context [ (?a<=?b)%N ] =>       rewrite (Z_of_N_le_iff a b)
+  (* IV: greater than *)
+  | H : (?a>?b)%N |- _ => generalize (Z_of_N_gt _ _ H); clear H; intro H
+  | |- (?a>?b)%N => apply (Z_of_N_gt_rev a b)
+  | H : context [ (?a>?b)%N ] |- _ => rewrite (Z_of_N_gt_iff a b) in H
+  | |- context [ (?a>?b)%N ] =>       rewrite (Z_of_N_gt_iff a b)
+  (* V: greater or equal *)
+  | H : (?a>=?b)%N |- _ => generalize (Z_of_N_ge _ _ H); clear H; intro H
+  | |- (?a>=?b)%N => apply (Z_of_N_ge_rev a b)
+  | H : context [ (?a>=?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H
+  | |- context [ (?a>=?b)%N ] =>       rewrite (Z_of_N_ge_iff a b)
+ end.
+
+Ltac zify_N_op :=
+ match goal with
+  (* misc type conversions: nat to positive *)
+  | H : context [ Z_of_N (N_of_nat ?a) ] |- _ => rewrite (Z_of_N_of_nat a) in H
+  | |- context [ Z_of_N (N_of_nat ?a) ] => rewrite (Z_of_N_of_nat a)
+  | H : context [ Z_of_N (Zabs_N ?a) ] |- _ => rewrite (Z_of_N_abs a) in H
+  | |- context [ Z_of_N (Zabs_N ?a) ] => rewrite (Z_of_N_abs a)
+  | H : context [ Z_of_N (Npos ?a) ] |- _ => rewrite (Z_of_N_pos a) in H
+  | |- context [ Z_of_N (Npos ?a) ] => rewrite (Z_of_N_pos a)
+  | H : context [ Z_of_N N0 ] |- _ => change (Z_of_N N0) with Z0 in H
+  | |- context [ Z_of_N N0 ] => change (Z_of_N N0) with Z0
+
+  (* Nplus -> Zplus *)
+  | H : context [ Z_of_N (Nplus ?a ?b) ] |- _ => rewrite (Z_of_N_plus a b) in H
+  | |- context [ Z_of_N (Nplus ?a ?b) ] => rewrite (Z_of_N_plus a b)
+
+  (* Nmin -> Zmin *)
+  | H : context [ Z_of_N (Nmin ?a ?b) ] |- _ => rewrite (Z_of_N_min a b) in H
+  | |- context [ Z_of_N (Nmin ?a ?b) ] => rewrite (Z_of_N_min a b)
+
+  (* Nmax -> Zmax *)
+  | H : context [ Z_of_N (Nmax ?a ?b) ] |- _ => rewrite (Z_of_N_max a b) in H
+  | |- context [ Z_of_N (Nmax ?a ?b) ] => rewrite (Z_of_N_max a b)
+
+  (* Nminus -> Zmax 0 (Zminus ... ...) *)
+  | H : context [ Z_of_N (Nminus ?a ?b) ] |- _ => rewrite (Z_of_N_minus a b) in H
+  | |- context [ Z_of_N (Nminus ?a ?b) ] => rewrite (Z_of_N_minus a b)
+
+  (* Nsucc -> Zsucc *)
+  | H : context [ Z_of_N (Nsucc ?a) ] |- _ => rewrite (Z_of_N_succ a) in H
+  | |- context [ Z_of_N (Nsucc ?a) ] => rewrite (Z_of_N_succ a)
+
+  (* Nmult -> Zmult and a positivity hypothesis *)
+  | H : context [ Z_of_N (Nmult ?a ?b) ] |- _ =>
+        let H:= fresh "H" in
+        assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
+  | |- context [ Z_of_N  (Nmult ?a ?b) ] =>
+        let H:= fresh "H" in
+        assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
+
+  (* atoms of type N : we add a positivity condition (if not already there) *)
+  | H : context [ Z_of_N ?a ] |- _ =>
+        match goal with
+         | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a
+         | H' : 0 <= Z_of_N' a |- _ => fail
+         | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a
+        end
+  | |- context [ Z_of_N ?a ] =>
+        match goal with
+         | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a
+         | H' : 0 <= Z_of_N' a |- _ => fail
+         | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a
+        end
+ end.
+
+Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
+
+
+
+(** The complete Z-ification tactic *)
+
+Ltac zify :=
+ repeat progress (zify_nat; zify_positive; zify_N); zify_op.
+
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
new file mode 100644
index 00000000..60616845
--- /dev/null
+++ b/plugins/omega/coq_omega.ml
@@ -0,0 +1,1823 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(**************************************************************************)
+(*                                                                        *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
+(*                                                                        *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Pp
+open Reduction
+open Proof_type
+open Names
+open Nameops
+open Term
+open Termops
+open Declarations
+open Environ
+open Sign
+open Inductive
+open Tacticals
+open Tacmach
+open Evar_refiner
+open Tactics
+open Clenv
+open Logic
+open Libnames
+open Nametab
+open Contradiction
+
+module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
+open OmegaSolver
+
+(* Added by JCF, 09/03/98 *)
+
+let elim_id id gl = simplest_elim (pf_global gl id) gl
+let resolve_id id gl = apply (pf_global gl id) gl
+
+let timing timer_name f arg = f arg
+
+let display_time_flag = ref false
+let display_system_flag = ref false
+let display_action_flag = ref false
+let old_style_flag = ref false
+
+let read f () = !f
+let write f x = f:=x
+
+open Goptions
+
+let _ =
+  declare_bool_option
+    { optsync  = false;
+      optname  = "Omega system time displaying flag";
+      optkey   = ["Omega";"System"];
+      optread  = read display_system_flag;
+      optwrite = write display_system_flag }
+
+let _ =
+  declare_bool_option
+    { optsync  = false;
+      optname  = "Omega action display flag";
+      optkey   = ["Omega";"Action"];
+      optread  = read display_action_flag;
+      optwrite = write display_action_flag }
+
+let _ =
+  declare_bool_option
+    { optsync  = false;
+      optname  = "Omega old style flag";
+      optkey   = ["Omega";"OldStyle"];
+      optread  = read old_style_flag;
+      optwrite = write old_style_flag }
+
+
+let all_time        = timing "Omega     "
+let solver_time     = timing "Solver    "
+let exact_time      = timing "Rewrites  "
+let elim_time       = timing "Elim      "
+let simpl_time      = timing "Simpl     "
+let generalize_time = timing "Generalize"
+
+let new_identifier =
+  let cpt = ref 0 in
+  (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; id_of_string s)
+
+let new_identifier_state =
+  let cpt = ref 0 in
+  (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s)
+
+let new_identifier_var =
+  let cpt = ref 0 in
+  (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s)
+
+let new_id =
+  let cpt = ref 0 in fun () -> incr cpt; !cpt
+
+let new_var_num =
+  let cpt = ref 1000 in (fun () -> incr cpt; !cpt)
+
+let new_var =
+  let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
+
+let display_var i = Printf.sprintf "X%d" i
+
+let intern_id,unintern_id =
+  let cpt = ref 0 in
+  let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in
+  (fun (name : identifier) ->
+     try Hashtbl.find table name with Not_found ->
+       let idx = !cpt in
+       Hashtbl.add table name idx;
+       Hashtbl.add co_table idx name;
+       incr cpt; idx),
+  (fun idx ->
+     try Hashtbl.find co_table idx with Not_found ->
+       let v = new_var () in
+       Hashtbl.add table v idx; Hashtbl.add co_table idx v; v)
+
+let mk_then = tclTHENLIST
+
+let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c])
+
+let generalize_tac t = generalize_time (generalize t)
+let elim t = elim_time (simplest_elim t)
+let exact t = exact_time (Tactics.refine t)
+let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s]
+
+let rev_assoc k =
+  let rec loop = function
+    | [] -> raise Not_found | (v,k')::_ when k = k' -> v | _ :: l -> loop l
+  in
+  loop
+
+let tag_hypothesis,tag_of_hyp, hyp_of_tag =
+  let l = ref ([]:(identifier * int) list) in
+  (fun h id -> l := (h,id):: !l),
+  (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"),
+  (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis")
+
+let hide_constr,find_constr,clear_tables,dump_tables =
+  let l = ref ([]:(constr * (identifier * identifier * bool)) list) in
+  (fun h id eg b -> l := (h,(id,eg,b)):: !l),
+  (fun h -> try List.assoc h !l with Not_found -> failwith "find_contr"),
+  (fun () -> l := []),
+  (fun () -> !l)
+
+(* Lazy evaluation is used for Coq constants, because this code
+ is evaluated before the compiled modules are loaded.
+ To use the constant Zplus, one must type "Lazy.force coq_Zplus"
+ This is the right way to access to Coq constants in tactics ML code *)
+
+open Coqlib
+
+let logic_dir = ["Coq";"Logic";"Decidable"]
+let coq_modules =
+  init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
+    @ [["Coq"; "omega"; "OmegaLemmas"]]
+
+let init_constant = gen_constant_in_modules "Omega" init_modules
+let constant = gen_constant_in_modules "Omega" coq_modules
+
+(* Zarith *)
+let coq_xH = lazy (constant "xH")
+let coq_xO = lazy (constant "xO")
+let coq_xI = lazy (constant "xI")
+let coq_Z0 = lazy (constant "Z0")
+let coq_Zpos = lazy (constant "Zpos")
+let coq_Zneg = lazy (constant "Zneg")
+let coq_Z = lazy (constant "Z")
+let coq_comparison = lazy (constant "comparison")
+let coq_Gt = lazy (constant "Gt")
+let coq_Zplus = lazy (constant "Zplus")
+let coq_Zmult = lazy (constant "Zmult")
+let coq_Zopp = lazy (constant "Zopp")
+let coq_Zminus = lazy (constant "Zminus")
+let coq_Zsucc = lazy (constant "Zsucc")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zle = lazy (constant "Zle")
+let coq_Z_of_nat = lazy (constant "Z_of_nat")
+let coq_inj_plus = lazy (constant "inj_plus")
+let coq_inj_mult = lazy (constant "inj_mult")
+let coq_inj_minus1 = lazy (constant "inj_minus1")
+let coq_inj_minus2 = lazy (constant "inj_minus2")
+let coq_inj_S = lazy (constant "inj_S")
+let coq_inj_le = lazy (constant "inj_le")
+let coq_inj_lt = lazy (constant "inj_lt")
+let coq_inj_ge = lazy (constant "inj_ge")
+let coq_inj_gt = lazy (constant "inj_gt")
+let coq_inj_neq = lazy (constant "inj_neq")
+let coq_inj_eq = lazy (constant "inj_eq")
+let coq_fast_Zplus_assoc_reverse = lazy (constant "fast_Zplus_assoc_reverse")
+let coq_fast_Zplus_assoc = lazy (constant "fast_Zplus_assoc")
+let coq_fast_Zmult_assoc_reverse = lazy (constant "fast_Zmult_assoc_reverse")
+let coq_fast_Zplus_permute = lazy (constant "fast_Zplus_permute")
+let coq_fast_Zplus_comm = lazy (constant "fast_Zplus_comm")
+let coq_fast_Zmult_comm = lazy (constant "fast_Zmult_comm")
+let coq_Zmult_le_approx = lazy (constant "Zmult_le_approx")
+let coq_OMEGA1 = lazy (constant "OMEGA1")
+let coq_OMEGA2 = lazy (constant "OMEGA2")
+let coq_OMEGA3 = lazy (constant "OMEGA3")
+let coq_OMEGA4 = lazy (constant "OMEGA4")
+let coq_OMEGA5 = lazy (constant "OMEGA5")
+let coq_OMEGA6 = lazy (constant "OMEGA6")
+let coq_OMEGA7 = lazy (constant "OMEGA7")
+let coq_OMEGA8 = lazy (constant "OMEGA8")
+let coq_OMEGA9 = lazy (constant "OMEGA9")
+let coq_fast_OMEGA10 = lazy (constant "fast_OMEGA10")
+let coq_fast_OMEGA11 = lazy (constant "fast_OMEGA11")
+let coq_fast_OMEGA12 = lazy (constant "fast_OMEGA12")
+let coq_fast_OMEGA13 = lazy (constant "fast_OMEGA13")
+let coq_fast_OMEGA14 = lazy (constant "fast_OMEGA14")
+let coq_fast_OMEGA15 = lazy (constant "fast_OMEGA15")
+let coq_fast_OMEGA16 = lazy (constant "fast_OMEGA16")
+let coq_OMEGA17 = lazy (constant "OMEGA17")
+let coq_OMEGA18 = lazy (constant "OMEGA18")
+let coq_OMEGA19 = lazy (constant "OMEGA19")
+let coq_OMEGA20 = lazy (constant "OMEGA20")
+let coq_fast_Zred_factor0 = lazy (constant "fast_Zred_factor0")
+let coq_fast_Zred_factor1 = lazy (constant "fast_Zred_factor1")
+let coq_fast_Zred_factor2 = lazy (constant "fast_Zred_factor2")
+let coq_fast_Zred_factor3 = lazy (constant "fast_Zred_factor3")
+let coq_fast_Zred_factor4 = lazy (constant "fast_Zred_factor4")
+let coq_fast_Zred_factor5 = lazy (constant "fast_Zred_factor5")
+let coq_fast_Zred_factor6 = lazy (constant "fast_Zred_factor6")
+let coq_fast_Zmult_plus_distr_l = lazy (constant "fast_Zmult_plus_distr_l")
+let coq_fast_Zmult_opp_comm =  lazy (constant "fast_Zmult_opp_comm")
+let coq_fast_Zopp_plus_distr =   lazy (constant "fast_Zopp_plus_distr")
+let coq_fast_Zopp_mult_distr_r = lazy (constant "fast_Zopp_mult_distr_r")
+let coq_fast_Zopp_eq_mult_neg_1 =  lazy (constant "fast_Zopp_eq_mult_neg_1")
+let coq_fast_Zopp_involutive = lazy (constant "fast_Zopp_involutive")
+let coq_Zegal_left = lazy (constant "Zegal_left")
+let coq_Zne_left = lazy (constant "Zne_left")
+let coq_Zlt_left = lazy (constant "Zlt_left")
+let coq_Zge_left = lazy (constant "Zge_left")
+let coq_Zgt_left = lazy (constant "Zgt_left")
+let coq_Zle_left = lazy (constant "Zle_left")
+let coq_new_var = lazy (constant "new_var")
+let coq_intro_Z = lazy (constant "intro_Z")
+
+let coq_dec_eq = lazy (constant "dec_eq")
+let coq_dec_Zne = lazy (constant "dec_Zne")
+let coq_dec_Zle = lazy (constant "dec_Zle")
+let coq_dec_Zlt = lazy (constant "dec_Zlt")
+let coq_dec_Zgt = lazy (constant "dec_Zgt")
+let coq_dec_Zge = lazy (constant "dec_Zge")
+
+let coq_not_Zeq = lazy (constant "not_Zeq")
+let coq_Znot_le_gt = lazy (constant "Znot_le_gt")
+let coq_Znot_lt_ge = lazy (constant "Znot_lt_ge")
+let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt")
+let coq_Znot_gt_le = lazy (constant "Znot_gt_le")
+let coq_neq = lazy (constant "neq")
+let coq_Zne = lazy (constant "Zne")
+let coq_Zle = lazy (constant "Zle")
+let coq_Zgt = lazy (constant "Zgt")
+let coq_Zge = lazy (constant "Zge")
+let coq_Zlt = lazy (constant "Zlt")
+
+(* Peano/Datatypes *)
+let coq_le = lazy (init_constant "le")
+let coq_lt = lazy (init_constant "lt")
+let coq_ge = lazy (init_constant "ge")
+let coq_gt = lazy (init_constant "gt")
+let coq_minus = lazy (init_constant "minus")
+let coq_plus = lazy (init_constant "plus")
+let coq_mult = lazy (init_constant "mult")
+let coq_pred = lazy (init_constant "pred")
+let coq_nat = lazy (init_constant "nat")
+let coq_S = lazy (init_constant "S")
+let coq_O = lazy (init_constant "O")
+
+(* Compare_dec/Peano_dec/Minus *)
+let coq_pred_of_minus = lazy (constant "pred_of_minus")
+let coq_le_gt_dec = lazy (constant "le_gt_dec")
+let coq_dec_eq_nat = lazy (constant "dec_eq_nat")
+let coq_dec_le = lazy (constant "dec_le")
+let coq_dec_lt = lazy (constant "dec_lt")
+let coq_dec_ge = lazy (constant "dec_ge")
+let coq_dec_gt = lazy (constant "dec_gt")
+let coq_not_eq = lazy (constant "not_eq")
+let coq_not_le = lazy (constant "not_le")
+let coq_not_lt = lazy (constant "not_lt")
+let coq_not_ge = lazy (constant "not_ge")
+let coq_not_gt = lazy (constant "not_gt")
+
+(* Logic/Decidable *)
+let coq_eq_ind_r = lazy (constant "eq_ind_r")
+
+let coq_dec_or = lazy (constant "dec_or")
+let coq_dec_and = lazy (constant "dec_and")
+let coq_dec_imp = lazy (constant "dec_imp")
+let coq_dec_iff = lazy (constant "dec_iff")
+let coq_dec_not = lazy (constant "dec_not")
+let coq_dec_False = lazy (constant "dec_False")
+let coq_dec_not_not = lazy (constant "dec_not_not")
+let coq_dec_True = lazy (constant "dec_True")
+
+let coq_not_or = lazy (constant "not_or")
+let coq_not_and = lazy (constant "not_and")
+let coq_not_imp = lazy (constant "not_imp")
+let coq_not_iff = lazy (constant "not_iff")
+let coq_not_not = lazy (constant "not_not")
+let coq_imp_simp = lazy (constant "imp_simp")
+let coq_iff = lazy (constant "iff")
+
+(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
+
+(* For unfold *)
+open Closure
+let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
+  | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
+      EvalConstRef kn
+  | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant")
+
+let sp_Zsucc =     lazy (evaluable_ref_of_constr "Zsucc" coq_Zsucc)
+let sp_Zminus = lazy (evaluable_ref_of_constr "Zminus" coq_Zminus)
+let sp_Zle = lazy (evaluable_ref_of_constr "Zle" coq_Zle)
+let sp_Zgt = lazy (evaluable_ref_of_constr "Zgt" coq_Zgt)
+let sp_Zge = lazy (evaluable_ref_of_constr "Zge" coq_Zge)
+let sp_Zlt = lazy (evaluable_ref_of_constr "Zlt" coq_Zlt)
+let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ())))
+
+let mk_var v = mkVar (id_of_string v)
+let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
+let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
+let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
+let mk_eq t1 t2 = mkApp (build_coq_eq (), [| Lazy.force coq_Z; t1; t2 |])
+let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
+let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
+let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
+let mk_and t1 t2 =  mkApp (build_coq_and (), [| t1; t2 |])
+let mk_or t1 t2 =  mkApp (build_coq_or (), [| t1; t2 |])
+let mk_not t = mkApp (build_coq_not (), [| t |])
+let mk_eq_rel t1 t2 = mkApp (build_coq_eq (),
+			      [| Lazy.force coq_comparison; t1; t2 |])
+let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
+
+let mk_integer n =
+  let rec loop n =
+    if n =? one then Lazy.force coq_xH else
+    mkApp((if n mod two =? zero then Lazy.force coq_xO else Lazy.force coq_xI),
+		[| loop (n/two) |])
+  in
+  if n =? zero then Lazy.force coq_Z0
+  else mkApp ((if n >? zero then Lazy.force coq_Zpos else Lazy.force coq_Zneg),
+		 [| loop (abs n) |])
+
+type omega_constant =
+  | Zplus | Zmult | Zminus | Zsucc | Zopp
+  | Plus | Mult | Minus | Pred | S | O
+  | Zpos | Zneg | Z0 | Z_of_nat
+  | Eq | Neq
+  | Zne | Zle | Zlt | Zge | Zgt
+  | Z | Nat
+  | And | Or | False | True | Not | Iff
+  | Le | Lt | Ge | Gt
+  | Other of string
+
+type omega_proposition =
+  | Keq of constr * constr * constr
+  | Kn
+
+type result =
+  | Kvar of identifier
+  | Kapp of omega_constant * constr list
+  | Kimp of constr * constr
+  | Kufo
+
+let destructurate_prop t =
+  let c, args = decompose_app t in
+  match kind_of_term c, args with
+    | _, [_;_;_] when c = build_coq_eq () -> Kapp (Eq,args)
+    | _, [_;_] when c = Lazy.force coq_neq -> Kapp (Neq,args)
+    | _, [_;_] when c = Lazy.force coq_Zne -> Kapp (Zne,args)
+    | _, [_;_] when c = Lazy.force coq_Zle -> Kapp (Zle,args)
+    | _, [_;_] when c = Lazy.force coq_Zlt -> Kapp (Zlt,args)
+    | _, [_;_] when c = Lazy.force coq_Zge -> Kapp (Zge,args)
+    | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args)
+    | _, [_;_] when c = build_coq_and () -> Kapp (And,args)
+    | _, [_;_] when c = build_coq_or () -> Kapp (Or,args)
+    | _, [_;_] when c = Lazy.force coq_iff -> Kapp (Iff, args)
+    | _, [_] when c = build_coq_not () -> Kapp (Not,args)
+    | _, [] when c = build_coq_False () -> Kapp (False,args)
+    | _, [] when c = build_coq_True () -> Kapp (True,args)
+    | _, [_;_] when c = Lazy.force coq_le -> Kapp (Le,args)
+    | _, [_;_] when c = Lazy.force coq_lt -> Kapp (Lt,args)
+    | _, [_;_] when c = Lazy.force coq_ge -> Kapp (Ge,args)
+    | _, [_;_] when c = Lazy.force coq_gt -> Kapp (Gt,args)
+    | Const sp, args ->
+	Kapp (Other (string_of_id (basename_of_global (ConstRef sp))),args)
+    | Construct csp , args ->
+	Kapp (Other (string_of_id (basename_of_global (ConstructRef csp))), args)
+    | Ind isp, args ->
+	Kapp (Other (string_of_id (basename_of_global (IndRef isp))),args)
+    | Var id,[] -> Kvar id
+    | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
+    | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
+    | _ -> Kufo
+
+let destructurate_type t =
+  let c, args = decompose_app t in
+  match kind_of_term c, args with
+    | _, [] when c = Lazy.force coq_Z -> Kapp (Z,args)
+    | _, [] when c = Lazy.force coq_nat -> Kapp (Nat,args)
+    | _ -> Kufo
+
+let destructurate_term t =
+  let c, args = decompose_app t in
+  match kind_of_term c, args with
+    | _, [_;_] when c = Lazy.force coq_Zplus -> Kapp (Zplus,args)
+    | _, [_;_] when c = Lazy.force coq_Zmult -> Kapp (Zmult,args)
+    | _, [_;_] when c = Lazy.force coq_Zminus -> Kapp (Zminus,args)
+    | _, [_] when c = Lazy.force coq_Zsucc -> Kapp (Zsucc,args)
+    | _, [_] when c = Lazy.force coq_Zopp -> Kapp (Zopp,args)
+    | _, [_;_] when c = Lazy.force coq_plus -> Kapp (Plus,args)
+    | _, [_;_] when c = Lazy.force coq_mult -> Kapp (Mult,args)
+    | _, [_;_] when c = Lazy.force coq_minus -> Kapp (Minus,args)
+    | _, [_] when c = Lazy.force coq_pred -> Kapp (Pred,args)
+    | _, [_] when c = Lazy.force coq_S -> Kapp (S,args)
+    | _, [] when c = Lazy.force coq_O -> Kapp (O,args)
+    | _, [_] when c = Lazy.force coq_Zpos -> Kapp (Zneg,args)
+    | _, [_] when c = Lazy.force coq_Zneg -> Kapp (Zpos,args)
+    | _, [] when c = Lazy.force coq_Z0 -> Kapp (Z0,args)
+    | _, [_] when c = Lazy.force coq_Z_of_nat -> Kapp (Z_of_nat,args)
+    | Var id,[] -> Kvar id
+    | _ -> Kufo
+
+let recognize_number t =
+  let rec loop t =
+    match decompose_app t with
+      | f, [t] when f = Lazy.force coq_xI -> one + two * loop t
+      | f, [t] when f = Lazy.force coq_xO -> two * loop t
+      | f, [] when f = Lazy.force coq_xH -> one
+      | _ -> failwith "not a number"
+  in
+  match decompose_app t with
+    | f, [t] when f = Lazy.force coq_Zpos -> loop t
+    | f, [t] when f = Lazy.force coq_Zneg -> neg (loop t)
+    | f, [] when f = Lazy.force coq_Z0 -> zero
+    | _ -> failwith "not a number"
+
+type constr_path =
+  | P_APP of int
+  (* Abstraction and product *)
+  | P_BODY
+  | P_TYPE
+  (* Case *)
+  | P_BRANCH of int
+  | P_ARITY
+  | P_ARG
+
+let context operation path (t : constr) =
+  let rec loop i p0 t =
+    match (p0,kind_of_term t) with
+      | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t)
+      | ([], _) -> operation i t
+      | ((P_APP n :: p),  App (f,v)) ->
+	  let v' = Array.copy v in
+	  v'.(pred n) <- loop i p v'.(pred n); mkApp (f, v')
+      | ((P_BRANCH n :: p), Case (ci,q,c,v)) ->
+	  (* avant, y avait mkApp... anyway, BRANCH seems nowhere used *)
+	  let v' = Array.copy v in
+	  v'.(n) <- loop i p v'.(n); (mkCase (ci,q,c,v'))
+      | ((P_ARITY :: p),  App (f,l)) ->
+	  appvect (loop i p f,l)
+      | ((P_ARG :: p),  App (f,v)) ->
+	  let v' = Array.copy v in
+	  v'.(0) <- loop i p v'.(0); mkApp (f,v')
+      | (p, Fix ((_,n as ln),(tys,lna,v))) ->
+	  let l = Array.length v in
+	  let v' = Array.copy v in
+	  v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v')))
+      | ((P_BODY :: p), Prod (n,t,c)) ->
+	  (mkProd (n,t,loop (succ i) p c))
+      | ((P_BODY :: p), Lambda (n,t,c)) ->
+	  (mkLambda (n,t,loop (succ i) p c))
+      | ((P_BODY :: p), LetIn (n,b,t,c)) ->
+	  (mkLetIn (n,b,t,loop (succ i) p c))
+      | ((P_TYPE :: p), Prod (n,t,c)) ->
+	  (mkProd (n,loop i p t,c))
+      | ((P_TYPE :: p), Lambda (n,t,c)) ->
+	  (mkLambda (n,loop i p t,c))
+      | ((P_TYPE :: p), LetIn (n,b,t,c)) ->
+	  (mkLetIn (n,b,loop i p t,c))
+      | (p, _) ->
+	  ppnl (Printer.pr_lconstr t);
+	  failwith ("abstract_path " ^ string_of_int(List.length p))
+  in
+  loop 1 path t
+
+let occurence path (t : constr) =
+  let rec loop p0 t = match (p0,kind_of_term t) with
+    | (p, Cast (c,_,_)) -> loop p c
+    | ([], _) -> t
+    | ((P_APP n :: p),  App (f,v)) -> loop p v.(pred n)
+    | ((P_BRANCH n :: p), Case (_,_,_,v)) -> loop p v.(n)
+    | ((P_ARITY :: p),  App (f,_)) -> loop p f
+    | ((P_ARG :: p),  App (f,v)) -> loop p v.(0)
+    | (p, Fix((_,n) ,(_,_,v))) -> loop p v.(n)
+    | ((P_BODY :: p), Prod (n,t,c)) -> loop p c
+    | ((P_BODY :: p), Lambda (n,t,c)) -> loop p c
+    | ((P_BODY :: p), LetIn (n,b,t,c)) -> loop p c
+    | ((P_TYPE :: p), Prod (n,term,c)) -> loop p term
+    | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
+    | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
+    | (p, _) ->
+	ppnl (Printer.pr_lconstr t);
+	failwith ("occurence " ^ string_of_int(List.length p))
+  in
+  loop path t
+
+let abstract_path typ path t =
+  let term_occur = ref (mkRel 0) in
+  let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in
+  mkLambda (Name (id_of_string "x"), typ, abstract), !term_occur
+
+let focused_simpl path gl =
+  let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
+  convert_concl_no_check newc DEFAULTcast gl
+
+let focused_simpl path = simpl_time (focused_simpl path)
+
+type oformula =
+  | Oplus of oformula * oformula
+  | Oinv of  oformula
+  | Otimes of oformula * oformula
+  | Oatom of identifier
+  | Oz of bigint
+  | Oufo of constr
+
+let rec oprint = function
+  | Oplus(t1,t2) ->
+      print_string "("; oprint t1; print_string "+";
+      oprint t2; print_string ")"
+  | Oinv t -> print_string "~"; oprint t
+  | Otimes (t1,t2) ->
+      print_string "("; oprint t1; print_string "*";
+      oprint t2; print_string ")"
+  | Oatom s -> print_string (string_of_id s)
+  | Oz i -> print_string (string_of_bigint i)
+  | Oufo f -> print_string "?"
+
+let rec weight = function
+  | Oatom c -> intern_id c
+  | Oz _ -> -1
+  | Oinv c -> weight c
+  | Otimes(c,_) -> weight c
+  | Oplus _ -> failwith "weight"
+  | Oufo _ -> -1
+
+let rec val_of = function
+  | Oatom c -> mkVar c
+  | Oz c -> mk_integer c
+  | Oinv c -> mkApp (Lazy.force coq_Zopp, [| val_of c |])
+  | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |])
+  | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |])
+  | Oufo c -> c
+
+let compile name kind =
+  let rec loop accu = function
+    | Oplus(Otimes(Oatom v,Oz n),r) -> loop ({v=intern_id v; c=n} :: accu) r
+    | Oz n ->
+	let id = new_id () in
+	tag_hypothesis name id;
+	{kind = kind; body = List.rev accu; constant = n; id = id}
+    | _ -> anomaly "compile_equation"
+  in
+  loop []
+
+let rec decompile af =
+  let rec loop = function
+    | ({v=v; c=n}::r) -> Oplus(Otimes(Oatom (unintern_id v),Oz n),loop r)
+    | [] -> Oz af.constant
+  in
+  loop af.body
+
+let mkNewMeta () = mkMeta (Evarutil.new_meta())
+
+let clever_rewrite_base_poly typ p result theorem gl =
+  let full = pf_concl gl in
+  let (abstracted,occ) = abstract_path typ (List.rev p) full in
+  let t =
+    applist
+      (mkLambda
+	 (Name (id_of_string "P"),
+	  mkArrow typ mkProp,
+          mkLambda
+	    (Name (id_of_string "H"),
+	     applist (mkRel 1,[result]),
+	     mkApp (Lazy.force coq_eq_ind_r,
+		       [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
+       [abstracted])
+  in
+  exact (applist(t,[mkNewMeta()])) gl
+
+let clever_rewrite_base p result theorem gl =
+  clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl
+
+let clever_rewrite_base_nat p result theorem gl =
+  clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem gl
+
+let clever_rewrite_gen p result (t,args) =
+  let theorem = applist(t, args) in
+  clever_rewrite_base p result theorem
+
+let clever_rewrite_gen_nat p result (t,args) =
+  let theorem = applist(t, args) in
+  clever_rewrite_base_nat p result theorem
+
+let clever_rewrite p vpath t gl =
+  let full = pf_concl gl in
+  let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in
+  let vargs = List.map (fun p -> occurence p occ) vpath in
+  let t' = applist(t, (vargs @ [abstracted])) in
+  exact (applist(t',[mkNewMeta()])) gl
+
+let rec shuffle p (t1,t2) =
+  match t1,t2 with
+    | Oplus(l1,r1), Oplus(l2,r2) ->
+	if weight l1 > weight l2 then
+          let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in
+          (clever_rewrite p [[P_APP 1;P_APP 1];
+			     [P_APP 1; P_APP 2];[P_APP 2]]
+             (Lazy.force coq_fast_Zplus_assoc_reverse)
+           :: tac,
+           Oplus(l1,t'))
+	else
+	  let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in
+          (clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
+             (Lazy.force coq_fast_Zplus_permute)
+           :: tac,
+           Oplus(l2,t'))
+    | Oplus(l1,r1), t2 ->
+	if weight l1 > weight t2 then
+          let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in
+          clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+            (Lazy.force coq_fast_Zplus_assoc_reverse)
+          :: tac,
+          Oplus(l1, t')
+	else
+          [clever_rewrite p [[P_APP 1];[P_APP 2]]
+	     (Lazy.force coq_fast_Zplus_comm)],
+          Oplus(t2,t1)
+    | t1,Oplus(l2,r2) ->
+	if weight l2 > weight t1 then
+          let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in
+          clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
+            (Lazy.force coq_fast_Zplus_permute)
+          :: tac,
+          Oplus(l2,t')
+	else [],Oplus(t1,t2)
+    | Oz t1,Oz t2 ->
+	[focused_simpl p], Oz(Bigint.add t1 t2)
+    | t1,t2 ->
+	if weight t1 < weight t2 then
+          [clever_rewrite p [[P_APP 1];[P_APP 2]]
+	     (Lazy.force coq_fast_Zplus_comm)],
+	  Oplus(t2,t1)
+	else [],Oplus(t1,t2)
+
+let rec shuffle_mult p_init k1 e1 k2 e2 =
+  let rec loop p = function
+    | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
+	if v1 = v2 then
+          let tac =
+            clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+                              [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+                              [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+                              [P_APP 1; P_APP 1; P_APP 2];
+                              [P_APP 2; P_APP 1; P_APP 2];
+                              [P_APP 1; P_APP 2];
+                              [P_APP 2; P_APP 2]]
+              (Lazy.force coq_fast_OMEGA10)
+	  in
+          if Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero then
+            let tac' =
+	      clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
+                (Lazy.force coq_fast_Zred_factor5) in
+	    tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' ::
+	    loop p (l1,l2)
+          else tac :: loop (P_APP 2 :: p) (l1,l2)
+	else if v1 > v2 then
+          clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+                            [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+                            [P_APP 1; P_APP 1; P_APP 2];
+                            [P_APP 2];
+                            [P_APP 1; P_APP 2]]
+            (Lazy.force coq_fast_OMEGA11) ::
+          loop (P_APP 2 :: p) (l1,l2')
+	else
+          clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+                            [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+                            [P_APP 1];
+                            [P_APP 2; P_APP 1; P_APP 2];
+                            [P_APP 2; P_APP 2]]
+            (Lazy.force coq_fast_OMEGA12) ::
+          loop (P_APP 2 :: p) (l1',l2)
+    | ({c=c1;v=v1}::l1), [] ->
+        clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+                          [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+                          [P_APP 1; P_APP 1; P_APP 2];
+                          [P_APP 2];
+                          [P_APP 1; P_APP 2]]
+          (Lazy.force coq_fast_OMEGA11) ::
+        loop (P_APP 2 :: p) (l1,[])
+    | [],({c=c2;v=v2}::l2) ->
+        clever_rewrite p  [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+                           [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+                           [P_APP 1];
+                           [P_APP 2; P_APP 1; P_APP 2];
+                           [P_APP 2; P_APP 2]]
+          (Lazy.force coq_fast_OMEGA12) ::
+        loop (P_APP 2 :: p) ([],l2)
+    | [],[] -> [focused_simpl p_init]
+  in
+  loop p_init (e1,e2)
+
+let rec shuffle_mult_right p_init e1 k2 e2 =
+  let rec loop p = function
+    | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
+	if v1 = v2 then
+          let tac =
+            clever_rewrite p
+              [[P_APP 1; P_APP 1; P_APP 1];
+               [P_APP 1; P_APP 1; P_APP 2];
+               [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+               [P_APP 1; P_APP 2];
+               [P_APP 2; P_APP 1; P_APP 2];
+               [P_APP 2; P_APP 2]]
+              (Lazy.force coq_fast_OMEGA15)
+	  in
+          if Bigint.add c1 (Bigint.mult k2 c2) =? zero then
+            let tac' =
+              clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
+                (Lazy.force coq_fast_Zred_factor5)
+	    in
+            tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' ::
+            loop p (l1,l2)
+          else tac :: loop (P_APP 2 :: p) (l1,l2)
+	else if v1 > v2 then
+          clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+            (Lazy.force coq_fast_Zplus_assoc_reverse) ::
+          loop (P_APP 2 :: p) (l1,l2')
+	else
+          clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+                            [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+                            [P_APP 1];
+                            [P_APP 2; P_APP 1; P_APP 2];
+                            [P_APP 2; P_APP 2]]
+            (Lazy.force coq_fast_OMEGA12) ::
+          loop (P_APP 2 :: p) (l1',l2)
+    | ({c=c1;v=v1}::l1), [] ->
+        clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+          (Lazy.force coq_fast_Zplus_assoc_reverse) ::
+        loop (P_APP 2 :: p) (l1,[])
+    | [],({c=c2;v=v2}::l2) ->
+        clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
+                          [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
+                          [P_APP 1];
+                          [P_APP 2; P_APP 1; P_APP 2];
+                          [P_APP 2; P_APP 2]]
+          (Lazy.force coq_fast_OMEGA12) ::
+        loop (P_APP 2 :: p) ([],l2)
+    | [],[] -> [focused_simpl p_init]
+  in
+  loop p_init (e1,e2)
+
+let rec shuffle_cancel p = function
+  | [] -> [focused_simpl p]
+  | ({c=c1}::l1) ->
+      let tac =
+	clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 2];
+                          [P_APP 2; P_APP 2];
+                          [P_APP 1; P_APP 1; P_APP 2; P_APP 1]]
+          (if c1 >? zero then
+	     (Lazy.force coq_fast_OMEGA13)
+	   else
+	     (Lazy.force coq_fast_OMEGA14))
+      in
+      tac :: shuffle_cancel p l1
+
+let rec scalar p n = function
+  | Oplus(t1,t2) ->
+      let tac1,t1' = scalar (P_APP 1 :: p) n t1 and
+        tac2,t2' = scalar (P_APP 2 :: p) n t2 in
+      clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
+        (Lazy.force coq_fast_Zmult_plus_distr_l) ::
+      (tac1 @ tac2), Oplus(t1',t2')
+  | Oinv t ->
+      [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
+	 (Lazy.force coq_fast_Zmult_opp_comm);
+       focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(neg n))
+  | Otimes(t1,Oz x) ->
+      [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
+         (Lazy.force coq_fast_Zmult_assoc_reverse);
+       focused_simpl (P_APP 2 :: p)],
+      Otimes(t1,Oz (n*x))
+  | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
+  | (Oatom _ as t) -> [], Otimes(t,Oz n)
+  | Oz i -> [focused_simpl p],Oz(n*i)
+  | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |]))
+
+let rec scalar_norm p_init =
+  let rec loop p = function
+    | [] -> [focused_simpl p_init]
+    | (_::l) ->
+	clever_rewrite p
+          [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2];
+           [P_APP 1; P_APP 2];[P_APP 2]]
+          (Lazy.force coq_fast_OMEGA16) :: loop (P_APP 2 :: p) l
+  in
+  loop p_init
+
+let rec norm_add p_init =
+  let rec loop p = function
+    | [] -> [focused_simpl p_init]
+    | _:: l ->
+	clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
+          (Lazy.force coq_fast_Zplus_assoc_reverse) ::
+	loop (P_APP 2 :: p) l
+  in
+  loop p_init
+
+let rec scalar_norm_add p_init =
+  let rec loop p = function
+    | [] -> [focused_simpl p_init]
+    | _ :: l ->
+	clever_rewrite p
+          [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
+           [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
+           [P_APP 1; P_APP 1; P_APP 2]; [P_APP 2]; [P_APP 1; P_APP 2]]
+          (Lazy.force coq_fast_OMEGA11) :: loop (P_APP 2 :: p) l
+  in
+  loop p_init
+
+let rec negate p = function
+  | Oplus(t1,t2) ->
+      let tac1,t1' = negate (P_APP 1 :: p) t1 and
+        tac2,t2' = negate (P_APP 2 :: p) t2 in
+      clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
+        (Lazy.force coq_fast_Zopp_plus_distr) ::
+      (tac1 @ tac2),
+      Oplus(t1',t2')
+  | Oinv t ->
+      [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_involutive)], t
+  | Otimes(t1,Oz x) ->
+      [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
+         (Lazy.force coq_fast_Zopp_mult_distr_r);
+       focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x))
+  | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
+  | (Oatom _ as t) ->
+      let r = Otimes(t,Oz(negone)) in
+      [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r
+  | Oz i -> [focused_simpl p],Oz(neg i)
+  | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |]))
+
+let rec transform p t =
+  let default isnat t' =
+    try
+      let v,th,_ = find_constr t' in
+      [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
+    with _ ->
+      let v = new_identifier_var ()
+      and th = new_identifier () in
+      hide_constr t' v th isnat;
+      [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
+  in
+  try match destructurate_term t with
+    | Kapp(Zplus,[t1;t2]) ->
+	let tac1,t1' = transform (P_APP 1 :: p) t1
+	and tac2,t2' = transform (P_APP 2 :: p) t2 in
+	let tac,t' = shuffle p (t1',t2') in
+	tac1 @ tac2 @ tac, t'
+    | Kapp(Zminus,[t1;t2]) ->
+	let tac,t =
+	  transform p
+	    (mkApp (Lazy.force coq_Zplus,
+		     [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
+	unfold sp_Zminus :: tac,t
+    | Kapp(Zsucc,[t1]) ->
+	let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
+					 [| t1; mk_integer one |])) in
+	unfold sp_Zsucc :: tac,t
+   | Kapp(Zmult,[t1;t2]) ->
+       let tac1,t1' = transform (P_APP 1 :: p) t1
+       and tac2,t2' = transform (P_APP 2 :: p) t2 in
+       begin match t1',t2' with
+         | (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t'
+         | (Oz n,_) ->
+             let sym =
+	       clever_rewrite p [[P_APP 1];[P_APP 2]]
+		 (Lazy.force coq_fast_Zmult_comm) in
+             let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t'
+         | _ -> default false t
+       end
+   | Kapp((Zpos|Zneg|Z0),_) ->
+       (try ([],Oz(recognize_number t)) with _ -> default false t)
+   | Kvar s -> [],Oatom s
+   | Kapp(Zopp,[t]) ->
+       let tac,t' = transform (P_APP 1 :: p) t in
+       let tac',t'' = negate p t' in
+       tac @ tac', t''
+   | Kapp(Z_of_nat,[t']) -> default true t'
+   | _ -> default false t
+  with e when catchable_exception e -> default false t
+
+let shrink_pair p f1 f2 =
+  match f1,f2 with
+    | Oatom v,Oatom _ ->
+	let r = Otimes(Oatom v,Oz two) in
+	clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zred_factor1), r
+    | Oatom v, Otimes(_,c2) ->
+	let r = Otimes(Oatom v,Oplus(c2,Oz one)) in
+	clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 2]]
+	  (Lazy.force coq_fast_Zred_factor2), r
+    | Otimes (v1,c1),Oatom v ->
+	let r = Otimes(Oatom v,Oplus(c1,Oz one)) in
+	clever_rewrite p [[P_APP 2];[P_APP 1;P_APP 2]]
+          (Lazy.force coq_fast_Zred_factor3), r
+    | Otimes (Oatom v,c1),Otimes (v2,c2) ->
+	let r = Otimes(Oatom v,Oplus(c1,c2)) in
+	clever_rewrite p
+          [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2;P_APP 2]]
+          (Lazy.force coq_fast_Zred_factor4),r
+    | t1,t2 ->
+	begin
+	  oprint t1; print_newline (); oprint t2; print_newline ();
+	  flush Pervasives.stdout; error "shrink.1"
+	end
+
+let reduce_factor p = function
+  | Oatom v ->
+      let r = Otimes(Oatom v,Oz one) in
+      [clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor0)],r
+  | Otimes(Oatom v,Oz n) as f -> [],f
+  | Otimes(Oatom v,c) ->
+      let rec compute = function
+        | Oz n -> n
+	| Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2)
+	| _ -> error "condense.1"
+      in
+      [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c))
+  | t -> oprint t; error "reduce_factor.1"
+
+let rec condense p = function
+  | Oplus(f1,(Oplus(f2,r) as t)) ->
+      if weight f1 = weight f2 then begin
+	let shrink_tac,t = shrink_pair (P_APP 1 :: p) f1 f2 in
+	let assoc_tac =
+          clever_rewrite p
+            [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
+            (Lazy.force coq_fast_Zplus_assoc) in
+	let tac_list,t' = condense p (Oplus(t,r)) in
+	(assoc_tac :: shrink_tac :: tac_list), t'
+      end else begin
+	let tac,f = reduce_factor (P_APP 1 :: p) f1 in
+	let tac',t' = condense (P_APP 2 :: p) t in
+	(tac @ tac'), Oplus(f,t')
+      end
+  | Oplus(f1,Oz n) ->
+      let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n)
+  | Oplus(f1,f2) ->
+      if weight f1 = weight f2 then begin
+	let tac_shrink,t = shrink_pair p f1 f2 in
+	let tac,t' = condense p t in
+	tac_shrink :: tac,t'
+      end else begin
+	let tac,f = reduce_factor (P_APP 1 :: p) f1 in
+	let tac',t' = condense (P_APP 2 :: p) f2 in
+	(tac @ tac'),Oplus(f,t')
+      end
+  | Oz _ as t -> [],t
+  | t ->
+      let tac,t' = reduce_factor p t in
+      let final = Oplus(t',Oz zero) in
+      let tac' = clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor6) in
+      tac @ [tac'], final
+
+let rec clear_zero p = function
+  | Oplus(Otimes(Oatom v,Oz n),r) when n =? zero ->
+      let tac =
+	clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
+	  (Lazy.force coq_fast_Zred_factor5) in
+      let tac',t = clear_zero p r in
+      tac :: tac',t
+  | Oplus(f,r) ->
+      let tac,t = clear_zero (P_APP 2 :: p) r in tac,Oplus(f,t)
+  | t -> [],t
+
+let replay_history tactic_normalisation =
+  let aux  = id_of_string "auxiliary" in
+  let aux1 = id_of_string "auxiliary_1" in
+  let aux2 = id_of_string "auxiliary_2" in
+  let izero = mk_integer zero in
+  let rec loop t =
+    match t with
+      | HYP e :: l ->
+	  begin
+	    try
+	      tclTHEN
+		(List.assoc (hyp_of_tag e.id) tactic_normalisation)
+		(loop l)
+	    with Not_found -> loop l end
+      | NEGATE_CONTRADICT (e2,e1,b) :: l ->
+	  let eq1 = decompile e1
+	  and eq2 = decompile e2 in
+	  let id1 = hyp_of_tag e1.id
+	  and id2 = hyp_of_tag e2.id in
+	  let k = if b then negone else one in
+	  let p_initial = [P_APP 1;P_TYPE] in
+	  let tac= shuffle_mult_right p_initial e1.body k e2.body in
+	  tclTHENLIST [
+	    (generalize_tac
+	      [mkApp (Lazy.force coq_OMEGA17, [|
+		val_of eq1;
+		val_of eq2;
+		mk_integer k;
+		mkVar id1; mkVar id2 |])]);
+	    (mk_then tac);
+	    (intros_using [aux]);
+	    (resolve_id aux);
+            reflexivity
+          ]
+      | CONTRADICTION (e1,e2) :: l ->
+	  let eq1 = decompile e1
+	  and eq2 = decompile e2 in
+	  let p_initial = [P_APP 2;P_TYPE] in
+	  let tac = shuffle_cancel p_initial e1.body in
+	  let solve_le =
+            let not_sup_sup = mkApp (build_coq_eq (), [|
+					Lazy.force coq_comparison;
+					Lazy.force coq_Gt;
+					Lazy.force coq_Gt |])
+	    in
+            tclTHENS
+	      (tclTHENLIST [
+		(unfold sp_Zle);
+		(simpl_in_concl);
+		intro;
+		(absurd not_sup_sup) ])
+	      [ assumption ; reflexivity ]
+	  in
+	  let theorem =
+            mkApp (Lazy.force coq_OMEGA2, [|
+		      val_of eq1; val_of eq2;
+		      mkVar (hyp_of_tag e1.id);
+		      mkVar (hyp_of_tag e2.id) |])
+	  in
+	  tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) (solve_le)
+      | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
+	  let id = hyp_of_tag e1.id in
+	  let eq1 = val_of(decompile e1)
+	  and eq2 = val_of(decompile e2) in
+	  let kk = mk_integer k
+	  and dd = mk_integer d in
+	  let rhs = mk_plus (mk_times eq2 kk) dd in
+	  let state_eg = mk_eq eq1 rhs in
+	  let tac = scalar_norm_add [P_APP 3] e2.body in
+	  tclTHENS
+	    (cut state_eg)
+	    [ tclTHENS
+	        (tclTHENLIST [
+		  (intros_using [aux]);
+		  (generalize_tac
+		    [mkApp (Lazy.force coq_OMEGA1,
+		      [| eq1; rhs; mkVar aux; mkVar id |])]);
+		  (clear [aux;id]);
+		  (intros_using [id]);
+		  (cut (mk_gt kk dd)) ])
+	        [ tclTHENS
+		    (cut (mk_gt kk izero))
+		    [ tclTHENLIST [
+		        (intros_using [aux1; aux2]);
+		        (generalize_tac
+			  [mkApp (Lazy.force coq_Zmult_le_approx,
+			    [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]);
+		        (clear [aux1;aux2;id]);
+		        (intros_using [id]);
+		        (loop l) ];
+		      tclTHENLIST [
+			(unfold sp_Zgt);
+			(simpl_in_concl);
+			reflexivity ] ];
+		  tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; reflexivity ]
+                ];
+	      tclTHEN (mk_then tac) reflexivity ]
+
+      | NOT_EXACT_DIVIDE (e1,k) :: l ->
+	  let c = floor_div e1.constant k in
+	  let d = Bigint.sub e1.constant (Bigint.mult c k) in
+	  let e2 =  {id=e1.id; kind=EQUA;constant = c;
+                     body = map_eq_linear (fun c -> c / k) e1.body } in
+	  let eq2 = val_of(decompile e2) in
+	  let kk = mk_integer k
+	  and dd = mk_integer d in
+	  let tac = scalar_norm_add [P_APP 2] e2.body in
+	  tclTHENS
+	    (cut (mk_gt dd izero))
+	    [ tclTHENS (cut (mk_gt kk dd))
+		[tclTHENLIST [
+		  (intros_using [aux2;aux1]);
+		  (generalize_tac
+		    [mkApp (Lazy.force coq_OMEGA4,
+                      [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
+		  (clear [aux1;aux2]);
+		  (unfold sp_not);
+		  (intros_using [aux]);
+		  (resolve_id aux);
+		  (mk_then tac);
+		  assumption ] ;
+		 tclTHENLIST [
+		   (unfold sp_Zgt);
+		   simpl_in_concl;
+		   reflexivity ] ];
+              tclTHENLIST [
+		(unfold sp_Zgt);
+                simpl_in_concl;
+		reflexivity ] ]
+      | EXACT_DIVIDE (e1,k) :: l ->
+	  let id = hyp_of_tag e1.id in
+	  let e2 =  map_eq_afine (fun c -> c / k) e1 in
+	  let eq1 = val_of(decompile e1)
+	  and eq2 = val_of(decompile e2) in
+	  let kk = mk_integer k in
+	  let state_eq = mk_eq eq1 (mk_times eq2 kk) in
+	  if e1.kind = DISE then
+            let tac = scalar_norm [P_APP 3] e2.body in
+            tclTHENS
+	      (cut state_eq)
+	      [tclTHENLIST [
+		(intros_using [aux1]);
+		(generalize_tac
+		  [mkApp (Lazy.force coq_OMEGA18,
+                    [| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
+		(clear [aux1;id]);
+		(intros_using [id]);
+		(loop l) ];
+	       tclTHEN (mk_then tac) reflexivity ]
+	  else
+            let tac = scalar_norm [P_APP 3] e2.body in
+            tclTHENS (cut state_eq)
+	      [
+		tclTHENS
+		 (cut (mk_gt kk izero))
+		 [tclTHENLIST [
+		   (intros_using [aux2;aux1]);
+		   (generalize_tac
+		     [mkApp (Lazy.force coq_OMEGA3,
+		       [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
+		   (clear [aux1;aux2;id]);
+		   (intros_using [id]);
+		   (loop l) ];
+		  tclTHENLIST [
+		    (unfold sp_Zgt);
+                    simpl_in_concl;
+		    reflexivity ] ];
+		tclTHEN (mk_then tac) reflexivity ]
+      | (MERGE_EQ(e3,e1,e2)) :: l ->
+	  let id = new_identifier () in
+	  tag_hypothesis id e3;
+	  let id1 = hyp_of_tag e1.id
+	  and id2 = hyp_of_tag e2 in
+	  let eq1 = val_of(decompile e1)
+	  and eq2 = val_of (decompile (negate_eq e1)) in
+	  let tac =
+	    clever_rewrite [P_APP 3] [[P_APP 1]]
+	      (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
+            scalar_norm [P_APP 3] e1.body
+	  in
+	  tclTHENS
+	    (cut (mk_eq eq1 (mk_inv eq2)))
+	    [tclTHENLIST [
+	      (intros_using [aux]);
+	      (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
+	        [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
+	      (clear [id1;id2;aux]);
+	      (intros_using [id]);
+	      (loop l) ];
+            tclTHEN (mk_then tac) reflexivity]
+
+      | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l ->
+	  let id = new_identifier ()
+	  and id2 = hyp_of_tag orig.id in
+	  tag_hypothesis id e.id;
+	  let eq1 = val_of(decompile def)
+	  and eq2 = val_of(decompile orig) in
+	  let vid = unintern_id v in
+	  let theorem =
+            mkApp (build_coq_ex (), [|
+		      Lazy.force coq_Z;
+		      mkLambda
+			(Name vid,
+			 Lazy.force coq_Z,
+			 mk_eq (mkRel 1) eq1) |])
+	  in
+	  let mm = mk_integer m in
+	  let p_initial = [P_APP 2;P_TYPE] in
+	  let tac =
+            clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial)
+              [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
+            shuffle_mult_right p_initial
+              orig.body m ({c= negone;v= v}::def.body) in
+	  tclTHENS
+	    (cut theorem)
+	    [tclTHENLIST [
+	      (intros_using [aux]);
+	      (elim_id aux);
+	      (clear [aux]);
+	      (intros_using [vid; aux]);
+	      (generalize_tac
+		[mkApp (Lazy.force coq_OMEGA9,
+		  [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
+	      (mk_then tac);
+	      (clear [aux]);
+	      (intros_using [id]);
+	      (loop l) ];
+            tclTHEN (exists_tac eq1) reflexivity ]
+      | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
+	  let id1 = new_identifier ()
+	  and id2 = new_identifier () in
+	  tag_hypothesis id1 e1; tag_hypothesis id2 e2;
+	  let id = hyp_of_tag e.id in
+	  let tac1 = norm_add [P_APP 2;P_TYPE] e.body in
+	  let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in
+	  let eq = val_of(decompile e) in
+	  tclTHENS
+	    (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))
+	    [tclTHENLIST [ (mk_then tac1); (intros_using [id1]); (loop act1) ];
+             tclTHENLIST [ (mk_then tac2); (intros_using [id2]); (loop act2) ]]
+      | SUM(e3,(k1,e1),(k2,e2)) :: l ->
+	  let id = new_identifier () in
+	  tag_hypothesis id e3;
+	  let id1 = hyp_of_tag e1.id
+	  and id2 = hyp_of_tag e2.id in
+	  let eq1 = val_of(decompile e1)
+	  and eq2 = val_of(decompile e2) in
+	  if k1 =? one & e2.kind = EQUA then
+            let tac_thm =
+              match e1.kind with
+		| EQUA -> Lazy.force coq_OMEGA5
+		| INEQ -> Lazy.force coq_OMEGA6
+		| DISE -> Lazy.force coq_OMEGA20
+	    in
+            let kk = mk_integer k2 in
+            let p_initial =
+              if e1.kind=DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
+            let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
+            tclTHENLIST [
+	      (generalize_tac
+                [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
+	      (mk_then tac);
+	      (intros_using [id]);
+	      (loop l)
+            ]
+	  else
+            let kk1 = mk_integer k1
+	    and kk2 = mk_integer k2 in
+	    let p_initial = [P_APP 2;P_TYPE] in
+	    let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in
+            tclTHENS (cut (mk_gt kk1 izero))
+	      [tclTHENS
+		 (cut (mk_gt kk2 izero))
+		 [tclTHENLIST [
+		   (intros_using [aux2;aux1]);
+		   (generalize_tac
+		     [mkApp (Lazy.force coq_OMEGA7, [|
+		       eq1;eq2;kk1;kk2;
+		       mkVar aux1;mkVar aux2;
+		       mkVar id1;mkVar id2 |])]);
+		   (clear [aux1;aux2]);
+		   (mk_then tac);
+		   (intros_using [id]);
+		   (loop l) ];
+		 tclTHENLIST [
+		   (unfold sp_Zgt);
+                   simpl_in_concl;
+		   reflexivity ] ];
+	      tclTHENLIST [
+		(unfold sp_Zgt);
+                simpl_in_concl;
+		reflexivity ] ]
+      | CONSTANT_NOT_NUL(e,k) :: l ->
+	  tclTHEN (generalize_tac [mkVar (hyp_of_tag e)]) Equality.discrConcl
+      | CONSTANT_NUL(e) :: l ->
+	  tclTHEN (resolve_id (hyp_of_tag e)) reflexivity
+      | CONSTANT_NEG(e,k) :: l ->
+	  tclTHENLIST [
+	    (generalize_tac [mkVar (hyp_of_tag e)]);
+            (unfold sp_Zle);
+	    simpl_in_concl;
+	    (unfold sp_not);
+	    (intros_using [aux]);
+	    (resolve_id aux);
+	    reflexivity
+          ]
+      | _ -> tclIDTAC
+  in
+  loop
+
+let normalize p_initial t =
+  let (tac,t') = transform p_initial t in
+  let (tac',t'') = condense p_initial t' in
+  let (tac'',t''') = clear_zero p_initial t'' in
+  tac @ tac' @ tac'' , t'''
+
+let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
+  let p_initial = [P_APP pos ;P_TYPE] in
+  let (tac,t') = normalize p_initial t in
+  let shift_left =
+    tclTHEN
+      (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
+      (tclTRY (clear [id]))
+  in
+  if tac <> [] then
+    let id' = new_identifier () in
+    ((id',(tclTHENLIST [ (shift_left); (mk_then tac); (intros_using [id']) ]))
+          :: tactic,
+     compile id' flag t' :: defs)
+  else
+    (tactic,defs)
+
+let destructure_omega gl tac_def (id,c) =
+  if atompart_of_id id = "State" then
+    tac_def
+  else
+    try match destructurate_prop c with
+      | Kapp(Eq,[typ;t1;t2])
+	when destructurate_type (pf_nf gl typ) = Kapp(Z,[]) ->
+	  let t = mk_plus t1 (mk_inv t2) in
+	  normalize_equation
+	    id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
+      | Kapp(Zne,[t1;t2]) ->
+	  let t = mk_plus t1 (mk_inv t2) in
+	  normalize_equation
+	    id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def
+      | Kapp(Zle,[t1;t2]) ->
+	  let t = mk_plus t2 (mk_inv t1) in
+	  normalize_equation
+	    id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def
+      | Kapp(Zlt,[t1;t2]) ->
+	  let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in
+	  normalize_equation
+	    id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def
+      | Kapp(Zge,[t1;t2]) ->
+	  let t = mk_plus t1 (mk_inv t2) in
+	  normalize_equation
+	    id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def
+      | Kapp(Zgt,[t1;t2]) ->
+	  let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in
+	  normalize_equation
+	    id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def
+      | _ -> tac_def
+    with e when catchable_exception e -> tac_def
+
+let reintroduce id =
+  (* [id] cannot be cleared if dependent: protect it by a try *)
+  tclTHEN (tclTRY (clear [id])) (intro_using id)
+
+let coq_omega gl =
+  clear_tables ();
+  let tactic_normalisation, system =
+    List.fold_left (destructure_omega gl) ([],[]) (pf_hyps_types gl) in
+  let prelude,sys =
+    List.fold_left
+      (fun (tac,sys) (t,(v,th,b)) ->
+	 if b then
+           let id = new_identifier () in
+           let i = new_id () in
+           tag_hypothesis id i;
+           (tclTHENLIST [
+	     (simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
+	     (intros_using [v; id]);
+	     (elim_id id);
+	     (clear [id]);
+	     (intros_using [th;id]);
+	     tac ]),
+           {kind = INEQ;
+	    body = [{v=intern_id v; c=one}];
+            constant = zero; id = i} :: sys
+	 else
+           (tclTHENLIST [
+	     (simplest_elim (applist (Lazy.force coq_new_var, [t])));
+	     (intros_using [v;th]);
+	     tac ]),
+           sys)
+      (tclIDTAC,[]) (dump_tables ())
+  in
+  let system = system @ sys in
+  if !display_system_flag then display_system display_var system;
+  if !old_style_flag then begin
+    try
+      let _ = simplify (new_id,new_var_num,display_var) false system in
+      tclIDTAC gl
+    with UNSOLVABLE ->
+      let _,path = depend [] [] (history ()) in
+      if !display_action_flag then display_action display_var path;
+      (tclTHEN prelude (replay_history tactic_normalisation path)) gl
+  end else begin
+    try
+      let path = simplify_strong (new_id,new_var_num,display_var) system in
+      if !display_action_flag then display_action display_var path;
+      (tclTHEN prelude (replay_history tactic_normalisation path)) gl
+    with NO_CONTRADICTION -> error "Omega can't solve this system"
+  end
+
+let coq_omega = solver_time coq_omega
+
+let nat_inject gl =
+  let rec explore p t =
+    try match destructurate_term t with
+      | Kapp(Plus,[t1;t2]) ->
+          tclTHENLIST [
+	    (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
+              ((Lazy.force coq_inj_plus),[t1;t2]));
+	    (explore (P_APP 1 :: p) t1);
+	    (explore (P_APP 2 :: p) t2)
+          ]
+      | Kapp(Mult,[t1;t2]) ->
+          tclTHENLIST [
+	    (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
+              ((Lazy.force coq_inj_mult),[t1;t2]));
+	    (explore (P_APP 1 :: p) t1);
+	    (explore (P_APP 2 :: p) t2)
+          ]
+      | Kapp(Minus,[t1;t2]) ->
+          let id = new_identifier () in
+          tclTHENS
+            (tclTHEN
+	       (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1])))
+	       (intros_using [id]))
+	    [
+	      tclTHENLIST [
+	        (clever_rewrite_gen p
+		  (mk_minus (mk_inj t1) (mk_inj t2))
+                  ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id]));
+		(loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]);
+		(explore (P_APP 1 :: p) t1);
+		(explore (P_APP 2 :: p) t2) ];
+	      (tclTHEN
+		 (clever_rewrite_gen p (mk_integer zero)
+                    ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))
+		 (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])]))
+	    ]
+      | Kapp(S,[t']) ->
+          let rec is_number t =
+            try match destructurate_term t with
+		Kapp(S,[t]) -> is_number t
+              | Kapp(O,[]) -> true
+              | _ -> false
+            with e when catchable_exception e -> false
+	  in
+          let rec loop p t =
+            try match destructurate_term t with
+		Kapp(S,[t]) ->
+                  (tclTHEN
+                     (clever_rewrite_gen p
+			(mkApp (Lazy.force coq_Zsucc, [| mk_inj t |]))
+			((Lazy.force coq_inj_S),[t]))
+		     (loop (P_APP 1 :: p) t))
+              | _ -> explore p t
+            with e when catchable_exception e -> explore p t
+	  in
+          if is_number t' then focused_simpl p else loop p t
+      | Kapp(Pred,[t]) ->
+          let t_minus_one =
+	    mkApp (Lazy.force coq_minus, [| t;
+		      mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in
+          tclTHEN
+            (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one
+               ((Lazy.force coq_pred_of_minus),[t]))
+            (explore p t_minus_one)
+      | Kapp(O,[]) -> focused_simpl p
+      | _ -> tclIDTAC
+    with e when catchable_exception e -> tclIDTAC
+
+  and loop = function
+    | [] -> tclIDTAC
+    | (i,t)::lit ->
+	  begin try match destructurate_prop t with
+              Kapp(Le,[t1;t2]) ->
+		tclTHENLIST [
+		  (generalize_tac
+		    [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
+		  (explore [P_APP 1; P_TYPE] t1);
+		  (explore [P_APP 2; P_TYPE] t2);
+		  (reintroduce i);
+		  (loop lit)
+                ]
+            | Kapp(Lt,[t1;t2]) ->
+		tclTHENLIST [
+		  (generalize_tac
+		    [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
+		  (explore [P_APP 1; P_TYPE] t1);
+		  (explore [P_APP 2; P_TYPE] t2);
+		  (reintroduce i);
+		  (loop lit)
+                ]
+            | Kapp(Ge,[t1;t2]) ->
+		tclTHENLIST [
+		  (generalize_tac
+		    [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
+		  (explore [P_APP 1; P_TYPE] t1);
+		  (explore [P_APP 2; P_TYPE] t2);
+		  (reintroduce i);
+		  (loop lit)
+                ]
+            | Kapp(Gt,[t1;t2]) ->
+		tclTHENLIST [
+		  (generalize_tac
+                    [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
+		  (explore [P_APP 1; P_TYPE] t1);
+		  (explore [P_APP 2; P_TYPE] t2);
+		  (reintroduce i);
+		  (loop lit)
+                ]
+            | Kapp(Neq,[t1;t2]) ->
+		tclTHENLIST [
+		  (generalize_tac
+		    [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
+		  (explore [P_APP 1; P_TYPE] t1);
+		  (explore [P_APP 2; P_TYPE] t2);
+		  (reintroduce i);
+		  (loop lit)
+                ]
+            | Kapp(Eq,[typ;t1;t2]) ->
+		if pf_conv_x gl typ (Lazy.force coq_nat) then
+                  tclTHENLIST [
+		    (generalize_tac
+		      [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
+		    (explore [P_APP 2; P_TYPE] t1);
+		    (explore [P_APP 3; P_TYPE] t2);
+		    (reintroduce i);
+		    (loop lit)
+                  ]
+		else loop lit
+	    | _ -> loop lit
+	  with e when catchable_exception e -> loop lit end
+  in
+  loop (List.rev (pf_hyps_types gl)) gl
+
+let rec decidability gl t =
+  match destructurate_prop t with
+    | Kapp(Or,[t1;t2]) ->
+	mkApp (Lazy.force coq_dec_or, [| t1; t2;
+		  decidability gl t1; decidability gl t2 |])
+    | Kapp(And,[t1;t2]) ->
+	mkApp (Lazy.force coq_dec_and, [| t1; t2;
+		  decidability gl t1; decidability gl t2 |])
+    | Kapp(Iff,[t1;t2]) ->
+	mkApp (Lazy.force coq_dec_iff, [| t1; t2;
+		  decidability gl t1; decidability gl t2 |])
+    | Kimp(t1,t2) ->
+	mkApp (Lazy.force coq_dec_imp, [| t1; t2;
+		  decidability gl t1; decidability gl t2 |])
+    | Kapp(Not,[t1]) -> mkApp (Lazy.force coq_dec_not, [| t1;
+				    decidability gl t1 |])
+    | Kapp(Eq,[typ;t1;t2]) ->
+	begin match destructurate_type (pf_nf gl typ) with
+          | Kapp(Z,[]) ->  mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
+          | Kapp(Nat,[]) ->  mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
+          | _ -> errorlabstrm "decidability"
+		(str "Omega: Can't solve a goal with equality on " ++
+		   Printer.pr_lconstr typ)
+	end
+    | Kapp(Zne,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |])
+    | Kapp(Zle,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zle, [| t1;t2 |])
+    | Kapp(Zlt,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zlt, [| t1;t2 |])
+    | Kapp(Zge,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zge, [| t1;t2 |])
+    | Kapp(Zgt,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zgt, [| t1;t2 |])
+    | Kapp(Le, [t1;t2]) -> mkApp (Lazy.force coq_dec_le, [| t1;t2 |])
+    | Kapp(Lt, [t1;t2]) -> mkApp (Lazy.force coq_dec_lt, [| t1;t2 |])
+    | Kapp(Ge, [t1;t2]) -> mkApp (Lazy.force coq_dec_ge, [| t1;t2 |])
+    | Kapp(Gt, [t1;t2]) -> mkApp (Lazy.force coq_dec_gt, [| t1;t2 |])
+    | Kapp(False,[]) -> Lazy.force coq_dec_False
+    | Kapp(True,[]) -> Lazy.force coq_dec_True
+    | Kapp(Other t,_::_) -> error
+	("Omega: Unrecognized predicate or connective: "^t)
+    | Kapp(Other t,[]) -> error ("Omega: Unrecognized atomic proposition: "^t)
+    | Kvar _ -> error "Omega: Can't solve a goal with proposition variables"
+    | _ -> error "Omega: Unrecognized proposition"
+
+let onClearedName id tac =
+  (* We cannot ensure that hyps can be cleared (because of dependencies), *)
+  (* so renaming may be necessary *)
+  tclTHEN
+    (tclTRY (clear [id]))
+    (fun gl ->
+      let id = fresh_id [] id gl in
+      tclTHEN (introduction id) (tac id) gl)
+
+let destructure_hyps gl =
+  let rec loop = function
+    | [] -> (tclTHEN nat_inject coq_omega)
+    | (i,body,t)::lit ->
+	begin try match destructurate_prop t with
+	  | Kapp(False,[]) -> elim_id i
+          | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
+          | Kapp(Or,[t1;t2]) ->
+              (tclTHENS
+                (elim_id i)
+                [ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
+                  onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
+          | Kapp(And,[t1;t2]) ->
+              tclTHENLIST [
+                (elim_id i);
+		(tclTRY (clear [i]));
+		(fun gl ->
+		  let i1 = fresh_id [] (add_suffix i "_left") gl in
+		  let i2 = fresh_id [] (add_suffix i "_right") gl in
+		  tclTHENLIST [
+		    (introduction i1);
+		    (introduction i2);
+		    (loop ((i1,None,t1)::(i2,None,t2)::lit)) ] gl)
+	      ]
+          | Kapp(Iff,[t1;t2]) ->
+              tclTHENLIST [
+                (elim_id i);
+		(tclTRY (clear [i]));
+		(fun gl ->
+		  let i1 = fresh_id [] (add_suffix i "_left") gl in
+		  let i2 = fresh_id [] (add_suffix i "_right") gl in
+		  tclTHENLIST [
+		    introduction i1;
+		    generalize_tac
+		      [mkApp (Lazy.force coq_imp_simp,
+                        [| t1; t2; decidability gl t1; mkVar i1|])];
+		    onClearedName i1 (fun i1 ->
+		      tclTHENLIST [
+			introduction i2;
+			generalize_tac
+			  [mkApp (Lazy.force coq_imp_simp,
+                            [| t2; t1; decidability gl t2; mkVar i2|])];
+			onClearedName i2 (fun i2 ->
+			  loop
+			  ((i1,None,mk_or (mk_not t1) t2)::
+			   (i2,None,mk_or (mk_not t2) t1)::lit))
+		      ])] gl)
+	      ]
+          | Kimp(t1,t2) ->
+              if
+                is_Prop (pf_type_of gl t1) &
+                is_Prop (pf_type_of gl t2) &
+                closed0 t2
+              then
+		tclTHENLIST [
+		  (generalize_tac [mkApp (Lazy.force coq_imp_simp,
+                    [| t1; t2; decidability gl t1; mkVar i|])]);
+		  (onClearedName i (fun i ->
+		    (loop ((i,None,mk_or (mk_not t1) t2)::lit))))
+                ]
+              else
+		loop lit
+          | Kapp(Not,[t]) ->
+              begin match destructurate_prop t with
+		  Kapp(Or,[t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
+		      (onClearedName i (fun i ->
+                        (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
+                    ]
+		| Kapp(And,[t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+		        [mkApp (Lazy.force coq_not_and, [| t1; t2;
+			  decidability gl t1; mkVar i|])]);
+		      (onClearedName i (fun i ->
+                        (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
+                    ]
+		| Kapp(Iff,[t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+		        [mkApp (Lazy.force coq_not_iff, [| t1; t2;
+			  decidability gl t1; decidability gl t2; mkVar i|])]);
+		      (onClearedName i (fun i ->
+                        (loop ((i,None,
+			        mk_or (mk_and t1 (mk_not t2))
+				      (mk_and (mk_not t1) t2))::lit))))
+                    ]
+		| Kimp(t1,t2) ->
+                    tclTHENLIST [
+		      (generalize_tac
+		        [mkApp (Lazy.force coq_not_imp, [| t1; t2;
+		          decidability gl t1;mkVar i |])]);
+		      (onClearedName i (fun i ->
+                        (loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
+                    ]
+		| Kapp(Not,[t]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+			[mkApp (Lazy.force coq_not_not, [| t;
+			  decidability gl t; mkVar i |])]);
+		      (onClearedName i (fun i -> (loop ((i,None,t)::lit))))
+                    ]
+		| Kapp(Zle, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_Znot_le_gt, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Zge, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_Znot_ge_lt, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Zlt, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_Znot_lt_ge, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Zgt, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_Znot_gt_le, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Le, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_le, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Ge, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_ge, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Lt, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_lt, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Gt, [t1;t2]) ->
+                    tclTHENLIST [
+		      (generalize_tac
+                        [mkApp (Lazy.force coq_not_gt, [| t1;t2;mkVar i|])]);
+		      (onClearedName i (fun _ -> loop lit))
+                    ]
+		| Kapp(Eq,[typ;t1;t2]) ->
+                    if !old_style_flag then begin
+		      match destructurate_type (pf_nf gl typ) with
+			| Kapp(Nat,_) ->
+                            tclTHENLIST [
+			      (simplest_elim
+				(mkApp
+                                  (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
+			      (onClearedName i (fun _ -> loop lit))
+                            ]
+			| Kapp(Z,_) ->
+                            tclTHENLIST [
+			      (simplest_elim
+				(mkApp
+				  (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
+			      (onClearedName i (fun _ -> loop lit))
+                            ]
+			| _ -> loop lit
+                    end else begin
+		      match destructurate_type (pf_nf gl typ) with
+			| Kapp(Nat,_) ->
+                               (tclTHEN
+			       (convert_hyp_no_check
+                                  (i,body,
+				  (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
+			       (loop lit))
+			| Kapp(Z,_) ->
+                               (tclTHEN
+			       (convert_hyp_no_check
+                                  (i,body,
+				  (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
+			       (loop lit))
+			| _ -> loop lit
+                    end
+		| _ -> loop lit
+              end
+          | _ -> loop lit
+	with e when catchable_exception e -> loop lit
+	end
+  in
+  loop (pf_hyps gl) gl
+
+let destructure_goal gl =
+  let concl = pf_concl gl in
+  let rec loop t =
+    match destructurate_prop t with
+      | Kapp(Not,[t]) ->
+          (tclTHEN
+	     (tclTHEN (unfold sp_not) intro)
+	     destructure_hyps)
+      | Kimp(a,b) -> (tclTHEN intro (loop b))
+      | Kapp(False,[]) -> destructure_hyps
+      | _ ->
+          (tclTHEN
+	     (tclTHEN
+		(Tactics.refine
+		   (mkApp (Lazy.force coq_dec_not_not, [| t;
+			      decidability gl t; mkNewMeta () |])))
+		intro)
+	     (destructure_hyps))
+  in
+  (loop concl) gl
+
+let destructure_goal = all_time (destructure_goal)
+
+let omega_solver gl =
+  Coqlib.check_required_library ["Coq";"omega";"Omega"];
+  let result = destructure_goal gl in
+  (* if !display_time_flag then begin text_time ();
+     flush Pervasives.stdout end; *)
+  result
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
new file mode 100644
index 00000000..3bfdce7f
--- /dev/null
+++ b/plugins/omega/g_omega.ml4
@@ -0,0 +1,47 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(**************************************************************************)
+(*                                                                        *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
+(*                                                                        *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Coq_omega
+open Refiner
+
+let omega_tactic l =
+  let tacs = List.map
+    (function
+       | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
+       | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
+       | "N" -> Tacinterp.interp <:tactic<zify_N>>
+       | "Z" -> Tacinterp.interp <:tactic<zify_op>>
+       | s -> Util.error ("No Omega knowledge base for type "^s))
+    (Util.list_uniquize (List.sort compare l))
+  in
+  tclTHEN
+    (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
+    omega_solver
+
+
+TACTIC EXTEND omega
+|  [ "omega" ] -> [ omega_tactic [] ]
+END
+
+TACTIC EXTEND omega'
+| [ "omega" "with" ne_ident_list(l) ] ->
+    [ omega_tactic (List.map Names.string_of_id l) ]
+| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ]
+END
+
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
new file mode 100644
index 00000000..11ab9c03
--- /dev/null
+++ b/plugins/omega/omega.ml
@@ -0,0 +1,716 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(**************************************************************************)
+(*                                                                        *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
+(*                                                                        *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(*                                                                        *)
+(* 13/10/2002 : modified to cope with an external numbering of equations  *)
+(*   and hypothesis. Its use for Omega is not more complex and it makes   *)
+(*   things much simpler for the reflexive version where we should limit  *)
+(*   the number of source of numbering.                                   *)
+(**************************************************************************)
+
+open Names
+
+module type INT = sig
+  type bigint
+  val less_than : bigint -> bigint -> bool
+  val add : bigint -> bigint -> bigint
+  val sub : bigint -> bigint -> bigint
+  val mult : bigint -> bigint -> bigint
+  val euclid : bigint -> bigint -> bigint * bigint
+  val neg : bigint -> bigint
+  val zero : bigint
+  val one : bigint
+  val to_string : bigint -> string
+end
+
+let debug = ref false
+
+module MakeOmegaSolver (Int:INT) = struct
+
+type bigint = Int.bigint
+let (<?) = Int.less_than
+let (<=?) x y = Int.less_than x y or x = y
+let (>?) x y = Int.less_than y x
+let (>=?) x y = Int.less_than y x or x = y
+let (=?) = (=)
+let (+) = Int.add
+let (-) = Int.sub
+let ( * ) = Int.mult
+let (/) x y = fst (Int.euclid x y)
+let (mod) x y = snd (Int.euclid x y)
+let zero = Int.zero
+let one = Int.one
+let two = one + one
+let negone = Int.neg one
+let abs x = if Int.less_than x zero then Int.neg x else x
+let string_of_bigint = Int.to_string
+let neg = Int.neg
+
+(* To ensure that polymorphic (<) is not used mistakenly on big integers *)
+(* Warning: do not use (=) either on big int *)
+let (<) = ((<) : int -> int -> bool)
+let (>) = ((>) : int -> int -> bool)
+let (<=) = ((<=) : int -> int -> bool)
+let (>=) = ((>=) : int -> int -> bool)
+
+let pp i = print_int i; print_newline (); flush stdout
+
+let push v l = l := v :: !l
+
+let rec pgcd x y = if y =? zero then x else pgcd y (x mod y)
+
+let pgcd_l = function
+  | [] -> failwith "pgcd_l"
+  | x :: l -> List.fold_left pgcd x l
+
+let floor_div a b =
+  match a >=? zero , b >? zero with
+    | true,true -> a / b
+    | false,false -> a / b
+    | true, false -> (a-one) / b - one
+    | false,true  -> (a+one) / b - one
+
+type coeff = {c: bigint ; v: int}
+
+type linear = coeff list
+
+type eqn_kind = EQUA | INEQ | DISE
+
+type afine = {
+  (* a number uniquely identifying the equation *)
+  id: int ;
+  (* a boolean true for an eq, false for an ineq (Sigma a_i x_i >= 0) *)
+  kind: eqn_kind;
+  (* the variables and their coefficient *)
+  body: coeff list;
+  (* a constant *)
+  constant: bigint }
+
+type state_action = {
+  st_new_eq : afine;
+  st_def    : afine;
+  st_orig   : afine;
+  st_coef   : bigint;
+  st_var    : int }
+
+type action =
+  | DIVIDE_AND_APPROX of afine * afine * bigint * bigint
+  | NOT_EXACT_DIVIDE of afine * bigint
+  | FORGET_C of int
+  | EXACT_DIVIDE of afine * bigint
+  | SUM of int * (bigint * afine) * (bigint * afine)
+  | STATE of state_action
+  | HYP of afine
+  | FORGET   of int * int
+  | FORGET_I of int * int
+  | CONTRADICTION of afine * afine
+  | NEGATE_CONTRADICT of afine * afine * bool
+  | MERGE_EQ of int * afine * int
+  | CONSTANT_NOT_NUL of int * bigint
+  | CONSTANT_NUL of int
+  | CONSTANT_NEG of int * bigint
+  | SPLIT_INEQ of afine * (int * action list) * (int * action list)
+  | WEAKEN of int * bigint
+
+exception UNSOLVABLE
+
+exception NO_CONTRADICTION
+
+let display_eq print_var (l,e) =
+  let _ =
+    List.fold_left
+      (fun not_first f ->
+	 print_string
+	   (if f.c <? zero then "- " else if not_first then "+ " else "");
+	 let c = abs f.c in
+	 if c =? one then
+	   Printf.printf "%s " (print_var f.v)
+	 else
+	   Printf.printf "%s %s " (string_of_bigint c) (print_var f.v);
+	 true)
+      false l
+  in
+  if e >? zero then
+    Printf.printf "+ %s " (string_of_bigint e)
+  else if e <? zero then
+    Printf.printf "- %s " (string_of_bigint (abs e))
+
+let rec trace_length l =
+  let action_length accu = function
+    | SPLIT_INEQ (_,(_,l1),(_,l2)) ->
+	accu + one + trace_length l1 + trace_length l2
+    | _ -> accu + one in
+  List.fold_left action_length zero l
+
+let operator_of_eq = function
+  | EQUA -> "=" | DISE -> "!=" | INEQ -> ">="
+
+let kind_of = function
+  | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation"
+
+let display_system print_var l =
+  List.iter
+    (fun { kind=b; body=e; constant=c; id=id} ->
+       Printf.printf "E%d: " id;
+       display_eq print_var (e,c);
+       Printf.printf "%s 0\n" (operator_of_eq b))
+    l;
+  print_string "------------------------\n\n"
+
+let display_inequations print_var l =
+  List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l;
+  print_string "------------------------\n\n"
+
+let sbi = string_of_bigint
+
+let rec display_action print_var = function
+  | act :: l -> begin match act with
+      | DIVIDE_AND_APPROX (e1,e2,k,d) ->
+          Printf.printf
+            "Inequation E%d is divided by %s and the constant coefficient is \
+            rounded by substracting %s.\n" e1.id (sbi k) (sbi d)
+      | NOT_EXACT_DIVIDE (e,k) ->
+          Printf.printf
+            "Constant in equation E%d is not divisible by the pgcd \
+            %s of its other coefficients.\n" e.id (sbi k)
+      | EXACT_DIVIDE (e,k) ->
+          Printf.printf
+            "Equation E%d is divided by the pgcd \
+            %s of its coefficients.\n" e.id (sbi k)
+      | WEAKEN (e,k) ->
+          Printf.printf
+            "To ensure a solution in the dark shadow \
+            the equation E%d is weakened by %s.\n" e (sbi k)
+      | SUM (e,(c1,e1),(c2,e2)) ->
+          Printf.printf
+            "We state %s E%d = %s %s E%d + %s %s E%d.\n"
+            (kind_of e1.kind) e (sbi c1) (kind_of e1.kind) e1.id (sbi c2)
+            (kind_of e2.kind) e2.id
+      | STATE { st_new_eq = e } ->
+          Printf.printf "We define a new equation E%d: " e.id;
+          display_eq print_var (e.body,e.constant);
+          print_string (operator_of_eq e.kind); print_string " 0"
+      | HYP e ->
+          Printf.printf "We define E%d: " e.id;
+          display_eq print_var (e.body,e.constant);
+          print_string (operator_of_eq e.kind); print_string " 0\n"
+      | FORGET_C e ->  Printf.printf "E%d is trivially satisfiable.\n" e
+      | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
+      | FORGET_I (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
+      | MERGE_EQ (e,e1,e2) ->
+         Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e
+      | CONTRADICTION (e1,e2) ->
+          Printf.printf
+            "Equations E%d and E%d imply a contradiction on their \
+            constant factors.\n" e1.id e2.id
+      | NEGATE_CONTRADICT(e1,e2,b) ->
+          Printf.printf
+            "Equations E%d and E%d state that their body is at the same time
+            equal and different\n" e1.id e2.id
+      | CONSTANT_NOT_NUL (e,k) ->
+          Printf.printf "Equation E%d states %s = 0.\n" e (sbi k)
+      | CONSTANT_NEG(e,k) ->
+          Printf.printf "Equation E%d states %s >= 0.\n" e (sbi k)
+      | CONSTANT_NUL e ->
+          Printf.printf "Inequation E%d states 0 != 0.\n" e
+      | SPLIT_INEQ (e,(e1,l1),(e2,l2)) ->
+          Printf.printf "Equation E%d is split in E%d and E%d\n\n" e.id e1 e2;
+          display_action print_var l1;
+          print_newline ();
+          display_action print_var l2;
+          print_newline ()
+    end; display_action print_var l
+  | [] ->
+      flush stdout
+
+let default_print_var v = Printf.sprintf "X%d" v (* For debugging *)
+
+(*""*)
+let add_event, history, clear_history =
+  let accu = ref [] in
+  (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu),
+  (fun () -> !accu),
+  (fun () -> accu := [])
+
+let nf_linear = Sort.list (fun x y -> x.v > y.v)
+
+let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x))
+
+let map_eq_linear f =
+  let rec loop = function
+    | x :: l -> let c = f x.c in if c=?zero then loop l else {v=x.v; c=c} :: loop l
+    | [] -> []
+  in
+  loop
+
+let map_eq_afine f e =
+  { id = e.id; kind = e.kind; body = map_eq_linear f e.body;
+    constant = f e.constant }
+
+let negate_eq = map_eq_afine (fun x -> neg x)
+
+let rec sum p0 p1 = match (p0,p1) with
+  | ([], l) -> l | (l, []) -> l
+  | (((x1::l1) as l1'), ((x2::l2) as l2')) ->
+      if x1.v = x2.v then
+	let c = x1.c + x2.c in
+	if c =? zero then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2
+      else if x1.v > x2.v then
+	x1 :: sum l1 l2'
+      else
+	x2 :: sum l1' l2
+
+let sum_afine new_eq_id eq1 eq2 =
+  { kind = eq1.kind; id = new_eq_id ();
+    body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant }
+
+exception FACTOR1
+
+let rec chop_factor_1 = function
+  | x :: l ->
+    if abs x.c =? one then x,l else let (c',l') = chop_factor_1 l in (c',x::l')
+  | [] -> raise FACTOR1
+
+exception CHOPVAR
+
+let rec chop_var v = function
+  | f :: l -> if f.v = v then f,l else let (f',l') = chop_var v l in (f',f::l')
+  | [] -> raise CHOPVAR
+
+let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) =
+  if e = [] then begin
+    match eq_flag with
+      | EQUA ->
+          if x =? zero then [] else begin
+            add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE
+         end
+      | DISE ->
+          if x <> zero then [] else begin
+            add_event (CONSTANT_NUL id); raise UNSOLVABLE
+          end
+      | INEQ ->
+          if x >=? zero then [] else begin
+            add_event (CONSTANT_NEG(id,x)); raise UNSOLVABLE
+          end
+  end else
+    let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in
+    if eq_flag=EQUA & x mod gcd <> zero then begin
+      add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE
+    end else if eq_flag=DISE & x mod gcd <> zero then begin
+      add_event (FORGET_C eq.id); []
+    end else if gcd <> one then begin
+      let c = floor_div x gcd in
+      let d = x - c * gcd in
+      let new_eq = {id=id; kind=eq_flag; constant=c;
+                    body=map_eq_linear (fun c -> c / gcd) e} in
+      add_event (if eq_flag=EQUA or eq_flag = DISE then EXACT_DIVIDE(eq,gcd)
+                 else DIVIDE_AND_APPROX(eq,new_eq,gcd,d));
+      [new_eq]
+    end else [eq]
+
+let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2
+                        ({body=e1; constant=c1} as eq1) =
+  try
+    let (f,_) = chop_var v e1 in
+    let coeff = if c_unite=?one then neg f.c else if c_unite=? negone then f.c
+                else failwith "eliminate_with_in" in
+    let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in
+    add_event (SUM (res.id,(one,eq1),(coeff,eq2))); res
+  with CHOPVAR -> eq1
+
+let omega_mod a b = a - b * floor_div (two * a + b) (two * b)
+let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 =
+  let e = original.body in
+  let sigma = new_var_id () in
+  let smallest,var =
+    try
+      List.fold_left (fun (v,p) c ->  if v >? (abs c.c) then abs c.c,c.v else (v,p))
+              (abs (List.hd e).c, (List.hd e).v) (List.tl e)
+    with Failure "tl" -> display_system print_var [original] ; failwith "TL" in
+  let m = smallest + one in
+  let new_eq =
+    { constant = omega_mod original.constant m;
+      body = {c= neg m;v=sigma} ::
+             map_eq_linear (fun a -> omega_mod a m) original.body;
+      id = new_eq_id (); kind = EQUA } in
+  let definition =
+    { constant = neg (floor_div (two * original.constant + m) (two * m));
+      body = map_eq_linear (fun a -> neg (floor_div (two * a + m) (two * m)))
+                             original.body;
+      id = new_eq_id (); kind = EQUA } in
+  add_event (STATE {st_new_eq = new_eq; st_def = definition;
+		    st_orig = original; st_coef = m; st_var = sigma});
+  let new_eq = List.hd (normalize new_eq) in
+  let eliminated_var, def = chop_var var new_eq.body in
+  let other_equations =
+    Util.list_map_append
+      (fun e ->
+        normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in
+  let inequations =
+    Util.list_map_append
+      (fun e ->
+        normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in
+  let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in
+  let mod_original = map_eq_afine (fun c -> c / m) original' in
+  add_event (EXACT_DIVIDE (original',m));
+  List.hd (normalize mod_original),other_equations,inequations
+
+let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) =
+  if !debug then display_system print_var (e::other);
+  try
+    let v,def = chop_factor_1 e.body in
+    (Util.list_map_append
+      (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other,
+     Util.list_map_append
+       (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs)
+  with FACTOR1 ->
+    eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs)
+
+let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) =
+  let rec fst_eq_1 = function
+     (eq::l) ->
+        if List.exists (fun x -> abs x.c =? one) eq.body then eq,l
+        else let (eq',l') = fst_eq_1 l in (eq',eq::l')
+   | [] -> raise Not_found in
+  match sys_eq with
+     [] -> if !debug then display_system print_var sys_ineq; sys_ineq
+   | (e1::rest) ->
+       let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in
+       if eq.body = [] then
+         if eq.constant =? zero then begin
+           add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq)
+         end else begin
+           add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE
+         end
+       else
+	 banerjee new_ids
+	   (eliminate_one_equation new_ids (eq,other,sys_ineq))
+
+type kind = INVERTED | NORMAL
+
+let redundancy_elimination new_eq_id system =
+  let normal = function
+     ({body=f::_} as e) when f.c <? zero ->  negate_eq e, INVERTED
+   | e -> e,NORMAL in
+  let table = Hashtbl.create 7 in
+  List.iter
+    (fun e ->
+       let ({body=ne} as nx) ,kind = normal e in
+       if ne = [] then
+         if nx.constant <? zero then begin
+           add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE
+         end else add_event (FORGET_C nx.id)
+       else
+       try
+         let (optnormal,optinvert) = Hashtbl.find table ne in
+         let final =
+           if kind = NORMAL then begin
+             match optnormal with
+                Some v ->
+                  let kept =
+                    if v.constant <? nx.constant
+                    then begin add_event (FORGET (v.id,nx.id));v end
+                    else begin add_event (FORGET (nx.id,v.id));nx end in
+                  (Some(kept),optinvert)
+              | None -> Some nx,optinvert
+           end else begin
+             match optinvert with
+                Some v ->
+                  let _kept =
+                    if v.constant >? nx.constant
+                    then begin add_event (FORGET_I (v.id,nx.id));v end
+                    else begin add_event (FORGET_I (nx.id,v.id));nx end in
+                  (optnormal,Some(if v.constant >? nx.constant then v else nx))
+              | None -> optnormal,Some nx
+           end in
+         begin match final with
+            (Some high, Some low) ->
+              if high.constant <? low.constant then begin
+                add_event(CONTRADICTION (high,negate_eq low));
+                raise UNSOLVABLE
+              end
+          | _ -> () end;
+         Hashtbl.remove table ne;
+         Hashtbl.add table ne final
+       with Not_found ->
+         Hashtbl.add table ne
+           (if kind = NORMAL then (Some nx,None) else (None,Some nx)))
+    system;
+  let accu_eq = ref [] in
+  let accu_ineq = ref [] in
+  Hashtbl.iter
+    (fun p0 p1 -> match (p0,p1) with
+       | (e, (Some x, Some y)) when x.constant =? y.constant ->
+           let id=new_eq_id () in
+           add_event (MERGE_EQ(id,x,y.id));
+           push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq
+       | (e, (optnorm,optinvert)) ->
+           begin match optnorm with
+               Some x -> push x accu_ineq | _ -> () end;
+           begin match optinvert with
+               Some x -> push (negate_eq x) accu_ineq | _ -> () end)
+    table;
+  !accu_eq,!accu_ineq
+
+exception SOLVED_SYSTEM
+
+let select_variable system =
+  let table = Hashtbl.create 7 in
+  let push v c=
+    try let r = Hashtbl.find table v in r := max !r (abs c)
+    with Not_found -> Hashtbl.add table v (ref (abs c)) in
+  List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system;
+  let vmin,cmin = ref (-1), ref zero in
+  let var_cpt = ref 0 in
+  Hashtbl.iter
+    (fun v ({contents =  c}) ->
+       incr var_cpt;
+       if c <? !cmin or !vmin = (-1) then begin vmin := v; cmin := c end)
+    table;
+  if !var_cpt < 1 then raise SOLVED_SYSTEM;
+  !vmin
+
+let classify v system =
+  List.fold_left
+    (fun (not_occ,below,over) eq ->
+       try let f,eq' = chop_var v eq.body in
+       if f.c >=? zero then (not_occ,((f.c,eq) :: below),over)
+       else (not_occ,below,((neg f.c,eq) :: over))
+       with CHOPVAR -> (eq::not_occ,below,over))
+    ([],[],[]) system
+
+let product new_eq_id dark_shadow low high =
+  List.fold_left
+    (fun accu (a,eq1) ->
+       List.fold_left
+         (fun accu (b,eq2) ->
+            let eq =
+              sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1)
+                (map_eq_afine (fun c -> c * a) eq2) in
+            add_event(SUM(eq.id,(b,eq1),(a,eq2)));
+            match normalize eq with
+	      | [eq] ->
+                  let final_eq =
+                    if dark_shadow then
+                      let delta = (a - one) * (b - one) in
+                      add_event(WEAKEN(eq.id,delta));
+                      {id = eq.id; kind=INEQ; body = eq.body;
+                       constant = eq.constant - delta}
+                    else eq
+                  in final_eq :: accu
+              | (e::_) -> failwith "Product dardk"
+              | [] -> accu)
+         accu high)
+    [] low
+
+let fourier_motzkin (new_eq_id,_,print_var) dark_shadow system =
+  let v = select_variable system in
+  let (ineq_out, ineq_low,ineq_high) = classify v system in
+  let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in
+  if !debug then display_system print_var expanded; expanded
+
+let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system =
+  if List.exists (fun e -> e.kind = DISE) system then
+    failwith "disequation in simplify";
+  clear_history ();
+  List.iter (fun e -> add_event (HYP e)) system;
+  let system = Util.list_map_append normalize system in
+  let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in
+  let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in
+  let system = (eqs @ simp_eq,simp_ineq) in
+  let rec loop1a system =
+    let sys_ineq = banerjee new_ids system in
+    loop1b sys_ineq
+  and loop1b sys_ineq =
+    let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in
+    if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq)
+  in
+  let rec loop2 system =
+    try
+      let expanded = fourier_motzkin new_ids dark_shadow system in
+      loop2 (loop1b expanded)
+    with SOLVED_SYSTEM ->
+      if !debug then display_system print_var system; system
+  in
+  loop2 (loop1a system)
+
+let rec depend relie_on accu = function
+  | act :: l ->
+      begin match act with
+	| DIVIDE_AND_APPROX (e,_,_,_) ->
+            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            else depend relie_on accu l
+	| EXACT_DIVIDE (e,_) ->
+            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            else depend relie_on accu l
+	| WEAKEN (e,_) ->
+            if List.mem e relie_on then depend relie_on (act::accu) l
+            else depend relie_on accu l
+	| SUM (e,(_,e1),(_,e2)) ->
+            if List.mem e relie_on then
+	      depend (e1.id::e2.id::relie_on) (act::accu) l
+            else
+	      depend relie_on accu l
+	| STATE {st_new_eq=e;st_orig=o} ->
+            if List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l
+            else depend relie_on accu l
+	| HYP e ->
+            if List.mem e.id relie_on then depend relie_on (act::accu) l
+            else depend relie_on accu l
+	| FORGET_C _ -> depend relie_on accu l
+	| FORGET _ -> depend relie_on accu l
+	| FORGET_I _ -> depend relie_on accu l
+	| MERGE_EQ (e,e1,e2) ->
+            if List.mem e relie_on then
+	      depend (e1.id::e2::relie_on) (act::accu) l
+            else
+	      depend relie_on accu l
+	| NOT_EXACT_DIVIDE (e,_) -> depend (e.id::relie_on) (act::accu) l
+	| CONTRADICTION (e1,e2) ->
+	    depend (e1.id::e2.id::relie_on) (act::accu) l
+	| CONSTANT_NOT_NUL (e,_) -> depend (e::relie_on) (act::accu) l
+	| CONSTANT_NEG (e,_) -> depend (e::relie_on) (act::accu) l
+	| CONSTANT_NUL e -> depend (e::relie_on) (act::accu) l
+	| NEGATE_CONTRADICT (e1,e2,_) ->
+            depend (e1.id::e2.id::relie_on) (act::accu) l
+	| SPLIT_INEQ _ -> failwith "depend"
+      end
+  | [] -> relie_on, accu
+
+(*
+let depend relie_on accu trace =
+  Printf.printf "Longueur de la trace initiale : %d\n"
+    (trace_length trace + trace_length accu);
+  let rel',trace' = depend relie_on accu trace in
+  Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace');
+  rel',trace'
+*)
+
+let solve (new_eq_id,new_eq_var,print_var) system =
+  try let _ = simplify new_eq_id false system in failwith "no contradiction"
+  with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ())))
+
+let negation (eqs,ineqs) =
+  let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in
+  let normal = function
+    | ({body=f::_} as e) when f.c <? zero ->  negate_eq e, INVERTED
+    | e -> e,NORMAL in
+  let table = Hashtbl.create 7 in
+  List.iter (fun e ->
+               let {body=ne;constant=c} ,kind = normal e in
+               Hashtbl.add table (ne,c) (kind,e)) diseq;
+  List.iter (fun e ->
+               assert (e.kind = EQUA);
+               let {body=ne;constant=c},kind = normal e in
+               try
+		 let (kind',e') = Hashtbl.find table (ne,c) in
+		 add_event (NEGATE_CONTRADICT (e,e',kind=kind'));
+		 raise UNSOLVABLE
+               with Not_found -> ()) eqs
+
+exception FULL_SOLUTION of action list * int list
+
+let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
+  clear_history ();
+  List.iter (fun e -> add_event (HYP e)) system;
+  (* Initial simplification phase *)
+  let rec loop1a system =
+    negation system;
+    let sys_ineq = banerjee new_ids system in
+    loop1b sys_ineq
+  and loop1b sys_ineq =
+    let dise,ine = List.partition (fun e -> e.kind = DISE) sys_ineq in
+    let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
+    if simp_eq = [] then dise @ simp_ineq
+    else loop1a (simp_eq,dise @ simp_ineq)
+  in
+  let rec loop2 system =
+    try
+      let expanded = fourier_motzkin new_ids false system in
+      loop2 (loop1b expanded)
+    with SOLVED_SYSTEM -> if !debug then display_system print_var system; system
+  in
+  let rec explode_diseq = function
+    | (de::diseq,ineqs,expl_map) ->
+	let id1 = new_eq_id ()
+	and id2 = new_eq_id () in
+	let e1 =
+          {id = id1; kind=INEQ; body = de.body; constant = de.constant -one} in
+	let e2 =
+	  {id = id2; kind=INEQ; body = map_eq_linear neg de.body;
+           constant = neg de.constant - one} in
+	let new_sys =
+          List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys))
+	    ineqs @
+          List.map (fun (what,sys) -> ((de.id,id2,false)::what,e2::sys))
+	    ineqs
+	in
+	explode_diseq (diseq,new_sys,(de.id,(de,id1,id2))::expl_map)
+    | ([],ineqs,expl_map) -> ineqs,expl_map
+  in
+  try
+    let system = Util.list_map_append normalize system in
+    let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in
+    let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in
+    let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
+    let system = (eqs @ simp_eq,simp_ineq @ dise) in
+    let system' = loop1a system in
+    let diseq,ineq = List.partition (fun e -> e.kind = DISE) system' in
+    let first_segment = history () in
+    let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in
+    let all_solutions =
+      List.map
+        (fun (decomp,sys) ->
+           clear_history ();
+           try let _ = loop2 sys in raise NO_CONTRADICTION
+           with UNSOLVABLE ->
+             let relie_on,path = depend [] [] (history ()) in
+             let dc,_ = List.partition (fun (_,id,_) -> List.mem id relie_on) decomp in
+             let red = List.map (fun (x,_,_) -> x) dc in
+             (red,relie_on,decomp,path))
+        sys_exploded
+    in
+    let max_count sys =
+      let tbl = Hashtbl.create 7 in
+      let augment x =
+        try incr (Hashtbl.find tbl x)
+	with Not_found -> Hashtbl.add tbl x (ref 1) in
+      let eq = ref (-1) and c = ref 0 in
+      List.iter (function
+		   | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on))
+                   | (l,_,_,_) -> List.iter augment l) sys;
+      Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl;
+      !eq
+    in
+    let rec solve systems =
+      try
+	let id = max_count systems in
+        let rec sign = function
+	  | ((id',_,b)::l) -> if id=id' then b else sign l
+          | [] -> failwith "solve" in
+        let s1,s2 =
+          List.partition (fun (_,_,decomp,_) -> sign decomp) systems in
+        let s1' =
+	  List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in
+        let s2' =
+	  List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in
+        let (r1,relie1) = solve s1'
+	and (r2,relie2) = solve s2' in
+	let (eq,id1,id2) = List.assoc id explode_map in
+	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2
+      with FULL_SOLUTION (x0,x1) -> (x0,x1)
+    in
+    let act,relie_on = solve all_solutions in
+    snd(depend relie_on act first_segment)
+  with UNSOLVABLE -> snd (depend [] [] (history ()))
+
+end
diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mllib
new file mode 100644
index 00000000..2b387fdc
--- /dev/null
+++ b/plugins/omega/omega_plugin.mllib
@@ -0,0 +1,4 @@
+Omega
+Coq_omega
+G_omega
+Omega_plugin_mod
diff --git a/plugins/omega/vo.itarget b/plugins/omega/vo.itarget
new file mode 100644
index 00000000..9d9a77a8
--- /dev/null
+++ b/plugins/omega/vo.itarget
@@ -0,0 +1,4 @@
+OmegaLemmas.vo
+OmegaPlugin.vo
+Omega.vo
+PreOmega.vo