Remove romega

24 files changed, 102 insertions, 3615 deletions

diff --git a/CHANGES b/CHANGES
index 87cf86e1eb..45dba33a90 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,10 @@ Plugins
   externally, the Coq development team can provide assistance for extracting
   the plugin and setting up a new repository.
 
+Tactics
+
+- Removed the deprecated `romega` tactics.
+
 Changes from 8.8.2 to 8.9+beta1
 ===============================
 
diff --git a/META.coq.in b/META.coq.in
index a7bf08ec49..1ccde1338f 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -301,18 +301,6 @@ package "plugins" (
     archive(native)  = "omega_plugin.cmx"
   )
 
-  package "romega" (
-
-    description = "Coq romega plugin"
-    version     = "8.10"
-
-    requires    = "coq.plugins.omega"
-    directory   = "romega"
-
-    archive(byte)    = "romega_plugin.cmo"
-    archive(native)  = "romega_plugin.cmx"
-  )
-
   package "micromega" (
 
     description = "Coq micromega plugin"
diff --git a/Makefile.common b/Makefile.common
index 69dea1d284..f90919a4bc 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -95,7 +95,7 @@ CORESRCDIRS:=\
   tactics 	vernac		stm		toplevel
 
 PLUGINDIRS:=\
-  omega		romega 		micromega \
+  omega		micromega \
   setoid_ring 	extraction \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          btauto \
@@ -129,7 +129,6 @@ GRAMMARCMA:=grammar/grammar.cma
 ###########################################################################
 
 OMEGACMO:=plugins/omega/omega_plugin.cmo
-ROMEGACMO:=plugins/romega/romega_plugin.cmo
 MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
 RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
 NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
@@ -150,7 +149,7 @@ LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
 
-PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
+PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \
         $(RINGCMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
diff --git a/Makefile.dev b/Makefile.dev
index 2a7e61126a..82b81908ac 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -169,7 +169,6 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \
 ################
 
 OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO))
-ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO))
 MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO))
 RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO))
 NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO))
@@ -181,7 +180,7 @@ CCVO:=
 DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO))
 LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO))
 
-omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
+omega: $(OMEGAVO) $(OMEGACMO)
 micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
 setoid_ring: $(RINGVO) $(RINGCMO)
 nsatz: $(NSATZVO) $(NSATZCMO)
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index bccd3fefb4..85bb04efe0 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -37,7 +37,7 @@ if [ -z "$GUESS_CHECKER" ]; then
         -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
         -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
         -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
-        -I $COQTOP/plugins/ring       -I $COQTOP/plugins/romega \
+        -I $COQTOP/plugins/ring \
 	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
         -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
         -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 6b7960c92f..dd3908c25f 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -765,8 +765,6 @@ Conflicts exists between integers and constrs.
 %% plugins/ring
 \nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}}
 \nlsep \TERM{ring}~\STAR{\tacconstr}
-%% plugins/romega
-\nlsep \TERM{romega}
 \SEPDEF
 \DEFNT{orient}
        \KWD{$\rightarrow$}~\mid~\KWD{$\leftarrow$}
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index d03a31c044..3b9760f586 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -112,11 +112,11 @@ and checked to be :math:`-1`.
 .. tacn:: lia
    :name: lia
 
-This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega`
-tactics. Roughly speaking, the deductive power of lia is the combined deductive
-power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear
-goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following
-so-called *omega nightmare* :cite:`TheOmegaPaper`.
+   This tactic offers an alternative to the :tacn:`omega` tactic. Roughly
+   speaking, the deductive power of lia is the combined deductive power of
+   :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals
+   that :tacn:`omega` does not solve, such as the following so-called *omega
+   nightmare* :cite:`TheOmegaPaper`.
 
 .. coqtop:: in
 
@@ -124,8 +124,7 @@ so-called *omega nightmare* :cite:`TheOmegaPaper`.
      27 <= 11 * x + 13 * y <= 45 ->
      -10 <= 7 * x - 9 * y <= 4 -> False.
 
-The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and
-:tacn:`romega` is under evaluation.
+The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation.
 
 High level view of `lia`
 ~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 828505b850..03d4f148e3 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -23,13 +23,6 @@ Description of ``omega``
    If the tactic cannot solve the goal, it fails with an error message.
    In any case, the computation eventually stops.
 
-.. tacv:: romega
-   :name: romega
-
-   .. deprecated:: 8.9
-
-      Use :tacn:`lia` instead.
-
 Arithmetical goals recognized by ``omega``
 ------------------------------------------
 
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index 3bd7cd622c..d82e8ae8ad 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -1,4 +1,4 @@
-Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega.
+Require Import Bool DecidableClass Algebra Ring PArith Omega.
 
 Section Bool.
 
diff --git a/plugins/romega/README b/plugins/romega/README
deleted file mode 100644
index 86c9e58afd..0000000000
--- a/plugins/romega/README
+++ /dev/null
@@ -1,6 +0,0 @@
-This work was done for the RNRT Project Calife. 
-As such it is distributed under the LGPL licence.
-
-Report bugs to :
-  pierre.cregut@francetelecom.com
-
diff --git a/plugins/romega/ROmega.v b/plugins/romega/ROmega.v
deleted file mode 100644
index 657aae90e8..0000000000
--- a/plugins/romega/ROmega.v
+++ /dev/null
@@ -1,14 +0,0 @@
-(*************************************************************************
-
-   PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
-   Licence : LGPL version 2.1
-
- *************************************************************************)
-
-Require Import ReflOmegaCore.
-Require Export Setoid.
-Require Export PreOmega.
-Require Export ZArith_base.
-Require Import OmegaPlugin.
-Declare ML Module "romega_plugin".
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
deleted file mode 100644
index da86f4274d..0000000000
--- a/plugins/romega/ReflOmegaCore.v
+++ /dev/null
@@ -1,1874 +0,0 @@
-(* -*- coding: utf-8 -*- *)
-(*************************************************************************
-
-   PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
-   Licence du projet : LGPL version 2.1
-
- *************************************************************************)
-
-Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base.
-Declare Scope Int_scope.
-Delimit Scope Int_scope with I.
-
-(** * Abstract Integers. *)
-
-Module Type Int.
-
-  Parameter t : Set.
-
-  Bind Scope Int_scope with t.
-
-  Parameter Inline zero : t.
-  Parameter Inline one : t.
-  Parameter Inline plus : t -> t -> t.
-  Parameter Inline opp : t -> t.
-  Parameter Inline minus : t -> t -> t.
-  Parameter Inline mult : t -> t -> t.
-
-  Notation "0" := zero : Int_scope.
-  Notation "1" := one : Int_scope.
-  Infix "+" := plus : Int_scope.
-  Infix "-" := minus : Int_scope.
-  Infix "*" := mult : Int_scope.
-  Notation "- x" := (opp x) : Int_scope.
-
-  Open Scope Int_scope.
-
-  (** First, Int is a ring: *)
-  Axiom ring : @ring_theory t 0 1 plus mult minus opp (@eq t).
-
-  (** Int should also be ordered: *)
-
-  Parameter Inline le : t -> t -> Prop.
-  Parameter Inline lt : t -> t -> Prop.
-  Parameter Inline ge : t -> t -> Prop.
-  Parameter Inline gt : t -> t -> Prop.
-  Notation "x <= y" := (le x y): Int_scope.
-  Notation "x < y" := (lt x y) : Int_scope.
-  Notation "x >= y" := (ge x y) : Int_scope.
-  Notation "x > y" := (gt x y): Int_scope.
-  Axiom le_lt_iff : forall i j, (i<=j) <-> ~(j<i).
-  Axiom ge_le_iff : forall i j, (i>=j) <-> (j<=i).
-  Axiom gt_lt_iff : forall i j, (i>j) <-> (j<i).
-
-  (** Basic properties of this order *)
-  Axiom lt_trans : forall i j k, i<j -> j<k -> i<k.
-  Axiom lt_not_eq : forall i j, i<j -> i<>j.
-
-  (** Compatibilities *)
-  Axiom lt_0_1 : 0<1.
-  Axiom plus_le_compat : forall i j k l, i<=j -> k<=l -> i+k<=j+l.
-  Axiom opp_le_compat : forall i j, i<=j -> (-j)<=(-i).
-  Axiom mult_lt_compat_l :
-   forall i j k, 0 < k -> i < j -> k*i<k*j.
-
-  (** We should have a way to decide the equality and the order*)
-  Parameter compare : t -> t -> comparison.
-  Infix "?=" := compare (at level 70, no associativity) : Int_scope.
-  Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j.
-  Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j.
-  Axiom compare_Gt : forall i j, compare i j = Gt <-> i>j.
-
-  (** Up to here, these requirements could be fulfilled
-     by any totally ordered ring. Let's now be int-specific: *)
-  Axiom le_lt_int : forall x y, x<y <-> x<=y+-(1).
-
-  (** Btw, lt_0_1 could be deduced from this last axiom *)
-
-  (** Now we also require a division function.
-      It is deliberately underspecified, since that's enough
-      for the proofs below. But the most appropriate variant
-      (and the one needed to stay in sync with the omega engine)
-      is "Floor" (the historical version of Coq's [Z.div]). *)
-
-  Parameter diveucl : t -> t -> t * t.
-  Notation "i / j" := (fst (diveucl i j)).
-  Notation "i 'mod' j" := (snd (diveucl i j)).
-  Axiom diveucl_spec :
-    forall i j, j<>0 -> i = j * (i/j) + (i mod j).
-
-End Int.
-
-
-
-(** Of course, Z is a model for our abstract int *)
-
-Module Z_as_Int <: Int.
-
-  Open Scope Z_scope.
-
-  Definition t := Z.
-  Definition zero := 0.
-  Definition one := 1.
-  Definition plus := Z.add.
-  Definition opp := Z.opp.
-  Definition minus := Z.sub.
-  Definition mult := Z.mul.
-
-  Lemma ring : @ring_theory t zero one plus mult minus opp (@eq t).
-  Proof.
-  constructor.
-  exact Z.add_0_l.
-  exact Z.add_comm.
-  exact Z.add_assoc.
-  exact Z.mul_1_l.
-  exact Z.mul_comm.
-  exact Z.mul_assoc.
-  exact Z.mul_add_distr_r.
-  unfold minus, Z.sub; auto.
-  exact Z.add_opp_diag_r.
-  Qed.
-
-  Definition le := Z.le.
-  Definition lt := Z.lt.
-  Definition ge := Z.ge.
-  Definition gt := Z.gt.
-  Definition le_lt_iff := Z.le_ngt.
-  Definition ge_le_iff := Z.ge_le_iff.
-  Definition gt_lt_iff := Z.gt_lt_iff.
-
-  Definition lt_trans := Z.lt_trans.
-  Definition lt_not_eq := Z.lt_neq.
-
-  Definition lt_0_1 := Z.lt_0_1.
-  Definition plus_le_compat := Z.add_le_mono.
-  Definition mult_lt_compat_l := Zmult_lt_compat_l.
-  Lemma opp_le_compat i j : i<=j -> (-j)<=(-i).
-  Proof. apply -> Z.opp_le_mono. Qed.
-
-  Definition compare := Z.compare.
-  Definition compare_Eq := Z.compare_eq_iff.
-  Lemma compare_Lt i j : compare i j = Lt <-> i<j.
-  Proof. reflexivity. Qed.
-  Lemma compare_Gt i j : compare i j = Gt <-> i>j.
-  Proof. reflexivity. Qed.
-
-  Definition le_lt_int := Z.lt_le_pred.
-
-  Definition diveucl := Z.div_eucl.
-  Definition diveucl_spec := Z.div_mod.
-
-End Z_as_Int.
-
-
-(** * Properties of abstract integers *)
-
-Module IntProperties (I:Int).
- Import I.
- Local Notation int := I.t.
-
- (** Primo, some consequences of being a ring theory... *)
-
- Definition two := 1+1.
- Notation "2" := two : Int_scope.
-
- (** Aliases for properties packed in the ring record. *)
-
- Definition plus_assoc := ring.(Radd_assoc).
- Definition plus_comm := ring.(Radd_comm).
- Definition plus_0_l := ring.(Radd_0_l).
- Definition mult_assoc := ring.(Rmul_assoc).
- Definition mult_comm := ring.(Rmul_comm).
- Definition mult_1_l := ring.(Rmul_1_l).
- Definition mult_plus_distr_r := ring.(Rdistr_l).
- Definition opp_def := ring.(Ropp_def).
- Definition minus_def := ring.(Rsub_def).
-
- Opaque plus_assoc plus_comm plus_0_l mult_assoc mult_comm mult_1_l
-  mult_plus_distr_r opp_def minus_def.
-
- (** More facts about [plus] *)
-
- Lemma plus_0_r : forall x, x+0 = x.
- Proof. intros; rewrite plus_comm; apply plus_0_l. Qed.
-
- Lemma plus_permute : forall x y z, x+(y+z) = y+(x+z).
- Proof. intros; do 2 rewrite plus_assoc; f_equal; apply plus_comm. Qed.
-
- Lemma plus_reg_l : forall x y z, x+y = x+z -> y = z.
- Proof.
-  intros.
-  rewrite <- (plus_0_r y), <- (plus_0_r z), <-(opp_def x).
-  now rewrite plus_permute, plus_assoc, H, <- plus_assoc, plus_permute.
- Qed.
-
- (** More facts about [mult] *)
-
- Lemma mult_plus_distr_l : forall x y z, x*(y+z)=x*y+x*z.
- Proof.
-  intros.
-  rewrite (mult_comm x (y+z)), (mult_comm x y), (mult_comm x z).
-  apply mult_plus_distr_r.
- Qed.
-
- Lemma mult_0_l x : 0*x = 0.
- Proof.
-  assert (H := mult_plus_distr_r 0 1 x).
-  rewrite plus_0_l, mult_1_l, plus_comm in H.
-  apply plus_reg_l with x.
-  now rewrite <- H, plus_0_r.
- Qed.
-
- Lemma mult_0_r x : x*0 = 0.
- Proof.
-   rewrite mult_comm. apply mult_0_l.
- Qed.
-
- Lemma mult_1_r x : x*1 = x.
- Proof.
-   rewrite mult_comm. apply mult_1_l.
- Qed.
-
- (** More facts about [opp] *)
-
- Definition plus_opp_r := opp_def.
-
- Lemma plus_opp_l : forall x, -x + x = 0.
- Proof. intros; now rewrite plus_comm, opp_def. Qed.
-
- Lemma mult_opp_comm : forall x y, - x * y = x * - y.
- Proof.
-  intros.
-  apply plus_reg_l with (x*y).
-  rewrite <- mult_plus_distr_l, <- mult_plus_distr_r.
-  now rewrite opp_def, opp_def, mult_0_l, mult_comm, mult_0_l.
- Qed.
-
- Lemma opp_eq_mult_neg_1 : forall x, -x = x * -(1).
- Proof.
-  intros; now rewrite mult_comm, mult_opp_comm, mult_1_l.
- Qed.
-
- Lemma opp_involutive : forall x, -(-x) = x.
- Proof.
-  intros.
-  apply plus_reg_l with (-x).
-  now rewrite opp_def, plus_comm, opp_def.
- Qed.
-
- Lemma opp_plus_distr : forall x y, -(x+y) = -x + -y.
- Proof.
-  intros.
-  apply plus_reg_l with (x+y).
-  rewrite opp_def.
-  rewrite plus_permute.
-  do 2 rewrite plus_assoc.
-  now rewrite (plus_comm (-x)), opp_def, plus_0_l, opp_def.
- Qed.
-
- Lemma opp_mult_distr_r : forall x y, -(x*y) = x * -y.
- Proof.
-  intros.
-  rewrite <- mult_opp_comm.
-  apply plus_reg_l with (x*y).
-  now rewrite opp_def, <-mult_plus_distr_r, opp_def, mult_0_l.
- Qed.
-
- Lemma egal_left n m : 0 = n+-m <-> n = m.
- Proof.
-  split; intros.
-  - apply plus_reg_l with (-m).
-    rewrite plus_comm, <- H. symmetry. apply plus_opp_l.
-  - symmetry. subst; apply opp_def.
- Qed.
-
- (** Specialized distributivities *)
-
- Hint Rewrite mult_plus_distr_l mult_plus_distr_r mult_assoc : int.
- Hint Rewrite <- plus_assoc : int.
-
- Hint Rewrite plus_0_l plus_0_r mult_0_l mult_0_r mult_1_l mult_1_r : int.
-
- Lemma OMEGA10 v c1 c2 l1 l2 k1 k2 :
-  v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2) =
-  (v * c1 + l1) * k1 + (v * c2 + l2) * k2.
- Proof.
-  autorewrite with int; f_equal; now rewrite plus_permute.
- Qed.
-
- Lemma OMEGA11 v1 c1 l1 l2 k1 :
-  v1 * (c1 * k1) + (l1 * k1 + l2) = (v1 * c1 + l1) * k1 + l2.
- Proof.
-  now autorewrite with int.
- Qed.
-
- Lemma OMEGA12 v2 c2 l1 l2 k2 :
-   v2 * (c2 * k2) + (l1 + l2 * k2) = l1 + (v2 * c2 + l2) * k2.
- Proof.
-  autorewrite with int; now rewrite plus_permute.
- Qed.
-
- Lemma sum1 a b c d : 0 = a -> 0 = b -> 0 = a * c + b * d.
- Proof.
- intros; subst. now autorewrite with int.
- Qed.
-
-
- (** Secondo, some results about order (and equality) *)
-
- Lemma lt_irrefl : forall n, ~ n<n.
- Proof.
- intros n H.
- elim (lt_not_eq _ _ H); auto.
- Qed.
-
- Lemma lt_antisym : forall n m, n<m -> m<n -> False.
- Proof.
- intros; elim (lt_irrefl _ (lt_trans _ _ _ H H0)); auto.
- Qed.
-
- Lemma lt_le_weak : forall n m, n<m -> n<=m.
- Proof.
-  intros; rewrite le_lt_iff; intro H'; eapply lt_antisym; eauto.
- Qed.
-
- Lemma le_refl : forall n, n<=n.
- Proof.
- intros; rewrite le_lt_iff; apply lt_irrefl; auto.
- Qed.
-
- Lemma le_antisym : forall n m, n<=m -> m<=n -> n=m.
- Proof.
- intros n m; do 2 rewrite le_lt_iff; intros.
- rewrite <- compare_Lt in H0.
- rewrite <- gt_lt_iff, <- compare_Gt in H.
- rewrite <- compare_Eq.
- destruct compare; intuition.
- Qed.
-
- Lemma lt_eq_lt_dec : forall n m, { n<m }+{ n=m }+{ m<n }.
- Proof.
-  intros.
-  generalize (compare_Lt n m)(compare_Eq n m)(compare_Gt n m).
-  destruct compare; [ left; right | left; left | right ]; intuition.
-  rewrite gt_lt_iff in H1; intuition.
- Qed.
-
- Lemma lt_dec : forall n m: int, { n<m } + { ~n<m }.
- Proof.
-  intros.
-  generalize (compare_Lt n m)(compare_Eq n m)(compare_Gt n m).
-  destruct compare; [ right | left | right ]; intuition discriminate.
- Qed.
-
- Lemma lt_le_iff : forall n m, (n<m) <-> ~(m<=n).
- Proof.
-  intros.
-  rewrite le_lt_iff.
-  destruct (lt_dec n m); intuition.
- Qed.
-
- Lemma le_dec : forall n m: int, { n<=m } + { ~n<=m }.
- Proof.
-  intros; destruct (lt_dec m n); [right|left]; rewrite le_lt_iff; intuition.
- Qed.
-
- Lemma le_lt_dec : forall n m, { n<=m } + { m<n }.
- Proof.
-  intros; destruct (le_dec n m); [left|right]; auto; now rewrite lt_le_iff.
- Qed.
-
-
- Definition beq i j := match compare i j with Eq => true | _ => false end.
-
- Infix "=?" := beq : Int_scope.
-
- Lemma beq_iff i j : (i =? j) = true <-> i=j.
- Proof.
- unfold beq. rewrite <- (compare_Eq i j). now destruct compare.
- Qed.
-
- Lemma beq_reflect i j : reflect (i=j) (i =? j).
- Proof.
- apply iff_reflect. symmetry. apply beq_iff.
- Qed.
-
- Lemma eq_dec : forall n m:int, { n=m } + { n<>m }.
- Proof.
-  intros n m; generalize (beq_iff n m); destruct beq; [left|right]; intuition.
- Qed.
-
- Definition blt i j := match compare i j with Lt => true | _ => false end.
-
- Infix "<?" := blt : Int_scope.
-
- Lemma blt_iff i j : (i <? j) = true <-> i<j.
- Proof.
- unfold blt. rewrite <- (compare_Lt i j). now destruct compare.
- Qed.
-
- Lemma blt_reflect i j : reflect (i<j) (i <? j).
- Proof.
- apply iff_reflect. symmetry. apply blt_iff.
- Qed.
-
- Lemma le_is_lt_or_eq : forall n m, n<=m -> { n<m } + { n=m }.
- Proof.
-  intros n m Hnm.
-  destruct (eq_dec n m) as [H'|H'].
-  - right; intuition.
-  - left; rewrite lt_le_iff.
-    contradict H'.
-    now apply le_antisym.
- Qed.
-
- Lemma le_neq_lt : forall n m, n<=m -> n<>m -> n<m.
- Proof.
-  intros n m H. now destruct (le_is_lt_or_eq _ _ H).
- Qed.
-
- Lemma le_trans : forall n m p, n<=m -> m<=p -> n<=p.
- Proof.
-  intros n m p; rewrite 3 le_lt_iff; intros A B C.
-  destruct (lt_eq_lt_dec p m) as [[H|H]|H]; subst; auto.
-  generalize (lt_trans _ _ _ H C); intuition.
- Qed.
-
- Lemma not_eq (a b:int) : ~ a <> b <-> a = b.
- Proof.
-  destruct (eq_dec a b); intuition.
- Qed.
-
- (** Order and operations *)
-
- Lemma le_0_neg n : n <= 0 <-> 0 <= -n.
- Proof.
- rewrite <- (mult_0_l (-(1))) at 2.
- rewrite <- opp_eq_mult_neg_1.
- split; intros.
- - now apply opp_le_compat.
- - rewrite <-(opp_involutive 0), <-(opp_involutive n).
-   now apply opp_le_compat.
- Qed.
-
- Lemma plus_le_reg_r : forall n m p, n + p <= m + p -> n <= m.
- Proof.
- intros.
- replace n with ((n+p)+-p).
- replace m with ((m+p)+-p).
- apply plus_le_compat; auto.
- apply le_refl.
- now rewrite <- plus_assoc, opp_def, plus_0_r.
- now rewrite <- plus_assoc, opp_def, plus_0_r.
- Qed.
-
- Lemma plus_le_lt_compat : forall n m p q, n<=m -> p<q -> n+p<m+q.
- Proof.
- intros.
- apply le_neq_lt.
- apply plus_le_compat; auto.
- apply lt_le_weak; auto.
- rewrite lt_le_iff in H0.
- contradict H0.
- apply plus_le_reg_r with m.
- rewrite (plus_comm q m), <-H0, (plus_comm p m).
- apply plus_le_compat; auto.
- apply le_refl; auto.
- Qed.
-
- Lemma plus_lt_compat : forall n m p q, n<m -> p<q -> n+p<m+q.
- Proof.
- intros.
- apply plus_le_lt_compat; auto.
- apply lt_le_weak; auto.
- Qed.
-
- Lemma opp_lt_compat : forall n m, n<m -> -m < -n.
- Proof.
- intros n m; do 2 rewrite lt_le_iff; intros H; contradict H.
- rewrite <-(opp_involutive m), <-(opp_involutive n).
- apply opp_le_compat; auto.
- Qed.
-
- Lemma lt_0_neg n : n < 0 <-> 0 < -n.
- Proof.
- rewrite <- (mult_0_l (-(1))) at 2.
- rewrite <- opp_eq_mult_neg_1.
- split; intros.
- - now apply opp_lt_compat.
- - rewrite <-(opp_involutive 0), <-(opp_involutive n).
-   now apply opp_lt_compat.
- Qed.
-
- Lemma mult_lt_0_compat : forall n m, 0 < n -> 0 < m -> 0 < n*m.
- Proof.
- intros.
- rewrite <- (mult_0_l n), mult_comm.
- apply mult_lt_compat_l; auto.
- Qed.
-
- Lemma mult_integral_r n m : 0 < n -> n * m = 0 -> m = 0.
- Proof.
- intros Hn H.
- destruct (lt_eq_lt_dec 0 m) as [[Hm| <- ]|Hm]; auto; exfalso.
- - generalize (mult_lt_0_compat _ _ Hn Hm).
-   rewrite H.
-   exact (lt_irrefl 0).
- - rewrite lt_0_neg in Hm.
-   generalize (mult_lt_0_compat _ _ Hn Hm).
-   rewrite <- opp_mult_distr_r, opp_eq_mult_neg_1, H, mult_0_l.
-   exact (lt_irrefl 0).
- Qed.
-
- Lemma mult_integral n m : n * m = 0 -> n = 0 \/ m = 0.
- Proof.
- intros H.
- destruct (lt_eq_lt_dec 0 n) as [[Hn|Hn]|Hn].
- - right; apply (mult_integral_r n m); trivial.
- - now left.
- - right; apply (mult_integral_r (-n) m).
-   + now apply lt_0_neg.
-   + rewrite mult_comm, <- opp_mult_distr_r, mult_comm, H.
-     now rewrite opp_eq_mult_neg_1, mult_0_l.
- Qed.
-
- Lemma mult_le_compat_l i j k :
-   0<=k -> i<=j -> k*i <= k*j.
- Proof.
- intros Hk Hij.
- apply le_is_lt_or_eq in Hk. apply le_is_lt_or_eq in Hij.
- destruct Hk as [Hk | <-], Hij as [Hij | <-];
-  rewrite ? mult_0_l; try apply le_refl.
- now apply lt_le_weak, mult_lt_compat_l.
- Qed.
-
- Lemma mult_le_compat i j k l :
-   i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l.
- Proof.
- intros Hij Hkl Hi Hk.
- apply le_trans with (i*l).
- - now apply mult_le_compat_l.
- - rewrite (mult_comm i), (mult_comm j).
-   apply mult_le_compat_l; trivial.
-   now apply le_trans with k.
- Qed.
-
- Lemma sum5 a b c d : 0 <> c -> 0 <> a -> 0 = b -> 0 <> a * c + b * d.
- Proof.
- intros Hc Ha <-. autorewrite with int. contradict Hc.
- symmetry in Hc. destruct (mult_integral _ _ Hc); congruence.
- Qed.
-
- Lemma le_left n m : n <= m <-> 0 <= m + - n.
- Proof.
-  split; intros.
-  - rewrite <- (opp_def m).
-    apply plus_le_compat.
-    apply le_refl.
-    apply opp_le_compat; auto.
-  - apply plus_le_reg_r with (-n).
-    now rewrite plus_opp_r.
- Qed.
-
- Lemma OMEGA8 x y : 0 <= x -> 0 <= y -> x = - y -> x = 0.
- Proof.
- intros.
- assert (y=-x).
-  subst x; symmetry; apply opp_involutive.
- clear H1; subst y.
- destruct (eq_dec 0 x) as [H'|H']; auto.
- assert (H'':=le_neq_lt _ _ H H').
- generalize (plus_le_lt_compat _ _ _ _ H0 H'').
- rewrite plus_opp_l, plus_0_l.
- intros.
- elim (lt_not_eq _ _ H1); auto.
- Qed.
-
- Lemma sum2 a b c d :
-   0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d.
- Proof.
- intros Hd <- Hb. autorewrite with int.
- rewrite <- (mult_0_l 0).
- apply mult_le_compat; auto; apply le_refl.
- Qed.
-
- Lemma sum3 a b c d :
-  0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d.
- Proof.
- intros.
- rewrite <- (plus_0_l 0).
- apply plus_le_compat; auto.
- rewrite <- (mult_0_l 0).
- apply mult_le_compat; auto; apply le_refl.
- rewrite <- (mult_0_l 0).
- apply mult_le_compat; auto; apply le_refl.
- Qed.
-
- (** Lemmas specific to integers (they use [le_lt_int]) *)
-
- Lemma lt_left n m : n < m <-> 0 <= m + -n + -(1).
- Proof.
- rewrite <- plus_assoc, (plus_comm (-n)), plus_assoc.
- rewrite <- le_left.
- apply le_lt_int.
- Qed.
-
- Lemma OMEGA4 x y z : 0 < x -> x < y -> z * y + x <> 0.
- Proof.
- intros H H0 H'.
- assert (0 < y) by now apply lt_trans with x.
- destruct (lt_eq_lt_dec z 0) as [[G|G]|G].
-
- - generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0).
-   rewrite H'.
-   rewrite <-(mult_1_l y) at 2. rewrite <-mult_plus_distr_r.
-   apply le_lt_iff.
-   rewrite mult_comm. rewrite <- (mult_0_r y).
-   apply mult_le_compat_l; auto using lt_le_weak.
-   apply le_0_neg. rewrite opp_plus_distr.
-   apply le_lt_int. now apply lt_0_neg.
-
- - apply (lt_not_eq 0 (z*y+x)); auto.
-   subst. now autorewrite with int.
-
- - apply (lt_not_eq 0 (z*y+x)); auto.
-   rewrite <- (plus_0_l 0).
-   auto using plus_lt_compat, mult_lt_0_compat.
- Qed.
-
- Lemma OMEGA19 x : x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1).
- Proof.
- intros.
- do 2 rewrite <- le_lt_int.
- rewrite <- opp_eq_mult_neg_1.
- destruct (lt_eq_lt_dec 0 x) as [[H'|H']|H'].
- auto.
- congruence.
- right.
- rewrite <-(mult_0_l (-(1))), <-(opp_eq_mult_neg_1 0).
- apply opp_lt_compat; auto.
- Qed.
-
- Lemma mult_le_approx n m p :
-  0 < n -> p < n -> 0 <= m * n + p -> 0 <= m.
- Proof.
- do 2 rewrite le_lt_iff; intros Hn Hpn H Hm. destruct H.
- apply lt_0_neg, le_lt_int, le_left in Hm.
- rewrite lt_0_neg.
- rewrite opp_plus_distr, mult_comm, opp_mult_distr_r.
- rewrite le_lt_int. apply lt_left.
- rewrite le_lt_int.
- apply le_trans with (n+-(1)); [ now apply le_lt_int | ].
- apply plus_le_compat; [ | apply le_refl ].
- rewrite <- (mult_1_r n) at 1.
- apply mult_le_compat_l; auto using lt_le_weak.
- Qed.
-
- (** Some decidabilities *)
-
- Lemma dec_eq : forall i j:int, decidable (i=j).
- Proof.
-  red; intros; destruct (eq_dec i j); auto.
- Qed.
-
- Lemma dec_ne : forall i j:int, decidable (i<>j).
- Proof.
-  red; intros; destruct (eq_dec i j); auto.
- Qed.
-
- Lemma dec_le : forall i j:int, decidable (i<=j).
- Proof.
-  red; intros; destruct (le_dec i j); auto.
- Qed.
-
- Lemma dec_lt : forall i j:int, decidable (i<j).
- Proof.
-  red; intros; destruct (lt_dec i j); auto.
- Qed.
-
- Lemma dec_ge : forall i j:int, decidable (i>=j).
- Proof.
-  red; intros; rewrite ge_le_iff; destruct (le_dec j i); auto.
- Qed.
-
- Lemma dec_gt : forall i j:int, decidable (i>j).
- Proof.
-  red; intros; rewrite gt_lt_iff; destruct (lt_dec j i); auto.
- Qed.
-
-End IntProperties.
-
-
-(** * The Coq side of the romega tactic *)
-
-Module IntOmega (I:Int).
-Import I.
-Module IP:=IntProperties(I).
-Import IP.
-Local Notation int := I.t.
-
-(* ** Definition of reified integer expressions
-
-   Terms are either:
-   - integers [Tint]
-   - variables [Tvar]
-   - operation over integers (addition, product, opposite, subtraction)
-
-   Opposite and subtraction are translated in additions and products.
-   Note that we'll only deal with products for which at least one side
-   is [Tint]. *)
-
-Inductive term : Set :=
-  | Tint : int -> term
-  | Tplus : term -> term -> term
-  | Tmult : term -> term -> term
-  | Tminus : term -> term -> term
-  | Topp : term -> term
-  | Tvar : N -> term.
-
-Declare Scope romega_scope.
-Bind Scope romega_scope with term.
-Delimit Scope romega_scope with term.
-Arguments Tint _%I.
-Arguments Tplus (_ _)%term.
-Arguments Tmult (_ _)%term.
-Arguments Tminus (_ _)%term.
-Arguments Topp _%term.
-
-Infix "+" := Tplus : romega_scope.
-Infix "*" := Tmult : romega_scope.
-Infix "-" := Tminus : romega_scope.
-Notation "- x" := (Topp x) : romega_scope.
-Notation "[ x ]" := (Tvar x) (at level 0) : romega_scope.
-
-(* ** Definition of reified goals
-
-   Very restricted definition of handled predicates that should be extended
-   to cover a wider set of operations.
-   Taking care of negations and disequations require solving more than a
-   goal in parallel. This is a major improvement over previous versions. *)
-
-Inductive proposition : Set :=
-  (** First, basic equations, disequations, inequations *)
-  | EqTerm : term -> term -> proposition
-  | NeqTerm : term -> term -> proposition
-  | LeqTerm : term -> term -> proposition
-  | GeqTerm : term -> term -> proposition
-  | GtTerm : term -> term -> proposition
-  | LtTerm : term -> term -> proposition
-  (** Then, the supported logical connectors *)
-  | TrueTerm : proposition
-  | FalseTerm : proposition
-  | Tnot : proposition -> proposition
-  | Tor : proposition -> proposition -> proposition
-  | Tand : proposition -> proposition -> proposition
-  | Timp : proposition -> proposition -> proposition
-  (** Everything else is left as a propositional atom (and ignored). *)
-  | Tprop : nat -> proposition.
-
-(** Definition of goals as a list of hypothesis *)
-Notation hyps := (list proposition).
-
-(** Definition of lists of subgoals (set of open goals) *)
-Notation lhyps := (list hyps).
-
-(** A single goal packed in a subgoal list *)
-Notation singleton := (fun a : hyps => a :: nil).
-
-(** An absurd goal *)
-Definition absurd := FalseTerm :: nil.
-
-(** ** Decidable equality on terms *)
-
-Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
-  match t1, t2 with
-  | Tint i1, Tint i2 => i1 =? i2
-  | (t11 + t12), (t21 + t22) => eq_term t11 t21 && eq_term t12 t22
-  | (t11 * t12), (t21 * t22) => eq_term t11 t21 && eq_term t12 t22
-  | (t11 - t12), (t21 - t22) => eq_term t11 t21 && eq_term t12 t22
-  | (- t1), (- t2) => eq_term t1 t2
-  | [v1], [v2] => N.eqb v1 v2
-  | _, _ => false
-  end%term.
-
-Infix "=?" := eq_term : romega_scope.
-
-Theorem eq_term_iff (t t' : term) :
- (t =? t')%term = true <-> t = t'.
-Proof.
- revert t'. induction t; destruct t'; simpl in *;
- rewrite ?andb_true_iff, ?beq_iff, ?N.eqb_eq, ?IHt, ?IHt1, ?IHt2;
-  intuition congruence.
-Qed.
-
-Theorem eq_term_reflect (t t' : term) : reflect (t=t') (t =? t')%term.
-Proof.
- apply iff_reflect. symmetry. apply eq_term_iff.
-Qed.
-
-(** ** Interpretations of terms (as integers). *)
-
-Fixpoint Nnth {A} (n:N)(l:list A)(default:A) :=
- match n, l with
-   | _, nil => default
-   | 0%N, x::_ => x
-   | _, _::l => Nnth (N.pred n) l default
- end.
-
-Fixpoint interp_term (env : list int) (t : term) : int :=
-  match t with
-  | Tint x => x
-  | (t1 + t2)%term => interp_term env t1 + interp_term env t2
-  | (t1 * t2)%term => interp_term env t1 * interp_term env t2
-  | (t1 - t2)%term => interp_term env t1 - interp_term env t2
-  | (- t)%term => - interp_term env t
-  | [n]%term => Nnth n env 0
-  end.
-
-(** ** Interpretation of predicats (as Coq propositions) *)
-
-Fixpoint interp_prop (envp : list Prop) (env : list int)
- (p : proposition) : Prop :=
-  match p with
-  | EqTerm t1 t2 => interp_term env t1 = interp_term env t2
-  | NeqTerm t1 t2 => (interp_term env t1) <> (interp_term env t2)
-  | LeqTerm t1 t2 => interp_term env t1 <= interp_term env t2
-  | GeqTerm t1 t2 => interp_term env t1 >= interp_term env t2
-  | GtTerm t1 t2 => interp_term env t1 > interp_term env t2
-  | LtTerm t1 t2 => interp_term env t1 < interp_term env t2
-  | TrueTerm => True
-  | FalseTerm => False
-  | Tnot p' => ~ interp_prop envp env p'
-  | Tor p1 p2 => interp_prop envp env p1 \/ interp_prop envp env p2
-  | Tand p1 p2 => interp_prop envp env p1 /\ interp_prop envp env p2
-  | Timp p1 p2 => interp_prop envp env p1 -> interp_prop envp env p2
-  | Tprop n => nth n envp True
-  end.
-
-(** ** Intepretation of hypothesis lists (as Coq conjunctions) *)
-
-Fixpoint interp_hyps (envp : list Prop) (env : list int) (l : hyps)
-  : Prop :=
-  match l with
-  | nil => True
-  | p' :: l' => interp_prop envp env p' /\ interp_hyps envp env l'
-  end.
-
-(** ** Interpretation of conclusion + hypotheses
-
-   Here we use Coq implications : it's less easy to manipulate,
-   but handy to relate to the Coq original goal (cf. the use of
-   [generalize], and lighter (no repetition of types in intermediate
-   conjunctions). *)
-
-Fixpoint interp_goal_concl (c : proposition) (envp : list Prop)
- (env : list int) (l : hyps) : Prop :=
-  match l with
-  | nil => interp_prop envp env c
-  | p' :: l' =>
-      interp_prop envp env p' -> interp_goal_concl c envp env l'
-  end.
-
-Notation interp_goal := (interp_goal_concl FalseTerm).
-
-(** Equivalence between these two interpretations. *)
-
-Theorem goal_to_hyps :
- forall (envp : list Prop) (env : list int) (l : hyps),
- (interp_hyps envp env l -> False) -> interp_goal envp env l.
-Proof.
- induction l; simpl; auto.
-Qed.
-
-Theorem hyps_to_goal :
- forall (envp : list Prop) (env : list int) (l : hyps),
- interp_goal envp env l -> interp_hyps envp env l -> False.
-Proof.
- induction l; simpl; auto.
- intros H (H1,H2). auto.
-Qed.
-
-(** ** Interpretations of list of goals
-
-    Here again, two flavours... *)
-
-Fixpoint interp_list_hyps (envp : list Prop) (env : list int)
- (l : lhyps) : Prop :=
-  match l with
-  | nil => False
-  | h :: l' => interp_hyps envp env h \/ interp_list_hyps envp env l'
-  end.
-
-Fixpoint interp_list_goal (envp : list Prop) (env : list int)
- (l : lhyps) : Prop :=
-  match l with
-  | nil => True
-  | h :: l' => interp_goal envp env h /\ interp_list_goal envp env l'
-  end.
-
-(** Equivalence between the two flavours. *)
-
-Theorem list_goal_to_hyps :
- forall (envp : list Prop) (env : list int) (l : lhyps),
- (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l.
-Proof.
- induction l; simpl; intuition. now apply goal_to_hyps.
-Qed.
-
-Theorem list_hyps_to_goal :
- forall (envp : list Prop) (env : list int) (l : lhyps),
- interp_list_goal envp env l -> interp_list_hyps envp env l -> False.
-Proof.
- induction l; simpl; intuition. eapply hyps_to_goal; eauto.
-Qed.
-
-(** ** Stabiliy and validity of operations *)
-
-(** An operation on terms is stable if the interpretation is unchanged. *)
-
-Definition term_stable (f : term -> term) :=
-  forall (e : list int) (t : term), interp_term e t = interp_term e (f t).
-
-(** An operation on one hypothesis is valid if this hypothesis implies
-    the result of this operation. *)
-
-Definition valid1 (f : proposition -> proposition) :=
-  forall (ep : list Prop) (e : list int) (p1 : proposition),
-  interp_prop ep e p1 -> interp_prop ep e (f p1).
-
-Definition valid2 (f : proposition -> proposition -> proposition) :=
-  forall (ep : list Prop) (e : list int) (p1 p2 : proposition),
-  interp_prop ep e p1 ->
-  interp_prop ep e p2 -> interp_prop ep e (f p1 p2).
-
-(** Same for lists of hypotheses, and for list of goals *)
-
-Definition valid_hyps (f : hyps -> hyps) :=
-  forall (ep : list Prop) (e : list int) (lp : hyps),
-  interp_hyps ep e lp -> interp_hyps ep e (f lp).
-
-Definition valid_list_hyps (f : hyps -> lhyps) :=
-  forall (ep : list Prop) (e : list int) (lp : hyps),
-  interp_hyps ep e lp -> interp_list_hyps ep e (f lp).
-
-Definition valid_list_goal (f : hyps -> lhyps) :=
-  forall (ep : list Prop) (e : list int) (lp : hyps),
-  interp_list_goal ep e (f lp) -> interp_goal ep e lp.
-
-(** Some results about these validities. *)
-
-Theorem valid_goal :
-  forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps),
-  valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l.
-Proof.
- intros; simpl; apply goal_to_hyps; intro H1;
- apply (hyps_to_goal ep env (a l) H0); apply H; assumption.
-Qed.
-
-Theorem goal_valid :
- forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f.
-Proof.
- unfold valid_list_goal; intros f H ep e lp H1; apply goal_to_hyps;
- intro H2; apply list_hyps_to_goal with (1 := H1);
- apply (H ep e lp); assumption.
-Qed.
-
-Theorem append_valid :
- forall (ep : list Prop) (e : list int) (l1 l2 : lhyps),
- interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 ->
- interp_list_hyps ep e (l1 ++ l2).
-Proof.
- induction l1; simpl in *.
- - now intros l2 [H| H].
- - intros l2 [[H| H]| H].
-   + auto.
-   + right; apply IHl1; now left.
-   + right; apply IHl1; now right.
-Qed.
-
-(** ** Valid operations on hypotheses *)
-
-(** Extract an hypothesis from the list *)
-
-Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm.
-
-Theorem nth_valid :
- forall (ep : list Prop) (e : list int) (i : nat) (l : hyps),
- interp_hyps ep e l -> interp_prop ep e (nth_hyps i l).
-Proof.
- unfold nth_hyps. induction i; destruct l; simpl in *; try easy.
- intros (H1,H2). now apply IHi.
-Qed.
-
-(** Apply a valid operation on two hypotheses from the list, and
-    store the result in the list. *)
-
-Definition apply_oper_2 (i j : nat)
-  (f : proposition -> proposition -> proposition) (l : hyps) :=
-  f (nth_hyps i l) (nth_hyps j l) :: l.
-
-Theorem apply_oper_2_valid :
- forall (i j : nat) (f : proposition -> proposition -> proposition),
- valid2 f -> valid_hyps (apply_oper_2 i j f).
-Proof.
- intros i j f Hf; unfold apply_oper_2, valid_hyps; simpl;
- intros lp Hlp; split.
- - apply Hf; apply nth_valid; assumption.
- - assumption.
-Qed.
-
-(** In-place modification of an hypothesis by application of
-    a valid operation. *)
-
-Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition)
- (l : hyps) {struct i} : hyps :=
-  match l with
-  | nil => nil
-  | p :: l' =>
-      match i with
-      | O => f p :: l'
-      | S j => p :: apply_oper_1 j f l'
-      end
-  end.
-
-Theorem apply_oper_1_valid :
- forall (i : nat) (f : proposition -> proposition),
- valid1 f -> valid_hyps (apply_oper_1 i f).
-Proof.
- unfold valid_hyps.
- induction i; intros f Hf ep e [ | p lp]; simpl; intuition.
-Qed.
-
-(** ** A tactic for proving stability *)
-
-Ltac loop t :=
-  match t with
-  (* Global *)
-  | (?X1 = ?X2) => loop X1 || loop X2
-  | (_ -> ?X1) => loop X1
-  (* Interpretations *)
-  | (interp_hyps _ _ ?X1) => loop X1
-  | (interp_list_hyps _ _ ?X1) => loop X1
-  | (interp_prop _ _ ?X1) => loop X1
-  | (interp_term _ ?X1) => loop X1
-  (* Propositions *)
-  | (EqTerm ?X1 ?X2) => loop X1 || loop X2
-  | (LeqTerm ?X1 ?X2) => loop X1 || loop X2
-  (* Terms *)
-  | (?X1 + ?X2)%term => loop X1 || loop X2
-  | (?X1 - ?X2)%term => loop X1 || loop X2
-  | (?X1 * ?X2)%term => loop X1 || loop X2
-  | (- ?X1)%term => loop X1
-  | (Tint ?X1) => loop X1
-  (* Eliminations *)
-  | (if ?X1 =? ?X2 then _ else _) =>
-      let H := fresh "H" in
-      case (beq_reflect X1 X2); intro H;
-      try (rewrite H in *; clear H); simpl; auto; Simplify
-  | (if ?X1 <? ?X2 then _ else _) =>
-      case (blt_reflect X1 X2); intro; simpl; auto; Simplify
-  | (if (?X1 =? ?X2)%term then _ else _) =>
-      let H := fresh "H" in
-      case (eq_term_reflect X1 X2); intro H;
-      try (rewrite H in *; clear H); simpl; auto; Simplify
-  | (if _ && _ then _ else _) => rewrite andb_if; Simplify
-  | (if negb _ then _ else _) => rewrite negb_if; Simplify
-  | match N.compare ?X1 ?X2 with _ => _ end =>
-    destruct (N.compare_spec X1 X2); Simplify
-  | match ?X1 with _ => _ end => destruct X1; auto; Simplify
-  | _ => fail
-  end
-
-with Simplify := match goal with
-  |  |- ?X1 => try loop X1
-  | _ => idtac
-  end.
-
-(** ** Operations on equation bodies *)
-
-(** The operations below handle in priority _normalized_ terms, i.e.
-    terms of the form:
-      [([v1]*Tint k1 + ([v2]*Tint k2 + (... + Tint cst)))]
-    with [v1>v2>...] and all [ki<>0].
-    See [normalize] below for a way to put terms in this form.
-
-    These operations also produce a correct (but suboptimal)
-    result in case of non-normalized input terms, but this situation
-    should normally not happen when running [romega].
-
-     /!\ Do not modify this section (especially [fusion] and [normalize])
-    without tweaking the corresponding functions in [refl_omega.ml].
-*)
-
-(** Multiplication and sum by two constants. Invariant: [k1<>0]. *)
-
-Fixpoint scalar_mult_add (t : term) (k1 k2 : int) : term :=
-  match t with
-  | v1 * Tint x1 + l1 =>
-    v1 * Tint (x1 * k1) + scalar_mult_add l1 k1 k2
-  | Tint x => Tint (k1 * x + k2)
-  | _ => t * Tint k1 + Tint k2 (* shouldn't happen *)
-  end%term.
-
-Theorem scalar_mult_add_stable e t k1 k2 :
- interp_term e (scalar_mult_add t k1 k2) =
- interp_term e (t * Tint k1 + Tint k2).
-Proof.
- induction t; simpl; Simplify; simpl; auto. f_equal. apply mult_comm.
- rewrite IHt2. simpl. apply OMEGA11.
-Qed.
-
-(** Multiplication by a (non-nul) constant. *)
-
-Definition scalar_mult (t : term) (k : int) := scalar_mult_add t k 0.
-
-Theorem scalar_mult_stable e t k :
- interp_term e (scalar_mult t k) =
- interp_term e (t * Tint k).
-Proof.
- unfold scalar_mult. rewrite scalar_mult_add_stable. simpl.
- apply plus_0_r.
-Qed.
-
-(** Adding a constant
-
-    Instead of using [scalar_norm_add t 1 k], the following
-    definition spares some computations.
- *)
-
-Fixpoint scalar_add (t : term) (k : int) : term :=
-  match t with
-  | m + l => m + scalar_add l k
-  | Tint x => Tint (x + k)
-  | _ => t + Tint k
-  end%term.
-
-Theorem scalar_add_stable e t k :
- interp_term e (scalar_add t k) = interp_term e (t + Tint k).
-Proof.
- induction t; simpl; Simplify; simpl; auto.
- rewrite IHt2. simpl. apply plus_assoc.
-Qed.
-
-(** Division by a constant
-
-    All the non-constant coefficients should be exactly dividable *)
-
-Fixpoint scalar_div (t : term) (k : int) : option (term * int) :=
-  match t with
-  | v * Tint x + l =>
-    let (q,r) := diveucl x k in
-    if (r =? 0)%I then
-      match scalar_div l k with
-      | None => None
-      | Some (u,c) => Some (v * Tint q + u, c)
-      end
-    else None
-  | Tint x =>
-    let (q,r) := diveucl x k in
-    Some (Tint q, r)
-  | _ => None
-  end%term.
-
-Lemma scalar_div_stable e t k u c : k<>0 ->
-  scalar_div t k = Some (u,c) ->
-  interp_term e (u * Tint k + Tint c) = interp_term e t.
-Proof.
- revert u c.
- induction t; simpl; Simplify; try easy.
- - intros u c Hk. assert (H := diveucl_spec t0 k Hk).
-   simpl in H.
-   destruct diveucl as (q,r). simpl in H. rewrite H.
-   injection 1 as <- <-. simpl. f_equal. apply mult_comm.
- - intros u c Hk.
-   destruct t1; simpl; Simplify; try easy.
-   destruct t1_2; simpl; Simplify; try easy.
-   assert (H := diveucl_spec t0 k Hk).
-   simpl in H.
-   destruct diveucl as (q,r). simpl in H. rewrite H.
-   case beq_reflect; [intros -> | easy].
-   destruct (scalar_div t2 k) as [(u',c')|] eqn:E; [|easy].
-   injection 1 as <- ->. simpl.
-   rewrite <- (IHt2 u' c Hk); simpl; auto.
-   rewrite plus_0_r , (mult_comm k q). symmetry. apply OMEGA11.
-Qed.
-
-
-(** Fusion of two equations.
-
-    From two normalized equations, this fusion will produce
-    a normalized output corresponding to the coefficiented sum.
-    Invariant: [k1<>0] and [k2<>0].
-*)
-
-Fixpoint fusion (t1 t2 : term) (k1 k2 : int) : term :=
-  match t1 with
-  | [v1] * Tint x1 + l1 =>
-    (fix fusion_t1 t2 : term :=
-       match t2 with
-         | [v2] * Tint x2 + l2 =>
-           match N.compare v1 v2 with
-             | Eq =>
-               let k := (k1 * x1 + k2 * x2)%I in
-               if (k =? 0)%I then fusion l1 l2 k1 k2
-               else [v1] * Tint k + fusion l1 l2 k1 k2
-             | Lt => [v2] * Tint (k2 * x2) + fusion_t1 l2
-             | Gt => [v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2
-           end
-         | Tint x2 => [v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2
-         | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *)
-       end) t2
-  | Tint x1 => scalar_mult_add t2 k2 (k1 * x1)
-  | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *)
-  end%term.
-
-Theorem fusion_stable e t1 t2 k1 k2 :
- interp_term e (fusion t1 t2 k1 k2) =
- interp_term e (t1 * Tint k1 + t2 * Tint k2).
-Proof.
- revert t2; induction t1; simpl; Simplify; simpl; auto.
- - intros; rewrite scalar_mult_add_stable. simpl.
-   rewrite plus_comm. f_equal. apply mult_comm.
- - intros. Simplify. induction t2; simpl; Simplify; simpl; auto.
-   + rewrite IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11.
-   + rewrite IHt1_2. simpl. subst n0.
-     rewrite (mult_comm k1), (mult_comm k2) in H0.
-     rewrite <- OMEGA10, H0. now autorewrite with int.
-   + rewrite IHt1_2. simpl. subst n0.
-     rewrite (mult_comm k1), (mult_comm k2); apply OMEGA10.
-   + rewrite IHt2_2. simpl. rewrite (mult_comm k2); apply OMEGA12.
-   + rewrite IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11.
-Qed.
-
-(** Term normalization.
-
-   Precondition: all [Tmult] should be on at least one [Tint].
-   Postcondition: a normalized equivalent term (see below).
-*)
-
-Fixpoint normalize t :=
-  match t with
-  | Tint n => Tint n
-  | [n]%term => ([n] * Tint 1 + Tint 0)%term
-  | (t + t')%term => fusion (normalize t) (normalize t') 1 1
-  | (- t)%term => scalar_mult (normalize t) (-(1))
-  | (t - t')%term => fusion (normalize t) (normalize t') 1 (-(1))
-  | (Tint k * t)%term | (t * Tint k)%term =>
-    if k =? 0 then Tint 0 else scalar_mult (normalize t) k
-  | (t1 * t2)%term => (t1 * t2)%term (* shouldn't happen *)
-  end.
-
-Theorem normalize_stable : term_stable normalize.
-Proof.
- intros e t.
- induction t; simpl; Simplify; simpl;
- rewrite ?scalar_mult_stable; simpl in *; rewrite <- ?IHt1;
- rewrite ?fusion_stable; simpl; autorewrite with int; auto.
- - now f_equal.
- - rewrite mult_comm. now f_equal.
- - rewrite <- opp_eq_mult_neg_1, <-minus_def. now f_equal.
- - rewrite <- opp_eq_mult_neg_1. now f_equal.
-Qed.
-
-(** ** Normalization of a proposition.
-
-    The only basic facts left after normalization are
-    [0 = ...] or [0 <> ...] or [0 <= ...].
-    When a fact is in negative position, we factorize a [Tnot]
-    out of it, and normalize the reversed fact inside.
-
-    /!\ Here again, do not change this code without corresponding
-    modifications in [refl_omega.ml].
-*)
-
-Fixpoint normalize_prop (negated:bool)(p:proposition) :=
-  match p with
-  | EqTerm t1 t2 =>
-    if negated then Tnot (NeqTerm (Tint 0) (normalize (t1-t2)))
-    else EqTerm (Tint 0) (normalize (t1-t2))
-  | NeqTerm t1 t2 =>
-    if negated then Tnot (EqTerm (Tint 0) (normalize (t1-t2)))
-    else NeqTerm (Tint 0) (normalize (t1-t2))
-  | LeqTerm t1 t2 =>
-    if negated then Tnot (LeqTerm (Tint 0) (normalize (t1-t2+Tint (-(1)))))
-    else LeqTerm (Tint 0) (normalize (t2-t1))
-  | GeqTerm t1 t2 =>
-    if negated then Tnot (LeqTerm (Tint 0) (normalize (t2-t1+Tint (-(1)))))
-    else LeqTerm (Tint 0) (normalize (t1-t2))
-  | LtTerm t1 t2 =>
-    if negated then Tnot (LeqTerm (Tint 0) (normalize (t1-t2)))
-    else LeqTerm (Tint 0) (normalize (t2-t1+Tint (-(1))))
-  | GtTerm t1 t2 =>
-    if negated then Tnot (LeqTerm (Tint 0) (normalize (t2-t1)))
-    else LeqTerm (Tint 0) (normalize (t1-t2+Tint (-(1))))
-  | Tnot p => Tnot (normalize_prop (negb negated) p)
-  | Tor p p' => Tor (normalize_prop negated p) (normalize_prop negated p')
-  | Tand p p' => Tand (normalize_prop negated p) (normalize_prop negated p')
-  | Timp p p' => Timp (normalize_prop (negb negated) p)
-                      (normalize_prop negated p')
-  | Tprop _ | TrueTerm | FalseTerm => p
-  end.
-
-Definition normalize_hyps := List.map (normalize_prop false).
-
-Local Ltac simp := cbn -[normalize].
-
-Theorem normalize_prop_valid b e ep p :
-  interp_prop e ep (normalize_prop b p) <-> interp_prop e ep p.
-Proof.
- revert b.
- induction p; intros; simp; try tauto.
- - destruct b; simp;
-   rewrite <- ?normalize_stable; simpl; rewrite ?minus_def.
-   + rewrite not_eq. apply egal_left.
-   + apply egal_left.
- - destruct b; simp;
-   rewrite <- ?normalize_stable; simpl; rewrite ?minus_def;
-   apply not_iff_compat, egal_left.
- - destruct b; simp;
-   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
-   + symmetry. rewrite le_lt_iff. apply not_iff_compat, lt_left.
-   + now rewrite <- le_left.
- - destruct b; simp;
-   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
-   + symmetry. rewrite ge_le_iff, le_lt_iff.
-     apply not_iff_compat, lt_left.
-   + rewrite ge_le_iff. now rewrite <- le_left.
- - destruct b; simp;
-   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
-   + rewrite gt_lt_iff, lt_le_iff. apply not_iff_compat.
-     now rewrite <- le_left.
-   + symmetry. rewrite gt_lt_iff. apply lt_left.
- - destruct b; simp;
-   rewrite <- ? normalize_stable; simpl; rewrite ?minus_def.
-   + rewrite lt_le_iff. apply not_iff_compat.
-     now rewrite <- le_left.
-   + symmetry. apply lt_left.
- - now rewrite IHp.
- - now rewrite IHp1, IHp2.
- - now rewrite IHp1, IHp2.
- - now rewrite IHp1, IHp2.
-Qed.
-
-Theorem normalize_hyps_valid : valid_hyps normalize_hyps.
-Proof.
- intros e ep l. induction l; simpl; intuition.
- now rewrite normalize_prop_valid.
-Qed.
-
-Theorem normalize_hyps_goal (ep : list Prop) (env : list int) (l : hyps) :
- interp_goal ep env (normalize_hyps l) -> interp_goal ep env l.
-Proof.
- intros; apply valid_goal with (2 := H); apply normalize_hyps_valid.
-Qed.
-
-(** ** A simple decidability checker
-
-   For us, everything is considered decidable except
-   propositional atoms [Tprop _]. *)
-
-Fixpoint decidability (p : proposition) : bool :=
-  match p with
-  | Tnot t => decidability t
-  | Tand t1 t2 => decidability t1 && decidability t2
-  | Timp t1 t2 => decidability t1 && decidability t2
-  | Tor t1 t2 => decidability t1 && decidability t2
-  | Tprop _ => false
-  | _ => true
-  end.
-
-Theorem decidable_correct :
- forall (ep : list Prop) (e : list int) (p : proposition),
- decidability p = true -> decidable (interp_prop ep e p).
-Proof.
- induction p; simpl; intros Hp; try destruct (andb_prop _ _ Hp).
- - apply dec_eq.
- - apply dec_ne.
- - apply dec_le.
- - apply dec_ge.
- - apply dec_gt.
- - apply dec_lt.
- - left; auto.
- - right; unfold not; auto.
- - apply dec_not; auto.
- - apply dec_or; auto.
- - apply dec_and; auto.
- - apply dec_imp; auto.
- - discriminate.
-Qed.
-
-(** ** Omega steps
-
-   The following inductive type describes steps as they can be
-   found in the trace coming from the decision procedure Omega.
-   We consider here only normalized equations [0=...], disequations
-   [0<>...] or inequations [0<=...].
-
-   First, the final steps leading to a contradiction:
-   - [O_BAD_CONSTANT i] : hypothesis i has a constant body
-     and this constant is not compatible with the kind of i.
-   - [O_NOT_EXACT_DIVIDE i k] :
-     equation i can be factorized as some [k*t+c] with [0<c<k].
-
-   Now, the intermediate steps leading to a new hypothesis:
-   - [O_DIVIDE i k cont] :
-     the body of hypothesis i could be factorized as [k*t+c]
-     with either [k<>0] and [c=0] for a (dis)equation, or
-     [0<k] and [c<k] for an inequation. We change in-place the
-     body of i for [t].
-   - [O_SUM k1 i1 k2 i2 cont] : creates a new hypothesis whose
-     kind depends on the kind of hypotheses [i1] and [i2], and
-     whose body is [k1*body(i1) + k2*body(i2)]. Depending of the
-     situation, [k1] or [k2] might have to be positive or non-nul.
-   - [O_MERGE_EQ i j cont] :
-     inequations i and j have opposite bodies, we add an equation
-     with one these bodies.
-   - [O_SPLIT_INEQ i cont1 cont2] :
-     disequation i is split into a disjonction of inequations.
-*)
-
-Definition idx := nat. (** Index of an hypothesis in the list *)
-
-Inductive t_omega : Set :=
-  | O_BAD_CONSTANT : idx -> t_omega
-  | O_NOT_EXACT_DIVIDE : idx -> int -> t_omega
-
-  | O_DIVIDE : idx -> int -> t_omega -> t_omega
-  | O_SUM : int -> idx -> int -> idx -> t_omega -> t_omega
-  | O_MERGE_EQ : idx -> idx -> t_omega -> t_omega
-  | O_SPLIT_INEQ : idx -> t_omega -> t_omega -> t_omega.
-
-(** ** Actual resolution steps of an omega normalized goal *)
-
-(** First, the final steps, leading to a contradiction *)
-
-(** [O_BAD_CONSTANT] *)
-
-Definition bad_constant (i : nat) (h : hyps) :=
-  match nth_hyps i h with
-  | EqTerm (Tint Nul) (Tint n) => if n =? Nul then h else absurd
-  | NeqTerm (Tint Nul) (Tint n) => if n =? Nul then absurd else h
-  | LeqTerm (Tint Nul) (Tint n) => if n <? Nul then absurd else h
-  | _ => h
-  end.
-
-Theorem bad_constant_valid i : valid_hyps (bad_constant i).
-Proof.
- unfold valid_hyps, bad_constant; intros ep e lp H.
- generalize (nth_valid ep e i lp H); Simplify.
- rewrite le_lt_iff. intuition.
-Qed.
-
-(** [O_NOT_EXACT_DIVIDE] *)
-
-Definition not_exact_divide (i : nat) (k : int) (l : hyps) :=
-  match nth_hyps i l with
-  | EqTerm (Tint Nul) b =>
-    match scalar_div b k with
-    | Some (body,c) =>
-      if (Nul =? 0) && (0 <? c) && (c <? k) then absurd
-      else l
-    | None => l
-    end
-  | _ => l
-  end.
-
-Theorem not_exact_divide_valid i k :
- valid_hyps (not_exact_divide i k).
-Proof.
- unfold valid_hyps, not_exact_divide; intros.
- generalize (nth_valid ep e i lp).
- destruct (nth_hyps i lp); simpl; auto.
- destruct t0; auto.
- destruct (scalar_div t1 k) as [(body,c)|] eqn:E; auto.
- Simplify.
- assert (k <> 0).
- { intro. apply (lt_not_eq 0 k); eauto using lt_trans. }
- apply (scalar_div_stable e) in E; auto. simpl in E.
- intros H'; rewrite <- H' in E; auto.
- exfalso. revert E. now apply OMEGA4.
-Qed.
-
-(** Now, the steps generating a new equation. *)
-
-(** [O_DIVIDE] *)
-
-Definition divide (k : int) (prop : proposition) :=
-  match prop with
-  | EqTerm (Tint o) b =>
-    match scalar_div b k with
-    | Some (body,c) =>
-      if (o =? 0) && (c =? 0) && negb (k =? 0)
-      then EqTerm (Tint 0) body
-      else TrueTerm
-    | None => TrueTerm
-    end
-  | NeqTerm (Tint o) b =>
-    match scalar_div b k with
-    | Some (body,c) =>
-      if (o =? 0) && (c =? 0) && negb (k =? 0)
-      then NeqTerm (Tint 0) body
-      else TrueTerm
-    | None => TrueTerm
-    end
-  | LeqTerm (Tint o) b =>
-    match scalar_div b k with
-    | Some (body,c) =>
-      if (o =? 0) && (0 <? k) && (c <? k)
-      then LeqTerm (Tint 0) body
-      else prop
-    | None => prop
-    end
-  | _ => TrueTerm
-  end.
-
-Theorem divide_valid k : valid1 (divide k).
-Proof.
- unfold valid1, divide; intros ep e p;
- destruct p; simpl; auto;
- destruct t0; simpl; auto;
- destruct scalar_div as [(body,c)|] eqn:E; simpl; Simplify; auto.
- - apply (scalar_div_stable e) in E; auto. simpl in E.
-   intros H'; rewrite <- H' in E. rewrite plus_0_r in E.
-   apply mult_integral in E. intuition.
- - apply (scalar_div_stable e) in E; auto. simpl in E.
-   intros H' H''. now rewrite <- H'', mult_0_l, plus_0_l in E.
- - assert (k <> 0).
-   { intro. apply (lt_not_eq 0 k); eauto using lt_trans. }
-   apply (scalar_div_stable e) in E; auto. simpl in E. rewrite <- E.
-   intro H'. now apply mult_le_approx with (3 := H').
-Qed.
-
-(** [O_SUM]. Invariant: [k1] and [k2] non-nul. *)
-
-Definition sum (k1 k2 : int) (prop1 prop2 : proposition) :=
-  match prop1 with
-  | EqTerm (Tint o) b1 =>
-      match prop2 with
-      | EqTerm (Tint o') b2 =>
-          if (o =? 0) && (o' =? 0)
-          then EqTerm (Tint 0) (fusion b1 b2 k1 k2)
-          else TrueTerm
-      | LeqTerm (Tint o') b2 =>
-          if (o =? 0) && (o' =? 0) && (0 <? k2)
-          then LeqTerm (Tint 0) (fusion b1 b2 k1 k2)
-          else TrueTerm
-      | NeqTerm (Tint o') b2 =>
-          if (o =? 0) && (o' =? 0) && negb (k2 =? 0)
-          then NeqTerm (Tint 0) (fusion b1 b2 k1 k2)
-          else TrueTerm
-      | _ => TrueTerm
-      end
-  | LeqTerm (Tint o) b1 =>
-      if (o =? 0) && (0 <? k1)
-      then match prop2 with
-          | EqTerm (Tint o') b2 =>
-              if o' =? 0 then
-              LeqTerm (Tint 0) (fusion b1 b2 k1 k2)
-              else TrueTerm
-          | LeqTerm (Tint o') b2 =>
-              if (o' =? 0) && (0 <? k2)
-              then LeqTerm (Tint 0) (fusion b1 b2 k1 k2)
-              else TrueTerm
-          | _ => TrueTerm
-          end
-      else TrueTerm
-  | NeqTerm (Tint o) b1 =>
-      match prop2 with
-      | EqTerm (Tint o') b2 =>
-          if (o =? 0) && (o' =? 0) && negb (k1 =? 0)
-          then NeqTerm (Tint 0) (fusion b1 b2 k1 k2)
-          else TrueTerm
-      | _ => TrueTerm
-      end
-  | _ => TrueTerm
-  end.
-
-Theorem sum_valid :
- forall (k1 k2 : int), valid2 (sum k1 k2).
-Proof.
- unfold valid2; intros k1 k2 t ep e p1 p2; unfold sum;
- Simplify; simpl; rewrite ?fusion_stable;
- simpl; intros; auto.
- - apply sum1; auto.
- - rewrite plus_comm. apply sum5; auto.
- - apply sum2; auto using lt_le_weak.
- - apply sum5; auto.
- - rewrite plus_comm. apply sum2; auto using lt_le_weak.
- - apply sum3; auto using lt_le_weak.
-Qed.
-
-(** [MERGE_EQ] *)
-
-Definition merge_eq (prop1 prop2 : proposition) :=
-  match prop1 with
-  | LeqTerm (Tint o) b1 =>
-      match prop2 with
-      | LeqTerm (Tint o') b2 =>
-          if (o =? 0) && (o' =? 0) &&
-             (b1 =? scalar_mult b2 (-(1)))%term
-          then EqTerm (Tint 0) b1
-          else TrueTerm
-      | _ => TrueTerm
-      end
-  | _ => TrueTerm
-  end.
-
-Theorem merge_eq_valid : valid2 merge_eq.
-Proof.
- unfold valid2, merge_eq; intros ep e p1 p2; Simplify; simpl; auto.
- rewrite scalar_mult_stable. simpl.
- intros; symmetry ; apply OMEGA8 with (2 := H0).
- - assumption.
- - elim opp_eq_mult_neg_1; trivial.
-Qed.
-
-(** [O_SPLIT_INEQ] (only step to produce two subgoals). *)
-
-Definition split_ineq (i : nat) (f1 f2 : hyps -> lhyps) (l : hyps) :=
-  match nth_hyps i l with
-  | NeqTerm (Tint o) b1 =>
-      if o =? 0 then
-       f1 (LeqTerm (Tint 0) (scalar_add b1 (-(1))) :: l) ++
-       f2 (LeqTerm (Tint 0) (scalar_mult_add b1 (-(1)) (-(1))) :: l)
-      else l :: nil
-  | _ => l :: nil
-  end.
-
-Theorem split_ineq_valid :
- forall (i : nat) (f1 f2 : hyps -> lhyps),
- valid_list_hyps f1 ->
- valid_list_hyps f2 -> valid_list_hyps (split_ineq i f1 f2).
-Proof.
- unfold valid_list_hyps, split_ineq; intros i f1 f2 H1 H2 ep e lp H;
- generalize (nth_valid _ _ i _ H); case (nth_hyps i lp);
- simpl; auto; intros t1 t2; case t1; simpl;
- auto; intros z; simpl; auto; intro H3.
- Simplify.
- apply append_valid; elim (OMEGA19 (interp_term e t2)).
- - intro H4; left; apply H1; simpl; rewrite scalar_add_stable;
-    simpl; auto.
- - intro H4; right; apply H2; simpl; rewrite scalar_mult_add_stable;
-    simpl; auto.
- - generalize H3; unfold not; intros E1 E2; apply E1;
-    symmetry ; trivial.
-Qed.
-
-(** ** Replaying the resolution trace *)
-
-Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps :=
-  match t with
-  | O_BAD_CONSTANT i => singleton (bad_constant i l)
-  | O_NOT_EXACT_DIVIDE i k => singleton (not_exact_divide i k l)
-  | O_DIVIDE i k cont =>
-      execute_omega cont (apply_oper_1 i (divide k) l)
-  | O_SUM k1 i1 k2 i2 cont =>
-      execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2) l)
-  | O_MERGE_EQ i1 i2 cont =>
-      execute_omega cont (apply_oper_2 i1 i2 merge_eq l)
-  | O_SPLIT_INEQ i cont1 cont2 =>
-      split_ineq i (execute_omega cont1) (execute_omega cont2) l
-  end.
-
-Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr).
-Proof.
- simple induction tr; unfold valid_list_hyps, valid_hyps; simpl.
- - intros; left; now apply bad_constant_valid.
- - intros; left; now apply not_exact_divide_valid.
- - intros m k t' Ht' ep e lp H; apply Ht';
-    apply
-     (apply_oper_1_valid m (divide k)
-        (divide_valid k) ep e lp H).
- - intros k1 i1 k2 i2 t' Ht' ep e lp H; apply Ht';
-    apply
-     (apply_oper_2_valid i1 i2 (sum k1 k2) (sum_valid k1 k2) ep e
-        lp H).
- - intros i1 i2 t' Ht' ep e lp H; apply Ht';
-    apply
-     (apply_oper_2_valid i1 i2 merge_eq merge_eq_valid ep e
-        lp H).
- - intros i k1 H1 k2 H2 ep e lp H;
-    apply
-     (split_ineq_valid i (execute_omega k1) (execute_omega k2) H1 H2 ep e
-        lp H).
-Qed.
-
-
-(** ** Rules for decomposing the hypothesis
-
-   This type allows navigation in the logical constructors that
-   form the predicats of the hypothesis in order to decompose them.
-   This allows in particular to extract one hypothesis from a conjunction.
-   NB: negations are now silently traversed. *)
-
-Inductive direction : Set :=
-  | D_left : direction
-  | D_right : direction.
-
-(** This type allows extracting useful components from hypothesis, either
-   hypothesis generated by splitting a disjonction, or equations.
-   The last constructor indicates how to solve the obtained system
-   via the use of the trace type of Omega [t_omega] *)
-
-Inductive e_step : Set :=
-  | E_SPLIT : nat -> list direction -> e_step -> e_step -> e_step
-  | E_EXTRACT : nat -> list direction -> e_step -> e_step
-  | E_SOLVE : t_omega -> e_step.
-
-(** Selection of a basic fact inside an hypothesis. *)
-
-Fixpoint extract_hyp_pos (s : list direction) (p : proposition) :
- proposition :=
-  match p, s with
-  | Tand x y, D_left :: l => extract_hyp_pos l x
-  | Tand x y, D_right :: l => extract_hyp_pos l y
-  | Tnot x, _ => extract_hyp_neg s x
-  | _, _ => p
-  end
-
- with extract_hyp_neg (s : list direction) (p : proposition) :
- proposition :=
-  match p, s with
-  | Tor x y, D_left :: l => extract_hyp_neg l x
-  | Tor x y, D_right :: l => extract_hyp_neg l y
-  | Timp x y, D_left :: l =>
-    if decidability x then extract_hyp_pos l x else Tnot p
-  | Timp x y, D_right :: l => extract_hyp_neg l y
-  | Tnot x, _ => if decidability x then extract_hyp_pos s x else Tnot p
-  | _, _ => Tnot p
-  end.
-
-Theorem extract_valid :
- forall s : list direction, valid1 (extract_hyp_pos s).
-Proof.
- assert (forall p s ep e,
-         (interp_prop ep e p ->
-          interp_prop ep e (extract_hyp_pos s p)) /\
-         (interp_prop ep e (Tnot p) ->
-          interp_prop ep e (extract_hyp_neg s p))).
- { induction p; destruct s; simpl; auto; split; try destruct d; try easy;
-   intros; (apply IHp || apply IHp1 || apply IHp2 || idtac); simpl; try tauto;
-   destruct decidability eqn:D; auto;
-   apply (decidable_correct ep e) in D; unfold decidable in D;
-   (apply IHp || apply IHp1); tauto. }
- red. intros. now apply H.
-Qed.
-
-(** Attempt to shorten error messages if romega goes rogue...
-    NB: [interp_list_goal _ _ BUG = False /\ True]. *)
-Definition BUG : lhyps := nil :: nil.
-
-(** Split and extract in hypotheses *)
-
-Fixpoint decompose_solve (s : e_step) (h : hyps) : lhyps :=
-  match s with
-  | E_SPLIT i dl s1 s2 =>
-      match extract_hyp_pos dl (nth_hyps i h) with
-      | Tor x y => decompose_solve s1 (x :: h) ++ decompose_solve s2 (y :: h)
-      | Tnot (Tand x y) =>
-          if decidability x
-          then
-           decompose_solve s1 (Tnot x :: h) ++
-           decompose_solve s2 (Tnot y :: h)
-          else BUG
-      | Timp x y =>
-          if decidability x then
-            decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (y :: h)
-          else BUG
-      | _ => BUG
-      end
-  | E_EXTRACT i dl s1 =>
-      decompose_solve s1 (extract_hyp_pos dl (nth_hyps i h) :: h)
-  | E_SOLVE t => execute_omega t h
-  end.
-
-Theorem decompose_solve_valid (s : e_step) :
- valid_list_goal (decompose_solve s).
-Proof.
- apply goal_valid. red. induction s; simpl; intros ep e lp H.
- - assert (H' : interp_prop ep e (extract_hyp_pos l (nth_hyps n lp))).
-   { now apply extract_valid, nth_valid. }
-   destruct extract_hyp_pos; simpl in *; auto.
-   + destruct p; simpl; auto.
-     destruct decidability eqn:D; [ | simpl; auto].
-     apply (decidable_correct ep e) in D.
-     apply append_valid. simpl in *. destruct D.
-     * right. apply IHs2. simpl; auto.
-     * left. apply IHs1. simpl; auto.
-   + apply append_valid. destruct H'.
-     * left. apply IHs1. simpl; auto.
-     * right. apply IHs2. simpl; auto.
-   + destruct decidability eqn:D; [ | simpl; auto].
-     apply (decidable_correct ep e) in D.
-     apply append_valid. destruct D.
-     * right. apply IHs2. simpl; auto.
-     * left. apply IHs1. simpl; auto.
- - apply IHs; simpl; split; auto.
-   now apply extract_valid, nth_valid.
- - now apply omega_valid.
-Qed.
-
-(** Reduction of subgoal list by discarding the contradictory subgoals. *)
-
-Definition valid_lhyps (f : lhyps -> lhyps) :=
-  forall (ep : list Prop) (e : list int) (lp : lhyps),
-  interp_list_hyps ep e lp -> interp_list_hyps ep e (f lp).
-
-Fixpoint reduce_lhyps (lp : lhyps) : lhyps :=
-  match lp with
-  | nil => nil
-  | (FalseTerm :: nil) :: lp' => reduce_lhyps lp'
-  | x :: lp' => BUG
-  end.
-
-Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps.
-Proof.
- unfold valid_lhyps; intros ep e lp; elim lp.
- - simpl; auto.
- - intros a l HR; elim a.
-    + simpl; tauto.
-    + intros a1 l1; case l1; case a1; simpl; tauto.
-Qed.
-
-Theorem do_reduce_lhyps :
- forall (envp : list Prop) (env : list int) (l : lhyps),
- interp_list_goal envp env (reduce_lhyps l) -> interp_list_goal envp env l.
-Proof.
- intros envp env l H; apply list_goal_to_hyps; intro H1;
- apply list_hyps_to_goal with (1 := H); apply reduce_lhyps_valid;
- assumption.
-Qed.
-
-(** Pushing the conclusion into the hypotheses. *)
-
-Definition concl_to_hyp (p : proposition) :=
-  if decidability p then Tnot p else TrueTerm.
-
-Definition do_concl_to_hyp :
-  forall (envp : list Prop) (env : list int) (c : proposition) (l : hyps),
-  interp_goal envp env (concl_to_hyp c :: l) ->
-  interp_goal_concl c envp env l.
-Proof.
- induction l; simpl.
- - unfold concl_to_hyp; simpl.
-   destruct decidability eqn:D; [ | simpl; tauto ].
-   apply (decidable_correct envp env) in D. unfold decidable in D.
-   simpl. tauto.
- - simpl in *; tauto.
-Qed.
-
-(** The omega tactic : all steps together *)
-
-Definition omega_tactic (t1 : e_step) (c : proposition) (l : hyps) :=
-  reduce_lhyps (decompose_solve t1 (normalize_hyps (concl_to_hyp c :: l))).
-
-Theorem do_omega :
- forall (t : e_step) (envp : list Prop)
-   (env : list int) (c : proposition) (l : hyps),
- interp_list_goal envp env (omega_tactic t c l) ->
- interp_goal_concl c envp env l.
-Proof.
- unfold omega_tactic; intros t ep e c l H.
- apply do_concl_to_hyp.
- apply normalize_hyps_goal.
- apply (decompose_solve_valid t).
- now apply do_reduce_lhyps.
-Qed.
-
-End IntOmega.
-
-(** For now, the above modular construction is instanciated on Z,
-    in order to retrieve the initial ROmega. *)
-
-Module ZOmega := IntOmega(Z_as_Int).
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
deleted file mode 100644
index 949cba2dbe..0000000000
--- a/plugins/romega/const_omega.ml
+++ /dev/null
@@ -1,332 +0,0 @@
-(*************************************************************************
-
-   PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
-   Licence : LGPL version 2.1
-
- *************************************************************************)
-
-open Names
-
-let module_refl_name = "ReflOmegaCore"
-let module_refl_path = ["Coq"; "romega"; module_refl_name]
-
-type result =
-  | Kvar of string
-  | Kapp of string * EConstr.t list
-  | Kimp of EConstr.t * EConstr.t
-  | Kufo
-
-let meaningful_submodule = [ "Z"; "N"; "Pos" ]
-
-let string_of_global r =
-  let dp = Nametab.dirpath_of_global r in
-  let prefix = match Names.DirPath.repr dp with
-    | [] -> ""
-    | m::_ ->
-      let s = Names.Id.to_string m in
-      if Util.String.List.mem s meaningful_submodule then s^"." else ""
-  in
-  prefix^(Names.Id.to_string (Nametab.basename_of_global r))
-
-let destructurate sigma t =
-  let c, args = EConstr.decompose_app sigma t in
-  let open Constr in
-  match EConstr.kind sigma c, args with
-  | Const (sp,_), args ->
-     Kapp (string_of_global (Globnames.ConstRef sp), args)
-  | Construct (csp,_) , args ->
-     Kapp (string_of_global (Globnames.ConstructRef csp), args)
-  | Ind (isp,_), args ->
-     Kapp (string_of_global (Globnames.IndRef isp), args)
-  | Var id, [] -> Kvar(Names.Id.to_string id)
-  | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
-  | _ -> Kufo
-
-exception DestConstApp
-
-let dest_const_apply sigma t =
-  let open Constr in
-  let f,args = EConstr.decompose_app sigma t in
-  let ref =
-  match EConstr.kind sigma f with
-    | Const (sp,_)      -> Globnames.ConstRef sp
-    | Construct (csp,_) -> Globnames.ConstructRef csp
-    | Ind (isp,_)       -> Globnames.IndRef isp
-    | _ -> raise DestConstApp
-  in Nametab.basename_of_global ref, args
-
-let logic_dir = ["Coq";"Logic";"Decidable"]
-
-let coq_modules =
-  Coqlib.init_modules @ [logic_dir] @ Coqlib.arith_modules @ Coqlib.zarith_base_modules
-    @ [["Coq"; "Lists"; "List"]]
-    @ [module_refl_path]
-    @ [module_refl_path@["ZOmega"]]
-
-let bin_module = [["Coq";"Numbers";"BinNums"]]
-let z_module = [["Coq";"ZArith";"BinInt"]]
-
-let init_constant x =
-  EConstr.of_constr @@
-  UnivGen.constr_of_global @@
-  Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x
-let constant x =
-  EConstr.of_constr @@
-  UnivGen.constr_of_global @@
-  Coqlib.gen_reference_in_modules "Omega" coq_modules x
-let z_constant x =
-  EConstr.of_constr @@
-  UnivGen.constr_of_global @@
-  Coqlib.gen_reference_in_modules "Omega" z_module x
-let bin_constant x =
-  EConstr.of_constr @@
-  UnivGen.constr_of_global @@
-  Coqlib.gen_reference_in_modules "Omega" bin_module x
-
-(* Logic *)
-let coq_refl_equal = lazy(init_constant "eq_refl")
-let coq_and = lazy(init_constant "and")
-let coq_not = lazy(init_constant "not")
-let coq_or = lazy(init_constant "or")
-let coq_True = lazy(init_constant "True")
-let coq_False = lazy(init_constant "False")
-let coq_I = lazy(init_constant "I")
-
-(* ReflOmegaCore/ZOmega *)
-
-let coq_t_int = lazy (constant  "Tint")
-let coq_t_plus = lazy (constant  "Tplus")
-let coq_t_mult = lazy (constant  "Tmult")
-let coq_t_opp = lazy (constant  "Topp")
-let coq_t_minus = lazy (constant  "Tminus")
-let coq_t_var = lazy (constant  "Tvar")
-
-let coq_proposition = lazy (constant  "proposition")
-let coq_p_eq = lazy (constant  "EqTerm")
-let coq_p_leq = lazy (constant  "LeqTerm")
-let coq_p_geq = lazy (constant  "GeqTerm")
-let coq_p_lt = lazy (constant  "LtTerm")
-let coq_p_gt = lazy (constant  "GtTerm")
-let coq_p_neq = lazy (constant  "NeqTerm")
-let coq_p_true = lazy (constant  "TrueTerm")
-let coq_p_false = lazy (constant  "FalseTerm")
-let coq_p_not = lazy (constant  "Tnot")
-let coq_p_or = lazy (constant  "Tor")
-let coq_p_and = lazy (constant  "Tand")
-let coq_p_imp = lazy (constant  "Timp")
-let coq_p_prop = lazy (constant  "Tprop")
-
-let coq_s_bad_constant = lazy (constant  "O_BAD_CONSTANT")
-let coq_s_divide = lazy (constant  "O_DIVIDE")
-let coq_s_not_exact_divide = lazy (constant  "O_NOT_EXACT_DIVIDE")
-let coq_s_sum = lazy (constant  "O_SUM")
-let coq_s_merge_eq = lazy (constant  "O_MERGE_EQ")
-let coq_s_split_ineq =lazy (constant  "O_SPLIT_INEQ")
-
-(* construction for the [extract_hyp] tactic *)
-let coq_direction = lazy  (constant  "direction")
-let coq_d_left = lazy  (constant  "D_left")
-let coq_d_right = lazy  (constant  "D_right")
-
-let coq_e_split = lazy  (constant  "E_SPLIT")
-let coq_e_extract = lazy  (constant  "E_EXTRACT")
-let coq_e_solve = lazy  (constant  "E_SOLVE")
-
-let coq_interp_sequent = lazy (constant  "interp_goal_concl")
-let coq_do_omega = lazy (constant  "do_omega")
-
-(* Nat *)
-
-let coq_S = lazy(init_constant "S")
-let coq_O = lazy(init_constant "O")
-
-let rec mk_nat = function
-  | 0 -> Lazy.force coq_O
-  | n -> EConstr.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |])
-
-(* Lists *)
-
-let mkListConst c =
-  let r =
-    Coqlib.coq_reference "" ["Init";"Datatypes"] c
-  in
-  let inst =
-    if Global.is_polymorphic r then
-      fun u -> EConstr.EInstance.make (Univ.Instance.of_array [|u|])
-    else
-      fun _ -> EConstr.EInstance.empty
-  in
-    fun u -> EConstr.mkConstructU (Globnames.destConstructRef r, inst u)
-
-let coq_cons univ typ = EConstr.mkApp (mkListConst "cons" univ, [|typ|])
-let coq_nil univ typ =  EConstr.mkApp (mkListConst "nil" univ, [|typ|])
-
-let mk_list univ typ l =
-  let rec loop = function
-    | [] -> coq_nil univ typ
-    | (step :: l) ->
-       EConstr.mkApp (coq_cons univ typ, [| step; loop l |]) in
-  loop l
-
-let mk_plist =
-  let type1lev = UnivGen.new_univ_level () in
-  fun l -> mk_list type1lev EConstr.mkProp l
-
-let mk_list = mk_list Univ.Level.set
-
-type parse_term =
-  | Tplus of EConstr.t * EConstr.t
-  | Tmult of EConstr.t * EConstr.t
-  | Tminus of EConstr.t * EConstr.t
-  | Topp of EConstr.t
-  | Tsucc of EConstr.t
-  | Tnum of Bigint.bigint
-  | Tother
-
-type parse_rel =
-  | Req of EConstr.t * EConstr.t
-  | Rne of EConstr.t * EConstr.t
-  | Rlt of EConstr.t * EConstr.t
-  | Rle of EConstr.t * EConstr.t
-  | Rgt of EConstr.t * EConstr.t
-  | Rge of EConstr.t * EConstr.t
-  | Rtrue
-  | Rfalse
-  | Rnot of EConstr.t
-  | Ror of EConstr.t * EConstr.t
-  | Rand of EConstr.t * EConstr.t
-  | Rimp of EConstr.t * EConstr.t
-  | Riff of EConstr.t * EConstr.t
-  | Rother
-
-let parse_logic_rel sigma c = match destructurate sigma c with
-  | Kapp("True",[]) -> Rtrue
-  | Kapp("False",[]) -> Rfalse
-  | Kapp("not",[t]) -> Rnot t
-  | Kapp("or",[t1;t2]) -> Ror (t1,t2)
-  | Kapp("and",[t1;t2]) -> Rand (t1,t2)
-  | Kimp(t1,t2) -> Rimp (t1,t2)
-  | Kapp("iff",[t1;t2]) -> Riff (t1,t2)
-  | _ -> Rother
-
-(* Binary numbers *)
-
-let coq_Z = lazy (bin_constant "Z")
-let coq_xH = lazy (bin_constant "xH")
-let coq_xO = lazy (bin_constant "xO")
-let coq_xI = lazy (bin_constant "xI")
-let coq_Z0 = lazy (bin_constant "Z0")
-let coq_Zpos = lazy (bin_constant "Zpos")
-let coq_Zneg = lazy (bin_constant "Zneg")
-let coq_N0 = lazy (bin_constant "N0")
-let coq_Npos = lazy (bin_constant "Npos")
-
-let rec mk_positive n =
-  if Bigint.equal n Bigint.one then Lazy.force coq_xH
-  else
-    let (q,r) = Bigint.euclid n Bigint.two in
-    EConstr.mkApp
-      ((if Bigint.equal r Bigint.zero
-        then Lazy.force coq_xO else Lazy.force coq_xI),
-       [| mk_positive q |])
-
-let mk_N = function
-  | 0 -> Lazy.force coq_N0
-  | n -> EConstr.mkApp (Lazy.force coq_Npos,
-                     [| mk_positive (Bigint.of_int n) |])
-
-module type Int = sig
-  val typ : EConstr.t Lazy.t
-  val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool
-  val plus : EConstr.t Lazy.t
-  val mult : EConstr.t Lazy.t
-  val opp : EConstr.t Lazy.t
-  val minus : EConstr.t Lazy.t
-
-  val mk : Bigint.bigint -> EConstr.t
-  val parse_term : Evd.evar_map -> EConstr.t -> parse_term
-  val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel
-  (* check whether t is built only with numbers and + * - *)
-  val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option
-end
-
-module Z : Int = struct
-
-let typ = coq_Z
-let plus = lazy (z_constant "Z.add")
-let mult = lazy (z_constant  "Z.mul")
-let opp = lazy (z_constant "Z.opp")
-let minus = lazy (z_constant "Z.sub")
-
-let recognize_pos sigma t =
-  let rec loop t =
-    let f,l = dest_const_apply sigma t in
-    match Id.to_string f,l with
-    | "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
-    | "xO",[t] -> Bigint.mult Bigint.two (loop t)
-    | "xH",[] -> Bigint.one
-    | _ -> raise DestConstApp
-  in
-  try Some (loop t) with DestConstApp -> None
-
-let recognize_Z sigma t =
-  try
-    let f,l = dest_const_apply sigma t in
-    match Id.to_string f,l with
-    | "Zpos",[t] -> recognize_pos sigma t
-    | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos sigma t)
-    | "Z0",[] -> Some Bigint.zero
-    | _ -> None
-  with DestConstApp -> None
-
-let mk_Z n =
-  if Bigint.equal n Bigint.zero then Lazy.force coq_Z0
-  else if Bigint.is_strictly_pos n then
-    EConstr.mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
-  else
-    EConstr.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |])
-
-let mk = mk_Z
-
-let parse_term sigma t =
-  match destructurate sigma t with
-  | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2)
-  | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2)
-  | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2)
-  | Kapp("Z.opp",[t]) -> Topp t
-  | Kapp("Z.succ",[t]) -> Tsucc t
-  | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
-  | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
-     (match recognize_Z sigma t with Some t -> Tnum t | None -> Tother)
-  | _ -> Tother
-
-let is_int_typ gl t =
-  Tacmach.New.pf_apply Reductionops.is_conv gl t (Lazy.force coq_Z)
-
-let parse_rel gl t =
-  let sigma = Proofview.Goal.sigma gl in
-  match destructurate sigma t with
-  | Kapp("eq",[typ;t1;t2]) when is_int_typ gl typ -> Req (t1,t2)
-  | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
-  | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
-  | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
-  | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2)
-  | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2)
-  | _ -> parse_logic_rel sigma t
-
-let rec get_scalar sigma t =
-  match destructurate sigma t with
-  | Kapp("Z.add", [t1;t2]) ->
-     Option.lift2 Bigint.add (get_scalar sigma t1) (get_scalar sigma t2)
-  | Kapp ("Z.sub",[t1;t2]) ->
-     Option.lift2 Bigint.sub (get_scalar sigma t1) (get_scalar sigma t2)
-  | Kapp ("Z.mul",[t1;t2]) ->
-     Option.lift2 Bigint.mult (get_scalar sigma t1) (get_scalar sigma t2)
-  | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar sigma t)
-  | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar sigma t)
-  | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar sigma t)
-  | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z sigma t
-  | _ -> None
-
-end
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
deleted file mode 100644
index 64668df007..0000000000
--- a/plugins/romega/const_omega.mli
+++ /dev/null
@@ -1,124 +0,0 @@
-(*************************************************************************
-
-   PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
-   Licence : LGPL version 2.1
-
- *************************************************************************)
-
-
-(** Coq objects used in romega *)
-
-(* from Logic *)
-val coq_refl_equal : EConstr.t lazy_t
-val coq_and : EConstr.t lazy_t
-val coq_not : EConstr.t lazy_t
-val coq_or : EConstr.t lazy_t
-val coq_True : EConstr.t lazy_t
-val coq_False : EConstr.t lazy_t
-val coq_I : EConstr.t lazy_t
-
-(* from ReflOmegaCore/ZOmega *)
-
-val coq_t_int : EConstr.t lazy_t
-val coq_t_plus : EConstr.t lazy_t
-val coq_t_mult : EConstr.t lazy_t
-val coq_t_opp : EConstr.t lazy_t
-val coq_t_minus : EConstr.t lazy_t
-val coq_t_var : EConstr.t lazy_t
-
-val coq_proposition : EConstr.t lazy_t
-val coq_p_eq : EConstr.t lazy_t
-val coq_p_leq : EConstr.t lazy_t
-val coq_p_geq : EConstr.t lazy_t
-val coq_p_lt : EConstr.t lazy_t
-val coq_p_gt : EConstr.t lazy_t
-val coq_p_neq : EConstr.t lazy_t
-val coq_p_true : EConstr.t lazy_t
-val coq_p_false : EConstr.t lazy_t
-val coq_p_not : EConstr.t lazy_t
-val coq_p_or : EConstr.t lazy_t
-val coq_p_and : EConstr.t lazy_t
-val coq_p_imp : EConstr.t lazy_t
-val coq_p_prop : EConstr.t lazy_t
-
-val coq_s_bad_constant : EConstr.t lazy_t
-val coq_s_divide : EConstr.t lazy_t
-val coq_s_not_exact_divide : EConstr.t lazy_t
-val coq_s_sum : EConstr.t lazy_t
-val coq_s_merge_eq : EConstr.t lazy_t
-val coq_s_split_ineq : EConstr.t lazy_t
-
-val coq_direction : EConstr.t lazy_t
-val coq_d_left : EConstr.t lazy_t
-val coq_d_right : EConstr.t lazy_t
-
-val coq_e_split : EConstr.t lazy_t
-val coq_e_extract : EConstr.t lazy_t
-val coq_e_solve : EConstr.t lazy_t
-
-val coq_interp_sequent : EConstr.t lazy_t
-val coq_do_omega : EConstr.t lazy_t
-
-val mk_nat : int -> EConstr.t
-val mk_N : int -> EConstr.t
-
-(** Precondition: the type of the list is in Set *)
-val mk_list : EConstr.t -> EConstr.t list -> EConstr.t
-val mk_plist : EConstr.types list -> EConstr.types
-
-(** Analyzing a coq term *)
-
-(* The generic result shape of the analysis of a term.
-   One-level depth, except when a number is found *)
-type parse_term =
-    Tplus of EConstr.t * EConstr.t
-  | Tmult of EConstr.t * EConstr.t
-  | Tminus of EConstr.t * EConstr.t
-  | Topp of EConstr.t
-  | Tsucc of EConstr.t
-  | Tnum of Bigint.bigint
-  | Tother
-
-(* The generic result shape of the analysis of a relation.
-   One-level depth. *)
-type parse_rel =
-    Req of EConstr.t * EConstr.t
-  | Rne of EConstr.t * EConstr.t
-  | Rlt of EConstr.t * EConstr.t
-  | Rle of EConstr.t * EConstr.t
-  | Rgt of EConstr.t * EConstr.t
-  | Rge of EConstr.t * EConstr.t
-  | Rtrue
-  | Rfalse
-  | Rnot of EConstr.t
-  | Ror of EConstr.t * EConstr.t
-  | Rand of EConstr.t * EConstr.t
-  | Rimp of EConstr.t * EConstr.t
-  | Riff of EConstr.t * EConstr.t
-  | Rother
-
-(* A module factorizing what we should now about the number representation *)
-module type Int =
-  sig
-    (* the coq type of the numbers *)
-    val typ : EConstr.t Lazy.t
-    (* Is a constr expands to the type of these numbers *)
-    val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool
-    (* the operations on the numbers *)
-    val plus : EConstr.t Lazy.t
-    val mult : EConstr.t Lazy.t
-    val opp : EConstr.t Lazy.t
-    val minus : EConstr.t Lazy.t
-    (* building a coq number *)
-    val mk : Bigint.bigint -> EConstr.t
-    (* parsing a term (one level, except if a number is found) *)
-    val parse_term : Evd.evar_map -> EConstr.t -> parse_term
-    (* parsing a relation expression, including = < <= >= > *)
-    val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel
-    (* Is a particular term only made of numbers and + * - ? *)
-    val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option
-  end
-
-(* Currently, we only use Z numbers *)
-module Z : Int
diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg
deleted file mode 100644
index ac4f30b1db..0000000000
--- a/plugins/romega/g_romega.mlg
+++ /dev/null
@@ -1,63 +0,0 @@
-(*************************************************************************
-
-   PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
-   Licence : LGPL version 2.1
-
- *************************************************************************)
-
-
-DECLARE PLUGIN "romega_plugin"
-
-{
-
-open Ltac_plugin
-open Names
-open Refl_omega
-open Stdarg
-
-let eval_tactic name =
-  let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
-  let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in
-  let tac = Tacenv.interp_ltac kn in
-  Tacinterp.eval_tactic tac
-
-let romega_tactic unsafe l =
-  let tacs = List.map
-    (function
-       | "nat" -> eval_tactic "zify_nat"
-       | "positive" -> eval_tactic "zify_positive"
-       | "N" -> eval_tactic "zify_N"
-       | "Z" -> eval_tactic "zify_op"
-       | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s)))
-    (Util.List.sort_uniquize String.compare l)
-  in
-  Tacticals.New.tclTHEN
-    (Tacticals.New.tclREPEAT (Proofview.tclPROGRESS (Tacticals.New.tclTHENLIST tacs)))
-    (Tacticals.New.tclTHEN
-       (* because of the contradiction process in (r)omega,
-          we'd better leave as little as possible in the conclusion,
-          for an easier decidability argument. *)
-       (Tactics.intros)
-       (total_reflexive_omega_tactic unsafe))
-
-let romega_depr =
-  Vernacinterp.mk_deprecation
-    ~since:(Some "8.9")
-    ~note:(Some "Use lia instead.")
-    ()
-
-}
-
-TACTIC EXTEND romega
-DEPRECATED { romega_depr }
-|  [ "romega" ] -> { romega_tactic false [] }
-|  [ "unsafe_romega" ] -> { romega_tactic true [] }
-END
-
-TACTIC EXTEND romega'
-DEPRECATED { romega_depr }
-| [ "romega" "with" ne_ident_list(l) ] ->
-    { romega_tactic false (List.map Names.Id.to_string l) }
-| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] }
-END
diff --git a/plugins/romega/plugin_base.dune b/plugins/romega/plugin_base.dune
deleted file mode 100644
index 49b0e10edf..0000000000
--- a/plugins/romega/plugin_base.dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(library
- (name romega_plugin)
- (public_name coq.plugins.romega)
- (synopsis "Coq's romega plugin")
- (libraries coq.plugins.omega))
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
deleted file mode 100644
index 930048400a..0000000000
--- a/plugins/romega/refl_omega.ml
+++ /dev/null
@@ -1,1071 +0,0 @@
-(*************************************************************************
-
-   PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
-   Licence : LGPL version 2.1
-
- *************************************************************************)
-
-open Pp
-open Util
-open Constr
-open Const_omega
-module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
-open OmegaSolver
-
-module Id = Names.Id
-module IntSet = Int.Set
-module IntHtbl = Hashtbl.Make(Int)
-
-(* \section{Useful functions and flags} *)
-(* Especially useful debugging functions *)
-let debug = ref false
-
-let show_goal = Tacticals.New.tclIDTAC
-
-let pp i = print_int i; print_newline (); flush stdout
-
-(* More readable than the prefix notation *)
-let (>>) = Tacticals.New.tclTHEN
-
-(* \section{Types}
-  \subsection{How to walk in a term}
-  To represent how to get to a proposition. Only choice points are
-  kept (branch to choose in a disjunction  and identifier of the disjunctive
-  connector) *)
-type direction = Left of int | Right of int
-
-(* Step to find a proposition (operators are at most binary). A list is
-   a path *)
-type occ_step = O_left | O_right | O_mono
-type occ_path = occ_step list
-
-(* chemin identifiant une proposition sous forme du nom de l'hypothèse et
-   d'une liste de pas à partir de la racine de l'hypothèse *)
-type occurrence = {o_hyp : Id.t; o_path : occ_path}
-
-type atom_index = int
-
-(* \subsection{reifiable formulas} *)
-type oformula =
-    (* integer *)
-  | Oint of Bigint.bigint
-    (* recognized binary and unary operations *)
-  | Oplus of oformula * oformula
-  | Omult of oformula * oformula (* Invariant : one side is [Oint] *)
-  | Ominus of oformula * oformula
-  | Oopp of  oformula
-    (* an atom in the environment *)
-  | Oatom of atom_index
-
-(* Operators for comparison recognized by Omega *)
-type comparaison = Eq | Leq | Geq | Gt | Lt | Neq
-
-(* Representation of reified predicats (fragment of propositional calculus,
-   no quantifier here). *)
-(* Note : in [Pprop p], the non-reified constr [p] should be closed
-   (it could contains some [Term.Var] but no [Term.Rel]). So no need to
-   lift when breaking or creating arrows. *)
-type oproposition =
-    Pequa of EConstr.t * oequation (* constr = copy of the Coq formula *)
-  | Ptrue
-  | Pfalse
-  | Pnot of oproposition
-  | Por of int * oproposition * oproposition
-  | Pand of int * oproposition * oproposition
-  | Pimp of int * oproposition * oproposition
-  | Pprop of EConstr.t
-
-(* The equations *)
-and oequation = {
-    e_comp: comparaison;		(* comparaison *)
-    e_left: oformula;			(* formule brute gauche *)
-    e_right: oformula;			(* formule brute droite *)
-    e_origin: occurrence;		(* l'hypothèse dont vient le terme *)
-    e_negated: bool;			(* vrai si apparait en position nié
-					   après normalisation *)
-    e_depends: direction list;		(* liste des points de disjonction dont
-					   dépend l'accès à l'équation avec la
-					   direction (branche) pour y accéder *)
-    e_omega: OmegaSolver.afine (* normalized formula *)
-  }
-
-(* \subsection{Proof context}
-  This environment codes
-  \begin{itemize}
-  \item the terms and propositions that are given as
-  parameters of the reified proof (and are represented as variables in the
-  reified goals)
-  \item translation functions linking the decision procedure and the Coq proof
-  \end{itemize} *)
-
-type environment = {
-  (* La liste des termes non reifies constituant l'environnement global *)
-  mutable terms : EConstr.t list;
-  (* La meme chose pour les propositions *)
-  mutable props : EConstr.t list;
-  (* Traduction des indices utilisés ici en les indices finaux utilisés par
-   * la tactique Omega après dénombrement des variables utiles *)
-  real_indices : int IntHtbl.t;
-  mutable cnt_connectors : int;
-  equations : oequation IntHtbl.t;
-  constructors : occurrence IntHtbl.t
-}
-
-(* \subsection{Solution tree}
-   Définition d'une solution trouvée par Omega sous la forme d'un identifiant,
-   d'un ensemble d'équation dont dépend la solution et d'une trace *)
-
-type solution = {
-  s_index : int;
-  s_equa_deps : IntSet.t;
-  s_trace : OmegaSolver.action list }
-
-(* Arbre de solution résolvant complètement un ensemble de systèmes *)
-type solution_tree =
-    Leaf of solution
-    (* un noeud interne représente un point de branchement correspondant à
-       l'élimination d'un connecteur générant plusieurs buts
-       (typ. disjonction). Le premier argument
-       est l'identifiant du connecteur *)
-  | Tree of int * solution_tree * solution_tree
-
-(* Représentation de l'environnement extrait du but initial sous forme de
-   chemins pour extraire des equations ou d'hypothèses *)
-
-type context_content =
-    CCHyp of occurrence
-  | CCEqua of int
-
-(** Some dedicated equality tests *)
-
-let occ_step_eq s1 s2 = match s1, s2 with
-| O_left, O_left | O_right, O_right | O_mono, O_mono -> true
-| _ -> false
-
-let rec oform_eq f f' = match f,f' with
-  | Oint i, Oint i' -> Bigint.equal i i'
-  | Oplus (f1,f2), Oplus (f1',f2')
-  | Omult (f1,f2), Omult (f1',f2')
-  | Ominus (f1,f2), Ominus (f1',f2') -> oform_eq f1 f1' && oform_eq f2 f2'
-  | Oopp f, Oopp f' -> oform_eq f f'
-  | Oatom a, Oatom a' -> Int.equal a a'
-  | _ -> false
-
-let dir_eq d d' = match d, d' with
-  | Left i, Left i' | Right i, Right i' -> Int.equal i i'
-  | _ -> false
-
-(* \section{Specific utility functions to handle base types} *)
-(* Nom arbitraire de l'hypothèse codant la négation du but final *)
-let id_concl = Id.of_string "__goal__"
-
-(* Initialisation de l'environnement de réification de la tactique *)
-let new_environment () = {
-  terms = []; props = []; cnt_connectors = 0;
-  real_indices = IntHtbl.create 7;
-  equations = IntHtbl.create 7;
-  constructors = IntHtbl.create 7;
-}
-
-(* Génération d'un nom d'équation *)
-let new_connector_id env =
-   env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors
-
-(* Calcul de la branche complémentaire *)
-let barre = function Left x -> Right x | Right x -> Left x
-
-(* Identifiant associé à une branche *)
-let indice = function Left x | Right x -> x
-
-(* Affichage de l'environnement de réification (termes et propositions) *)
-let print_env_reification env =
-  let rec loop c i = function
-      [] ->  str "  ===============================\n\n"
-    | t :: l ->
-      let sigma, env = Pfedit.get_current_context () in
-      let s = Printf.sprintf "(%c%02d)" c i in
-      spc () ++ str s ++ str " := " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++
-      loop c (succ i) l
-  in
-  let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in
-  let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in
-  Feedback.msg_debug (prop_info ++ fnl () ++ term_info)
-
-(* \subsection{Gestion des environnements de variable pour Omega} *)
-(* generation d'identifiant d'equation pour Omega *)
-
-let new_omega_eq, rst_omega_eq =
-  let cpt = ref (-1) in
-  (function () -> incr cpt; !cpt),
-  (function () -> cpt:=(-1))
-
-(* generation d'identifiant de variable pour Omega *)
-
-let new_omega_var, rst_omega_var, set_omega_maxvar =
-  let cpt = ref (-1) in
-  (function () -> incr cpt; !cpt),
-  (function () -> cpt:=(-1)),
-  (function n -> cpt:=n)
-
-(* Affichage des variables d'un système *)
-
-let display_omega_var i = Printf.sprintf "OV%d" i
-
-(* \subsection{Gestion des environnements de variable pour la réflexion}
-   Gestion des environnements de traduction entre termes des constructions
-   non réifiés et variables des termes reifies. Attention il s'agit de
-   l'environnement initial contenant tout. Il faudra le réduire après
-   calcul des variables utiles. *)
-
-let add_reified_atom sigma t env =
-  try List.index0 (EConstr.eq_constr sigma) t env.terms
-  with Not_found ->
-    let i = List.length env.terms in
-    env.terms <- env.terms @ [t]; i
-
-let get_reified_atom env =
-  try List.nth env.terms with Invalid_argument _ -> failwith "get_reified_atom"
-
-(** When the omega resolution has created a variable [v], we re-sync
-    the environment with this new variable. To be done in the right order. *)
-
-let set_reified_atom v t env =
-  assert (Int.equal v (List.length env.terms));
-  env.terms <- env.terms @ [t]
-
-(* \subsection{Gestion de l'environnement de proposition pour Omega} *)
-(* ajout d'une proposition *)
-let add_prop sigma env t =
-  try List.index0 (EConstr.eq_constr sigma) t env.props
-  with Not_found ->
-    let i = List.length env.props in  env.props <- env.props @ [t]; i
-
-(* accès a une proposition *)
-let get_prop v env =
-  try List.nth v env with Invalid_argument _ -> failwith "get_prop"
-
-(* \subsection{Gestion du nommage des équations} *)
-(* Ajout d'une equation dans l'environnement de reification *)
-let add_equation env e =
-  let id = e.e_omega.id in
-  if IntHtbl.mem env.equations id then () else IntHtbl.add env.equations id e
-
-(* accès a une equation *)
-let get_equation env id =
-  try IntHtbl.find env.equations id
-  with Not_found as e ->
-    Printf.printf "Omega Equation %d non trouvée\n" id; raise e
-
-(* Affichage des termes réifiés *)
-let rec oprint ch = function
-  | Oint n -> Printf.fprintf ch "%s" (Bigint.to_string n)
-  | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2
-  | Omult (t1,t2) -> Printf.fprintf ch "(%a * %a)" oprint t1 oprint t2
-  | Ominus(t1,t2) -> Printf.fprintf ch "(%a - %a)" oprint t1 oprint t2
-  | Oopp t1 ->Printf.fprintf ch "~ %a" oprint t1
-  | Oatom n -> Printf.fprintf ch "V%02d" n
-
-let print_comp = function
-  | Eq -> "=" | Leq -> "<=" | Geq -> ">="
-  | Gt -> ">" | Lt -> "<" | Neq -> "!="
-
-let rec pprint ch = function
-    Pequa (_,{ e_comp=comp; e_left=t1; e_right=t2 })  ->
-      Printf.fprintf ch "%a %s %a" oprint t1 (print_comp comp) oprint t2
-  | Ptrue -> Printf.fprintf ch "TT"
-  | Pfalse -> Printf.fprintf ch "FF"
-  | Pnot t -> Printf.fprintf ch "not(%a)" pprint t
-  | Por (_,t1,t2) -> Printf.fprintf ch "(%a or %a)" pprint t1 pprint t2
-  | Pand(_,t1,t2) -> Printf.fprintf ch "(%a and %a)" pprint t1 pprint t2
-  | Pimp(_,t1,t2) -> Printf.fprintf ch "(%a => %a)" pprint t1 pprint t2
-  | Pprop c -> Printf.fprintf ch "Prop"
-
-(* \subsection{Omega vers Oformula} *)
-
-let oformula_of_omega af =
-  let rec loop = function
-    | ({v=v; c=n}::r) -> Oplus(Omult(Oatom v,Oint n),loop r)
-    | [] -> Oint af.constant
-  in
-  loop af.body
-
-let app f v = EConstr.mkApp(Lazy.force f,v)
-
-(* \subsection{Oformula vers COQ reel} *)
-
-let coq_of_formula env t =
-  let rec loop = function
-  | Oplus (t1,t2) -> app Z.plus [| loop t1; loop t2 |]
-  | Oopp t -> app Z.opp [| loop t |]
-  | Omult(t1,t2) -> app Z.mult [| loop t1; loop t2 |]
-  | Oint v ->   Z.mk v
-  | Oatom var ->
-      (* attention ne traite pas les nouvelles variables si on ne les
-       * met pas dans env.term *)
-      get_reified_atom env var
-  | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in
-  loop t
-
-(* \subsection{Oformula vers COQ reifié} *)
-
-let reified_of_atom env i =
-  try IntHtbl.find env.real_indices i
-  with Not_found ->
-    Printf.printf "Atome %d non trouvé\n" i;
-    IntHtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices;
-    raise Not_found
-
-let reified_binop = function
-  | Oplus _ -> app coq_t_plus
-  | Ominus _ -> app coq_t_minus
-  | Omult _ -> app coq_t_mult
-  | _ -> assert false
-
-let rec reified_of_formula env t = match t with
-  | Oplus (t1,t2) | Omult (t1,t2) | Ominus (t1,t2) ->
-     reified_binop t [| reified_of_formula env t1; reified_of_formula env t2 |]
-  | Oopp t -> app coq_t_opp [| reified_of_formula env t |]
-  | Oint v -> app coq_t_int [| Z.mk v |]
-  | Oatom i -> app coq_t_var [| mk_N (reified_of_atom env i) |]
-
-let reified_of_formula env f =
-  try reified_of_formula env f
-  with reraise -> oprint stderr f; raise reraise
-
-let reified_cmp = function
-  | Eq -> app coq_p_eq
-  | Leq -> app coq_p_leq
-  | Geq -> app coq_p_geq
-  | Gt -> app coq_p_gt
-  | Lt -> app coq_p_lt
-  | Neq -> app coq_p_neq
-
-let reified_conn = function
-  | Por _ -> app coq_p_or
-  | Pand _ -> app coq_p_and
-  | Pimp _ -> app coq_p_imp
-  | _ -> assert false
-
-let rec reified_of_oprop sigma env t = match t with
-  | Pequa (_,{ e_comp=cmp; e_left=t1; e_right=t2 }) ->
-     reified_cmp cmp [| reified_of_formula env t1; reified_of_formula env t2 |]
-  | Ptrue -> Lazy.force coq_p_true
-  | Pfalse -> Lazy.force coq_p_false
-  | Pnot t -> app coq_p_not [| reified_of_oprop sigma env t |]
-  | Por (_,t1,t2) | Pand (_,t1,t2) | Pimp (_,t1,t2) ->
-     reified_conn t
-      [| reified_of_oprop sigma env t1; reified_of_oprop sigma env t2 |]
-  | Pprop t -> app coq_p_prop [| mk_nat (add_prop sigma env t) |]
-
-let reified_of_proposition sigma env f =
-  try reified_of_oprop sigma env f
-  with reraise -> pprint stderr f; raise reraise
-
-let reified_of_eq env (l,r) =
-  app coq_p_eq [| reified_of_formula env l; reified_of_formula env r |]
-
-(* \section{Opérations sur les équations}
-Ces fonctions préparent les traces utilisées par la tactique réfléchie
-pour faire des opérations de normalisation sur les équations.  *)
-
-(* \subsection{Extractions des variables d'une équation} *)
-(* Extraction des variables d'une équation. *)
-(* Chaque fonction retourne une liste triée sans redondance *)
-
-let (@@) = IntSet.union
-
-let rec vars_of_formula = function
-  | Oint _ -> IntSet.empty
-  | Oplus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
-  | Omult (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
-  | Ominus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
-  | Oopp e -> vars_of_formula e
-  | Oatom i -> IntSet.singleton i
-
-let rec vars_of_equations = function
-  | [] -> IntSet.empty
-  | e::l ->
-      (vars_of_formula e.e_left) @@
-      (vars_of_formula e.e_right) @@
-      (vars_of_equations l)
-
-let rec vars_of_prop = function
-  | Pequa(_,e) -> vars_of_equations [e]
-  | Pnot p -> vars_of_prop p
-  | Por(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
-  | Pand(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
-  | Pimp(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
-  | Pprop _ | Ptrue | Pfalse -> IntSet.empty
-
-(* Normalized formulas :
-
-   - sorted list of monomials, largest index first,
-     with non-null coefficients
-   - a constant coefficient
-
-   /!\ Keep in sync with the corresponding functions in ReflOmegaCore !
-*)
-
-type nformula =
-  { coefs : (atom_index * Bigint.bigint) list;
-    cst : Bigint.bigint }
-
-let scale n { coefs; cst } =
-  { coefs = List.map (fun (v,k) -> (v,k*n)) coefs;
-    cst = cst*n }
-
-let shuffle nf1 nf2 =
-  let rec merge l1 l2 = match l1,l2 with
-    | [],_ -> l2
-    | _,[] -> l1
-    | (v1,k1)::r1,(v2,k2)::r2 ->
-       if Int.equal v1 v2 then
-         let k = k1+k2 in
-         if Bigint.equal k Bigint.zero then merge r1 r2
-         else (v1,k) :: merge r1 r2
-       else if v1 > v2 then (v1,k1) :: merge r1 l2
-       else (v2,k2) :: merge l1 r2
-  in
-  { coefs = merge nf1.coefs nf2.coefs;
-    cst = nf1.cst + nf2.cst }
-
-let rec normalize = function
-  | Oplus(t1,t2) -> shuffle (normalize t1) (normalize t2)
-  | Ominus(t1,t2) -> normalize (Oplus (t1, Oopp(t2)))
-  | Oopp(t) -> scale negone (normalize t)
-  | Omult(t,Oint n) | Omult (Oint n, t) ->
-     if Bigint.equal n Bigint.zero then { coefs = []; cst = zero }
-     else scale n (normalize t)
-  | Omult _ -> assert false (* invariant on Omult *)
-  | Oint n -> { coefs = []; cst = n }
-  | Oatom v -> { coefs = [v,Bigint.one]; cst=Bigint.zero}
-
-(* From normalized formulas to omega representations *)
-
-let omega_of_nformula env kind nf =
-  { id = new_omega_eq ();
-    kind;
-    constant=nf.cst;
-    body = List.map (fun (v,c) -> { v; c }) nf.coefs }
-
-
-let negate_oper = function
-    Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq
-
-let normalize_equation env (negated,depends,origin,path) oper t1 t2 =
-  let mk_step t kind =
-    let equa = omega_of_nformula env kind (normalize t) in
-    { e_comp = oper; e_left = t1; e_right = t2;
-      e_negated = negated; e_depends = depends;
-      e_origin = { o_hyp = origin; o_path = List.rev path };
-      e_omega = equa }
-  in
-  try match (if negated then (negate_oper oper) else oper) with
-    | Eq  -> mk_step (Oplus (t1,Oopp t2)) EQUA
-    | Neq -> mk_step (Oplus (t1,Oopp t2)) DISE
-    | Leq -> mk_step (Oplus (t2,Oopp t1)) INEQ
-    | Geq -> mk_step (Oplus (t1,Oopp t2)) INEQ
-    | Lt  -> mk_step (Oplus (Oplus(t2,Oint negone),Oopp t1)) INEQ
-    | Gt -> mk_step (Oplus (Oplus(t1,Oint negone),Oopp t2)) INEQ
-  with e when Logic.catchable_exception e -> raise e
-
-(* \section{Compilation des hypothèses} *)
-
-let mkPor i x y = Por (i,x,y)
-let mkPand i x y = Pand (i,x,y)
-let mkPimp i x y = Pimp (i,x,y)
-
-let rec oformula_of_constr sigma env t =
-  match Z.parse_term sigma t with
-    | Tplus (t1,t2) -> binop sigma env (fun x y -> Oplus(x,y)) t1 t2
-    | Tminus (t1,t2) -> binop sigma env (fun x y -> Ominus(x,y)) t1 t2
-    | Tmult (t1,t2) ->
-       (match Z.get_scalar sigma t1 with
-        | Some n -> Omult (Oint n,oformula_of_constr sigma env t2)
-        | None ->
-           match Z.get_scalar sigma t2 with
-           | Some n -> Omult (oformula_of_constr sigma env t1, Oint n)
-           | None -> Oatom (add_reified_atom sigma t env))
-    | Topp t -> Oopp(oformula_of_constr sigma env t)
-    | Tsucc t -> Oplus(oformula_of_constr sigma env t, Oint one)
-    | Tnum n -> Oint n
-    | Tother -> Oatom (add_reified_atom sigma t env)
-
-and binop sigma env c t1 t2 =
-  let t1' = oformula_of_constr sigma env t1 in
-  let t2' = oformula_of_constr sigma env t2 in
-  c t1' t2'
-
-and binprop sigma env (neg2,depends,origin,path)
-             add_to_depends neg1 gl c t1 t2 =
-  let i = new_connector_id env in
-  let depends1 = if add_to_depends then Left i::depends else depends in
-  let depends2 = if add_to_depends then Right i::depends else depends in
-  if add_to_depends then
-    IntHtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path};
-  let t1' =
-    oproposition_of_constr sigma env (neg1,depends1,origin,O_left::path) gl t1 in
-  let t2' =
-    oproposition_of_constr sigma env (neg2,depends2,origin,O_right::path) gl t2 in
-  (* On numérote le connecteur dans l'environnement. *)
-  c i t1' t2'
-
-and mk_equation sigma env ctxt c connector t1 t2 =
-  let t1' = oformula_of_constr sigma env t1 in
-  let t2' = oformula_of_constr sigma env t2 in
-  (* On ajoute l'equation dans l'environnement. *)
-  let omega = normalize_equation env ctxt connector t1' t2' in
-  add_equation env omega;
-  Pequa (c,omega)
-
-and oproposition_of_constr sigma env ((negated,depends,origin,path) as ctxt) gl c =
-  match Z.parse_rel gl c with
-    | Req (t1,t2) -> mk_equation sigma env ctxt c Eq t1 t2
-    | Rne (t1,t2) -> mk_equation sigma env ctxt c Neq t1 t2
-    | Rle (t1,t2) -> mk_equation sigma env ctxt c Leq t1 t2
-    | Rlt (t1,t2) -> mk_equation sigma env ctxt c Lt t1 t2
-    | Rge (t1,t2) -> mk_equation sigma env ctxt c Geq t1 t2
-    | Rgt (t1,t2) -> mk_equation sigma env ctxt c Gt t1 t2
-    | Rtrue -> Ptrue
-    | Rfalse -> Pfalse
-    | Rnot t ->
-       let ctxt' = (not negated, depends, origin,(O_mono::path)) in
-       Pnot (oproposition_of_constr sigma env ctxt' gl t)
-    | Ror (t1,t2) -> binprop sigma env ctxt (not negated) negated gl mkPor t1 t2
-    | Rand (t1,t2) -> binprop sigma env ctxt negated negated gl mkPand t1 t2
-    | Rimp (t1,t2) ->
-       binprop sigma env ctxt (not negated) (not negated) gl mkPimp t1 t2
-    | Riff (t1,t2) ->
-       (* No lifting here, since Omega only works on closed propositions. *)
-       binprop sigma env ctxt negated negated gl mkPand
-         (EConstr.mkArrow t1 t2) (EConstr.mkArrow t2 t1)
-    | _ -> Pprop c
-
-(* Destructuration des hypothèses et de la conclusion *)
-
-let display_gl env t_concl t_lhyps =
-  Printf.printf "REIFED PROBLEM\n\n";
-  Printf.printf "  CONCL: %a\n" pprint t_concl;
-  List.iter
-    (fun (i,_,t) -> Printf.printf "  %s: %a\n" (Id.to_string i) pprint t)
-    t_lhyps;
-  print_env_reification env
-
-type defined = Defined | Assumed
-
-let reify_hyp sigma env gl i =
-  let open Context.Named.Declaration in
-  let ctxt = (false,[],i,[]) in
-  match Tacmach.New.pf_get_hyp i gl with
-  | LocalDef (_,d,t) when Z.is_int_typ gl t ->
-     let dummy = Lazy.force coq_True in
-     let p = mk_equation sigma env ctxt dummy Eq (EConstr.mkVar i) d in
-     i,Defined,p
-  | LocalDef (_,_,t) | LocalAssum (_,t) ->
-     let p = oproposition_of_constr sigma env ctxt gl t in
-     i,Assumed,p
-
-let reify_gl env gl =
-  let sigma = Proofview.Goal.sigma gl in
-  let concl = Tacmach.New.pf_concl gl in
-  let hyps = Tacmach.New.pf_ids_of_hyps gl in
-  let ctxt_concl = (true,[],id_concl,[O_mono]) in
-  let t_concl = oproposition_of_constr sigma env ctxt_concl gl concl in
-  let t_lhyps = List.map (reify_hyp sigma env gl) hyps in
-  let () = if !debug then display_gl env t_concl t_lhyps in
-  t_concl, t_lhyps
-
-let rec destruct_pos_hyp eqns = function
-  | Pequa (_,e) -> [e :: eqns]
-  | Ptrue | Pfalse | Pprop _ -> [eqns]
-  | Pnot t -> destruct_neg_hyp eqns t
-  | Por (_,t1,t2) ->
-      let s1 = destruct_pos_hyp eqns t1 in
-      let s2 = destruct_pos_hyp eqns t2 in
-      s1 @ s2
-  | Pand(_,t1,t2) ->
-      List.map_append
-        (fun le1 -> destruct_pos_hyp le1 t2)
-        (destruct_pos_hyp eqns t1)
-  | Pimp(_,t1,t2) ->
-      let s1 = destruct_neg_hyp eqns t1 in
-      let s2 = destruct_pos_hyp eqns t2 in
-      s1 @ s2
-
-and destruct_neg_hyp eqns = function
-  | Pequa (_,e) -> [e :: eqns]
-  | Ptrue | Pfalse | Pprop _ -> [eqns]
-  | Pnot t -> destruct_pos_hyp eqns t
-  | Pand (_,t1,t2) ->
-      let s1 = destruct_neg_hyp eqns t1 in
-      let s2 = destruct_neg_hyp eqns t2 in
-      s1 @ s2
-  | Por(_,t1,t2) ->
-      List.map_append
-        (fun le1 -> destruct_neg_hyp le1 t2)
-        (destruct_neg_hyp eqns t1)
-  | Pimp(_,t1,t2) ->
-      List.map_append
-        (fun le1 -> destruct_neg_hyp le1 t2)
-        (destruct_pos_hyp eqns t1)
-
-let rec destructurate_hyps = function
-  | [] -> [[]]
-  | (i,_,t) :: l ->
-     let l_syst1 = destruct_pos_hyp [] t in
-     let l_syst2 = destructurate_hyps l in
-     List.cartesian (@) l_syst1 l_syst2
-
-(* \subsection{Affichage d'un système d'équation} *)
-
-(* Affichage des dépendances de système *)
-let display_depend = function
-    Left i -> Printf.printf " L%d" i
-  | Right i -> Printf.printf " R%d" i
-
-let display_systems syst_list =
-  let display_omega om_e =
-    Printf.printf "  E%d : %a %s 0\n"
-      om_e.id
-      (fun _ -> display_eq display_omega_var)
-      (om_e.body, om_e.constant)
-      (operator_of_eq om_e.kind) in
-
-  let display_equation oformula_eq =
-    pprint stdout (Pequa (Lazy.force coq_I,oformula_eq)); print_newline ();
-    display_omega oformula_eq.e_omega;
-    Printf.printf "  Depends on:";
-    List.iter display_depend oformula_eq.e_depends;
-    Printf.printf "\n  Path: %s"
-      (String.concat ""
-	 (List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M")
-	    oformula_eq.e_origin.o_path));
-    Printf.printf "\n  Origin: %s (negated : %s)\n\n"
-      (Id.to_string oformula_eq.e_origin.o_hyp)
-      (if oformula_eq.e_negated then "yes" else "no") in
-
-  let display_system syst =
-    Printf.printf "=SYSTEM===================================\n";
-    List.iter display_equation syst in
-  List.iter display_system syst_list
-
-(* Extraction des prédicats utilisées dans une trace. Permet ensuite le
-   calcul des hypothèses *)
-
-let rec hyps_used_in_trace = function
-  | [] -> IntSet.empty
-  | act :: l ->
-     match act with
-     | HYP e -> IntSet.add e.id (hyps_used_in_trace l)
-     | SPLIT_INEQ (_,(_,act1),(_,act2)) ->
-        hyps_used_in_trace act1 @@ hyps_used_in_trace act2
-     | _ -> hyps_used_in_trace l
-
-(** Retreive variables declared as extra equations during resolution
-    and declare them into the environment.
-    We should consider these variables in their introduction order,
-    otherwise really bad things will happen. *)
-
-let state_cmp x y = Int.compare x.st_var y.st_var
-
-module StateSet =
-  Set.Make (struct type t = state_action let compare = state_cmp end)
-
-let rec stated_in_trace = function
-  | [] -> StateSet.empty
-  | [SPLIT_INEQ (_,(_,t1),(_,t2))] ->
-     StateSet.union (stated_in_trace t1) (stated_in_trace t2)
-  | STATE action :: l -> StateSet.add action (stated_in_trace l)
-  | _ :: l -> stated_in_trace l
-
-let rec stated_in_tree = function
-  | Tree(_,t1,t2) -> StateSet.union (stated_in_tree t1) (stated_in_tree t2)
-  | Leaf s -> stated_in_trace s.s_trace
-
-let mk_refl t = app coq_refl_equal [|Lazy.force Z.typ; t|]
-
-let digest_stated_equations env tree =
-  let do_equation st (vars,gens,eqns,ids) =
-    (** We turn the definition of [v]
-        - into a reified formula : *)
-    let v_def = oformula_of_omega st.st_def in
-    (** - into a concrete Coq formula
-          (this uses only older vars already in env) : *)
-    let coq_v = coq_of_formula env v_def in
-    (** We then update the environment *)
-    set_reified_atom st.st_var coq_v env;
-    (** The term we'll introduce *)
-    let term_to_generalize = mk_refl coq_v in
-    (** Its representation as equation (but not reified yet,
-        we lack the proper env to do that). *)
-    let term_to_reify = (v_def,Oatom st.st_var) in
-    (st.st_var::vars,
-     term_to_generalize::gens,
-     term_to_reify::eqns,
-     CCEqua st.st_def.id :: ids)
-  in
-  let (vars,gens,eqns,ids) =
-    StateSet.fold do_equation (stated_in_tree tree) ([],[],[],[])
-  in
-  (List.rev vars, List.rev gens, List.rev eqns, List.rev ids)
-
-(* Calcule la liste des éclatements à réaliser sur les hypothèses
-   nécessaires pour extraire une liste d'équations donnée *)
-
-(* PL: experimentally, the result order of the following function seems
-   _very_ crucial for efficiency. No idea why. Do not remove the List.rev
-   or modify the current semantics of Util.List.union (some elements of first
-   arg, then second arg), unless you know what you're doing. *)
-
-let rec get_eclatement env = function
-  | [] -> []
-  | i :: r ->
-     let l = try (get_equation env i).e_depends with Not_found -> [] in
-     List.union dir_eq (List.rev l) (get_eclatement env r)
-
-let select_smaller l =
-  let comp (_,x) (_,y) = Int.compare (List.length x) (List.length y) in
-  try List.hd (List.sort comp l) with Failure _ -> failwith "select_smaller"
-
-let filter_compatible_systems required systems =
-  let rec select = function
-    | [] -> []
-    | (x::l) ->
-       if List.mem_f dir_eq x required then select l
-       else if List.mem_f dir_eq (barre x) required then raise Exit
-       else x :: select l
-  in
-  List.map_filter
-    (function (sol, splits) ->
-      try Some (sol, select splits) with Exit -> None)
-    systems
-
-let rec equas_of_solution_tree = function
-  | Tree(_,t1,t2) ->
-     (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)
-  | Leaf s -> s.s_equa_deps
-
-(** [maximize_prop] pushes useless props in a new Pprop atom.
-  The reified formulas get shorter, but be careful with decidabilities.
-  For instance, anything that contains a Pprop is considered to be
-  undecidable in [ReflOmegaCore], whereas a Pfalse for instance at
-  the same spot will lead to a decidable formula.
-  In particular, do not use this function on the conclusion.
-  Even in hypotheses, we could probably build pathological examples
-  that romega won't handle correctly, but they should be pretty rare.
-*)
-
-let maximize_prop equas c =
-  let rec loop c = match c with
-    | Pequa(t,e) -> if IntSet.mem e.e_omega.id equas then c else Pprop t
-    | Pnot t ->
-       (match loop t with
-        | Pprop p -> Pprop (app coq_not [|p|])
-        | t' -> Pnot t')
-    | Por(i,t1,t2) ->
-       (match loop t1, loop t2 with
-        | Pprop p1, Pprop p2 -> Pprop (app coq_or [|p1;p2|])
-        | t1', t2' -> Por(i,t1',t2'))
-    | Pand(i,t1,t2) ->
-       (match loop t1, loop t2 with
-        | Pprop p1, Pprop p2 -> Pprop (app coq_and [|p1;p2|])
-        | t1', t2' -> Pand(i,t1',t2'))
-    | Pimp(i,t1,t2) ->
-       (match loop t1, loop t2 with
-        | Pprop p1, Pprop p2 -> Pprop (EConstr.mkArrow p1 p2) (* no lift (closed) *)
-        | t1', t2' -> Pimp(i,t1',t2'))
-    | Ptrue -> Pprop (app coq_True [||])
-    | Pfalse -> Pprop (app coq_False [||])
-    | Pprop _ -> c
-  in loop c
-
-let rec display_solution_tree ch = function
-    Leaf t ->
-      output_string ch
-       (Printf.sprintf "%d[%s]"
-         t.s_index
-         (String.concat " " (List.map string_of_int
-                                      (IntSet.elements t.s_equa_deps))))
-  | Tree(i,t1,t2) ->
-      Printf.fprintf ch "S%d(%a,%a)" i
-	display_solution_tree t1 display_solution_tree t2
-
-let rec solve_with_constraints all_solutions path =
-  let rec build_tree sol buf = function
-      [] -> Leaf sol
-    | (Left i :: remainder) ->
-	Tree(i,
-	     build_tree sol (Left i :: buf) remainder,
-	     solve_with_constraints all_solutions (List.rev(Right i :: buf)))
-    | (Right i :: remainder) ->
-	 Tree(i,
-	      solve_with_constraints all_solutions (List.rev (Left i ::  buf)),
-	      build_tree sol (Right i :: buf) remainder) in
-  let weighted = filter_compatible_systems path all_solutions in
-  let (winner_sol,winner_deps) =
-    try select_smaller weighted
-    with reraise ->
-      Printf.printf "%d - %d\n"
-	(List.length weighted) (List.length all_solutions);
-      List.iter display_depend path; raise reraise
-  in
-  build_tree winner_sol (List.rev path) winner_deps
-
-let find_path {o_hyp=id;o_path=p} env =
-  let rec loop_path = function
-      ([],l) -> Some l
-    | (x1::l1,x2::l2) when occ_step_eq x1 x2 -> loop_path (l1,l2)
-    | _ -> None in
-  let rec loop_id i = function
-      CCHyp{o_hyp=id';o_path=p'} :: l when Id.equal id id' ->
-	begin match loop_path (p',p) with
-	  Some r -> i,r
-	| None -> loop_id (succ i) l
-	end
-    | _ :: l -> loop_id (succ i) l
-    | [] -> failwith "find_path" in
-  loop_id 0 env
-
-let mk_direction_list l =
-  let trans = function
-    | O_left -> Some (Lazy.force coq_d_left)
-    | O_right -> Some (Lazy.force coq_d_right)
-    | O_mono -> None (* No more [D_mono] constructor now *)
-  in
-  mk_list (Lazy.force coq_direction) (List.map_filter trans l)
-
-
-(* \section{Rejouer l'historique} *)
-
-let hyp_idx env_hyp i =
-  let rec loop count = function
-    | [] -> failwith (Printf.sprintf "get_hyp %d" i)
-    | CCEqua i' :: _ when Int.equal i i' -> mk_nat count
-    | _ :: l -> loop (succ count) l
-  in loop 0 env_hyp
-
-
-(* We now expand NEGATE_CONTRADICT and CONTRADICTION into
-   a O_SUM followed by a O_BAD_CONSTANT *)
-
-let sum_bad inv i1 i2 =
-  let open EConstr in
-  mkApp (Lazy.force coq_s_sum,
-         [| Z.mk Bigint.one; i1;
-            Z.mk (if inv then negone else Bigint.one); i2;
-            mkApp (Lazy.force coq_s_bad_constant, [| mk_nat 0 |])|])
-
-let rec reify_trace env env_hyp =
-  let open EConstr in
-  function
-  | CONSTANT_NOT_NUL(e,_) :: []
-  | CONSTANT_NEG(e,_) :: []
-  | CONSTANT_NUL e :: [] ->
-     mkApp (Lazy.force coq_s_bad_constant,[| hyp_idx env_hyp e |])
-  | NEGATE_CONTRADICT(e1,e2,direct) :: [] ->
-     sum_bad direct (hyp_idx env_hyp e1.id) (hyp_idx env_hyp e2.id)
-  | CONTRADICTION (e1,e2) :: [] ->
-     sum_bad false (hyp_idx env_hyp e1.id) (hyp_idx env_hyp e2.id)
-  | NOT_EXACT_DIVIDE (e1,k) :: [] ->
-     mkApp (Lazy.force coq_s_not_exact_divide,
-            [| hyp_idx env_hyp e1.id; Z.mk k |])
-  | DIVIDE_AND_APPROX (e1,_,k,_) :: l
-  | EXACT_DIVIDE (e1,k) :: l ->
-     mkApp (Lazy.force coq_s_divide,
-            [| hyp_idx env_hyp e1.id; Z.mk k;
-               reify_trace env env_hyp l |])
-  | MERGE_EQ(e3,e1,e2) :: l ->
-     mkApp (Lazy.force coq_s_merge_eq,
-            [| hyp_idx env_hyp e1.id; hyp_idx env_hyp e2;
-               reify_trace env (CCEqua e3:: env_hyp) l |])
-  | SUM(e3,(k1,e1),(k2,e2)) :: l ->
-     mkApp (Lazy.force coq_s_sum,
-            [| Z.mk k1; hyp_idx env_hyp e1.id;
-               Z.mk k2; hyp_idx env_hyp e2.id;
-               reify_trace env (CCEqua e3 :: env_hyp) l |])
-  | STATE {st_new_eq; st_def; st_orig; st_coef } :: l ->
-     (* we now produce a [O_SUM] here *)
-     mkApp (Lazy.force coq_s_sum,
-            [| Z.mk Bigint.one; hyp_idx env_hyp st_orig.id;
-               Z.mk st_coef; hyp_idx env_hyp st_def.id;
-               reify_trace env (CCEqua st_new_eq.id :: env_hyp) l |])
-  | HYP _ :: l -> reify_trace env env_hyp l
-  | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: _ ->
-     let r1 = reify_trace env (CCEqua e1 :: env_hyp) l1 in
-     let r2 = reify_trace env (CCEqua e2 :: env_hyp) l2 in
-     mkApp (Lazy.force coq_s_split_ineq,
-            [| hyp_idx env_hyp e.id; r1 ; r2 |])
-  | (FORGET_C _ | FORGET _ | FORGET_I _) :: l -> reify_trace env env_hyp l
-  | WEAKEN  _ :: l -> failwith "not_treated"
-  | _ -> failwith "bad history"
-
-let rec decompose_tree env ctxt = function
-   Tree(i,left,right) ->
-     let org =
-       try IntHtbl.find env.constructors i
-       with Not_found ->
-	 failwith (Printf.sprintf "Cannot find constructor %d" i) in
-     let (index,path) = find_path org ctxt in
-     let left_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_left]} in
-     let right_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_right]} in
-     app coq_e_split
-       [| mk_nat index;
-	  mk_direction_list path;
-	  decompose_tree env (left_hyp::ctxt) left;
-	  decompose_tree env (right_hyp::ctxt) right |]
-  | Leaf s ->
-      decompose_tree_hyps s.s_trace env ctxt (IntSet.elements s.s_equa_deps)
-and decompose_tree_hyps trace env ctxt = function
-    [] -> app coq_e_solve [| reify_trace env ctxt trace |]
-  | (i::l) ->
-      let equation =
-        try IntHtbl.find env.equations i
-        with Not_found ->
-	  failwith (Printf.sprintf "Cannot find equation %d" i) in
-      let (index,path) = find_path equation.e_origin ctxt in
-      let cont =
-	decompose_tree_hyps trace env
-	   (CCEqua equation.e_omega.id :: ctxt) l in
-      app coq_e_extract [|mk_nat index; mk_direction_list path; cont |]
-
-let solve_system env index list_eq =
-  let system = List.map (fun eq -> eq.e_omega) list_eq in
-  let trace =
-    OmegaSolver.simplify_strong
-      (new_omega_eq,new_omega_var,display_omega_var)
-      system
-  in
-  (* Hypotheses used for this solution *)
-  let vars = hyps_used_in_trace trace in
-  let splits = get_eclatement env (IntSet.elements vars) in
-  if !debug then
-    begin
-      Printf.printf "SYSTEME %d\n" index;
-      display_action display_omega_var trace;
-      print_string "\n  Depend :";
-      IntSet.iter (fun i -> Printf.printf " %d" i) vars;
-      print_string "\n  Split points :";
-      List.iter display_depend splits;
-      Printf.printf "\n------------------------------------\n"
-    end;
-  {s_index = index; s_trace = trace; s_equa_deps = vars}, splits
-
-(* \section{La fonction principale} *)
- (* Cette fonction construit la
-trace pour la procédure de décision réflexive.  A partir des résultats
-de l'extraction des systèmes, elle lance la résolution par Omega, puis
-l'extraction d'un ensemble minimal de solutions permettant la
-résolution globale du système et enfin construit la trace qui permet
-de faire rejouer cette solution par la tactique réflexive. *)
-
-let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list =
-  if !debug then Printf.printf "\n====================================\n";
-  let all_solutions = List.mapi (solve_system env) systems_list in
-  let solution_tree = solve_with_constraints all_solutions [] in
-  if !debug then  begin
-    display_solution_tree stdout solution_tree;
-    print_newline()
-  end;
-  (** Collect all hypotheses and variables used in the solution tree *)
-  let useful_equa_ids = equas_of_solution_tree solution_tree in
-  let useful_hypnames, useful_vars =
-    IntSet.fold
-      (fun i (hyps,vars) ->
-        let e = get_equation env i in
-        Id.Set.add e.e_origin.o_hyp hyps,
-        vars_of_equations [e] @@ vars)
-      useful_equa_ids
-      (Id.Set.empty, vars_of_prop reified_concl)
-  in
-  let useful_hypnames =
-    Id.Set.elements (Id.Set.remove id_concl useful_hypnames)
-  in
-
-  (** Parts coming from equations introduced by omega: *)
-  let stated_vars, l_generalize_arg, to_reify_stated, hyp_stated_vars =
-    digest_stated_equations env solution_tree
-  in
-  (** The final variables are either coming from:
-     - useful hypotheses (and conclusion)
-     - equations introduced during resolution *)
-  let all_vars_env = (IntSet.elements useful_vars) @ stated_vars
-  in
-  (** We prepare the renumbering from all variables to useful ones.
-      Since [all_var_env] is sorted, this renumbering will preserve
-      order: this way, the equations in ReflOmegaCore will have
-      the same normal forms as here. *)
-  let reduced_term_env =
-    let rec loop i = function
-      | [] -> []
-      | var :: l ->
-         let t = get_reified_atom env var in
-         IntHtbl.add env.real_indices var i; t :: loop (succ i) l
-    in
-    mk_list (Lazy.force Z.typ) (loop 0 all_vars_env)
-  in
-  (** The environment [env] (and especially [env.real_indices]) is now
-      ready for the coming reifications: *)
-  let l_reified_stated = List.map (reified_of_eq env) to_reify_stated in
-  let reified_concl = reified_of_proposition sigma env reified_concl in
-  let l_reified_terms =
-    List.map
-      (fun id ->
-        match Id.Map.find id reified_hyps with
-        | Defined,p ->
-           reified_of_proposition sigma env p, mk_refl (EConstr.mkVar id)
-        | Assumed,p ->
-           reified_of_proposition sigma env (maximize_prop useful_equa_ids p),
-           EConstr.mkVar id
-        | exception Not_found -> assert false)
-      useful_hypnames
-  in
-  let l_reified_terms, l_reified_hypnames = List.split l_reified_terms in
-  let env_props_reified = mk_plist env.props in
-  let reified_goal =
-    mk_list (Lazy.force coq_proposition)
-            (l_reified_stated @ l_reified_terms) in
-  let reified =
-    app coq_interp_sequent
-       [| reified_concl;env_props_reified;reduced_term_env;reified_goal|]
-  in
-  let mk_occ id = {o_hyp=id;o_path=[]} in
-  let initial_context =
-    List.map (fun id -> CCHyp (mk_occ id)) useful_hypnames in
-  let context =
-    CCHyp (mk_occ id_concl) :: hyp_stated_vars @ initial_context in
-  let decompose_tactic = decompose_tree env context solution_tree in
-
-  Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >>
-  Tactics.convert_concl_no_check reified DEFAULTcast >>
-  Tactics.apply (app coq_do_omega [|decompose_tactic|]) >>
-  show_goal >>
-  (if unsafe then
-     (* Trust the produced term. Faster, but might fail later at Qed.
-        Also handy when debugging, e.g. via a Show Proof after romega. *)
-     Tactics.convert_concl_no_check (Lazy.force coq_True) VMcast
-   else
-     Tactics.normalise_vm_in_concl) >>
-  Tactics.apply (Lazy.force coq_I)
-
-let total_reflexive_omega_tactic unsafe =
-  Proofview.Goal.enter begin fun gl ->
-  Coqlib.check_required_library ["Coq";"romega";"ROmega"];
-  rst_omega_eq ();
-  rst_omega_var ();
-  try
-  let env = new_environment () in
-  let (concl,hyps) = reify_gl env gl in
-  (* Register all atom indexes created during reification as omega vars *)
-  set_omega_maxvar (pred (List.length env.terms));
-  let full_reified_goal = (id_concl,Assumed,Pnot concl) :: hyps in
-  let systems_list = destructurate_hyps full_reified_goal in
-  let hyps =
-    List.fold_left (fun s (id,d,p) -> Id.Map.add id (d,p) s) Id.Map.empty hyps
-  in
-  if !debug then display_systems systems_list;
-  let sigma = Proofview.Goal.sigma gl in
-  resolution unsafe sigma env (concl,hyps) systems_list
-  with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system")
-  end
-
diff --git a/plugins/romega/romega_plugin.mlpack b/plugins/romega/romega_plugin.mlpack
deleted file mode 100644
index 38d0e94111..0000000000
--- a/plugins/romega/romega_plugin.mlpack
+++ /dev/null
@@ -1,3 +0,0 @@
-Const_omega
-Refl_omega
-G_romega
diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v
index 1507fa4bf0..bd9bac37ef 100644
--- a/test-suite/bugs/closed/4717.v
+++ b/test-suite/bugs/closed/4717.v
@@ -19,8 +19,6 @@ Proof.
   omega.
 Qed.
 
-Require Import ZArith ROmega.
-
 Open Scope Z_scope.
 
 Definition Z' := Z.
@@ -32,6 +30,4 @@ Theorem Zle_not_eq_lt : forall n m,
 Proof.
   intros.
   omega.
-  Undo.
-  romega.
 Qed.
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
index 0df3d5685d..a97afa7ff0 100644
--- a/test-suite/success/ROmega.v
+++ b/test-suite/success/ROmega.v
@@ -1,5 +1,7 @@
-
-Require Import ZArith ROmega.
+(* This file used to test the `romega` tactics.
+   In Coq 8.9 (end of 2018), these tactics are deprecated.
+   The tests in this file remain but now call the `lia` tactic. *)
+Require Import ZArith Lia.
 
 (* Submitted by Xavier Urbain 18 Jan 2002 *)
 
@@ -7,14 +9,14 @@ Lemma lem1 :
  forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z.
 Proof.
 intros x y.
-romega.
+lia.
 Qed.
 
 (* Proposed by Pierre Crégut *)
 
 Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z.
 intro.
- romega.
+ lia.
 Qed.
 
 (* Proposed by Jean-Christophe Filliâtre *)
@@ -22,7 +24,7 @@ Qed.
 Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
 (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
@@ -32,7 +34,7 @@ Section A.
 Variable x y : Z.
 Hypothesis H : (x > y)%Z.
 Lemma lem4 : (x > y)%Z.
- romega.
+ lia.
 Qed.
 End A.
 
@@ -48,7 +50,7 @@ Hypothesis L : (R1 >= 0)%Z -> S2 = S1.
 Hypothesis M : (H <= 2 * S)%Z.
 Hypothesis N : (S < H)%Z.
 Lemma lem5 : (H > 0)%Z.
- romega.
+ lia.
 Qed.
 End B.
 
@@ -56,11 +58,10 @@ End B.
 Lemma lem6 :
  forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z.
 intros.
- romega.
+ lia.
 Qed.
 
 (* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
-Require Import Omega.
 Section C.
 Parameter g : forall m : nat, m <> 0 -> Prop.
 Parameter f : forall (m : nat) (H : m <> 0), g m H.
@@ -68,23 +69,21 @@ Variable n : nat.
 Variable ap_n : n <> 0.
 Let delta := f n ap_n.
 Lemma lem7 : n = n.
- romega with nat.
+ lia.
 Qed.
 End C.
 
 (* Problem of dependencies *)
-Require Import Omega.
 Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
 intros.
-romega with nat.
+lia.
 Qed.
 
 (* Bug that what caused by the use of intro_using in Omega *)
-Require Import Omega.
 Lemma lem9 :
  forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p.
 intros.
-romega with nat.
+lia.
 Qed.
 
 (* Check that the interpretation of mult on nat enforces its positivity *)
@@ -92,5 +91,5 @@ Qed.
 (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
 Lemma lem10 : forall n m : nat, le n (plus n (mult n m)).
 Proof.
-intros; romega with nat.
+intros; lia.
 Qed.
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
index 3ddf6a40fb..7f69422ab3 100644
--- a/test-suite/success/ROmega0.v
+++ b/test-suite/success/ROmega0.v
@@ -1,25 +1,27 @@
-Require Import ZArith ROmega.
+Require Import ZArith Lia.
 Open Scope Z_scope.
 
 (* Pierre L: examples gathered while debugging romega. *)
+(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated.
+   The tests in this file remain but now call the `lia` tactic. *)
 
-Lemma test_romega_0 :
+Lemma test_lia_0 :
  forall m m',
   0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_0b :
+Lemma test_lia_0b :
  forall m m',
   0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 Proof.
 intros m m'.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_1 :
+Lemma test_lia_1 :
  forall (z z1 z2 : Z),
     z2 <= z1 ->
     z1 <= z2 ->
@@ -29,10 +31,10 @@ Lemma test_romega_1 :
     z >= 0.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_1b :
+Lemma test_lia_1b :
  forall (z z1 z2 : Z),
     z2 <= z1 ->
     z1 <= z2 ->
@@ -42,24 +44,24 @@ Lemma test_romega_1b :
     z >= 0.
 Proof.
 intros z z1 z2.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_2 : forall a b c:Z,
+Lemma test_lia_2 : forall a b c:Z,
  0<=a-b<=1 -> b-c<=2 -> a-c<=3.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_2b : forall a b c:Z,
+Lemma test_lia_2b : forall a b c:Z,
  0<=a-b<=1 -> b-c<=2 -> a-c<=3.
 Proof.
 intros a b c.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_3 : forall a b h hl hr ha hb,
+Lemma test_lia_3 : forall a b h hl hr ha hb,
  0 <= ha - hl <= 1 ->
  -2 <= hl - hr <= 2 ->
  h =b+1 ->
@@ -70,10 +72,10 @@ Lemma test_romega_3 : forall a b h hl hr ha hb,
  0 <= hb - h <= 1.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_3b : forall a b h hl hr ha hb,
+Lemma test_lia_3b : forall a b h hl hr ha hb,
  0 <= ha - hl <= 1 ->
  -2 <= hl - hr <= 2 ->
  h =b+1 ->
@@ -84,79 +86,79 @@ Lemma test_romega_3b : forall a b h hl hr ha hb,
  0 <= hb - h <= 1.
 Proof.
 intros a b h hl hr ha hb.
-romega.
+lia.
 Qed.
 
 
-Lemma test_romega_4 : forall hr ha,
+Lemma test_lia_4 : forall hr ha,
  ha = 0 ->
  (ha = 0 -> hr =0) ->
  hr = 0.
 Proof.
 intros hr ha.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_5 : forall hr ha,
+Lemma test_lia_5 : forall hr ha,
  ha = 0 ->
  (~ha = 0 \/ hr =0) ->
  hr = 0.
 Proof.
 intros hr ha.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False.
+Lemma test_lia_6 : forall z, z>=0 -> 0>z+2 -> False.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
+Lemma test_lia_6b : forall z, z>=0 -> 0>z+2 -> False.
 Proof.
 intros z.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_7 : forall z,
+Lemma test_lia_7 : forall z,
   0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_7b : forall z,
+Lemma test_lia_7b : forall z,
   0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
 (* Magaud BZ#240 *)
 
-Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+Lemma test_lia_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+Lemma test_lia_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
 Proof.
 intros x y.
-romega.
+lia.
 Qed.
 
 (* Besson BZ#1298 *)
 
-Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False.
+Lemma test_lia9 : forall z z':Z, z<>z' -> z'=z -> False.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
 (* Letouzey, May 2017 *)
 
-Lemma test_romega10 : forall x a a' b b',
+Lemma test_lia10 : forall x a a' b b',
  a' <= b ->
  a <= b' ->
  b < b' ->
@@ -164,5 +166,5 @@ Lemma test_romega10 : forall x a a' b b',
  a <= x < b' <-> a <= x < b \/ a' <= x < b'.
 Proof.
  intros.
- romega.
+ lia.
 Qed.
diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v
index 43eda67ea3..e3b090699d 100644
--- a/test-suite/success/ROmega2.v
+++ b/test-suite/success/ROmega2.v
@@ -1,4 +1,6 @@
-Require Import ZArith ROmega.
+(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated.
+   The tests in this file remain but now call the `lia` tactic. *)
+Require Import ZArith Lia.
 
 (* Submitted by Yegor Bryukhov (BZ#922) *)
 
@@ -13,7 +15,7 @@ forall v1 v2 v5 : Z,
 0 < v2 ->
 4*v2 <> 5*v1.
 intros.
-romega.
+lia.
 Qed.
 
 
@@ -37,5 +39,5 @@ forall v1 v2 v3 v4 v5 : Z,
 ((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
 -> False.
 intros.
-romega.
+lia.
 Qed.
diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v
index fd4ff260b5..ef9cb17b4b 100644
--- a/test-suite/success/ROmega3.v
+++ b/test-suite/success/ROmega3.v
@@ -1,10 +1,14 @@
 
-Require Import ZArith ROmega.
+Require Import ZArith Lia.
 Local Open Scope Z_scope.
 
 (** Benchmark provided by Chantal Keller, that romega used to
     solve far too slowly (compared to omega or lia). *)
 
+(* In Coq 8.9 (end of 2018), the `romega` tactics are deprecated.
+   The tests in this file remain but now call the `lia` tactic. *)
+
+
 Parameter v4 : Z.
 Parameter v3 : Z.
 Parameter o4 : Z.
@@ -27,5 +31,5 @@ Lemma lemma_5833 :
       (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
          (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024.
 Proof.
-Timeout 1 romega. (* should take a few milliseconds, not seconds *)
+Timeout 1 lia. (* should take a few milliseconds, not seconds *)
 Timeout 1 Qed. (* ditto *)
diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
index fa659273e1..6ca32f450f 100644
--- a/test-suite/success/ROmegaPre.v
+++ b/test-suite/success/ROmegaPre.v
@@ -1,127 +1,123 @@
-Require Import ZArith Nnat ROmega.
+Require Import ZArith Nnat Lia.
 Open Scope Z_scope.
 
 (** Test of the zify preprocessor for (R)Omega *)
+(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated.
+   The tests in this file remain but now call the `lia` tactic. *)
 
 (* More details in file PreOmega.v
-
-   (r)omega with Z        : starts with zify_op
-   (r)omega with nat      : starts with zify_nat
-   (r)omega with positive : starts with zify_positive
-   (r)omega with N        : starts with uses zify_N
-   (r)omega with *        : starts zify (a saturation of the others)
 *)
 
 (* zify_op *)
 
 Goal forall a:Z, Z.max a a = a.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall a b:Z, Z.max a b = Z.max b a.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
 intros.
 zify.
-intuition; subst; romega. (* pure multiplication: omega alone can't do it *)
+intuition; subst; lia. (* pure multiplication: omega alone can't do it *)
 Qed.
 
 Goal forall a:Z, Z.abs a = a -> a >= 0.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
 intros.
-romega with *.
+lia.
 Qed.
 
 (* zify_nat *)
 
 Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
 intros.
-romega with *.
+lia.
 Qed.
 (* 2000 instead of 200: works, but quite slow *)
 
 Goal forall m: nat, (m*m>=0)%nat.
 intros.
-romega with *.
+lia.
 Qed.
 
 (* zify_positive *)
 
 Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m: positive, (m*m>=1)%positive.
 intros.
-romega with *.
+lia.
 Qed.
 
 (* zify_N *)
 
 Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m:N, (m<1)%N -> (m=0)%N.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m:N, (m*m>=0)%N.
 intros.
-romega with *.
+lia.
 Qed.
 
 (* mix of datatypes *)
 
 Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
 intros.
-romega with *.
+lia.
 Qed.