Remove the omega tactic and related options

5 files changed, 4 insertions, 32 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 47137414dc..ff1a2b5a53 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1775,8 +1775,6 @@ weak_Zmult_plus_distr_r (now Z.mul_add_distr_pos)
 
 Definition Zne (x y:Z) := x <> y. (* TODO : to remove someday ? *)
 
-Register Zne as plugins.omega.Zne.
-
 Ltac elim_compare com1 com2 :=
   case (Dcompare (com1 ?= com2)%Z);
     [ idtac | let x := fresh "H" in
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index ed47539e1e..5490044ac7 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -16,9 +16,11 @@ Require Export ZArith_base.
 
 Require Export Zpow_def.
 
-(** Extra modules using [Omega] or [Ring]. *)
+(** Extra modules using [Ring]. *)
 
-Require Export Omega.
+Require Export OmegaLemmas.
+Require Export PreOmega.
+Require Export ZArith_hints.
 Require Export Zcomplements.
 Require Export Zpower.
 Require Export Zdiv.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 7f72d42d1f..b7cd849323 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -959,13 +959,6 @@ Definition inj_lt n m := proj1 (Nat2Z.inj_lt n m).
 Definition inj_ge n m := proj1 (Nat2Z.inj_ge n m).
 Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m).
 
-Register neq as plugins.omega.neq.
-Register inj_eq as plugins.omega.inj_eq.
-Register inj_neq as plugins.omega.inj_neq.
-Register inj_le as plugins.omega.inj_le.
-Register inj_lt as plugins.omega.inj_lt.
-Register inj_ge as plugins.omega.inj_ge.
-Register inj_gt as plugins.omega.inj_gt.
 
 (** For the others, a Notation is fine *)
 
@@ -1033,5 +1026,3 @@ Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z.of_nat (n - m) = 0.
 Proof.
  intros. rewrite not_le_minus_0; auto with arith.
 Qed.
-
-Register inj_minus2 as plugins.omega.inj_minus2.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 4c533ac458..bef9cede12 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -64,11 +64,6 @@ Proof.
   apply Z.lt_gt_cases.
 Qed.
 
-Register dec_Zne as plugins.omega.dec_Zne.
-Register dec_Zgt as plugins.omega.dec_Zgt.
-Register dec_Zge as plugins.omega.dec_Zge.
-Register not_Zeq as plugins.omega.not_Zeq.
-
 (** * Relating strict and large orders *)
 
 Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing).
@@ -120,12 +115,6 @@ Proof.
   destruct (Z.eq_decidable n m); [assumption|now elim H].
 Qed.
 
-Register Znot_le_gt as plugins.omega.Znot_le_gt.
-Register Znot_lt_ge as plugins.omega.Znot_lt_ge.
-Register Znot_ge_lt as plugins.omega.Znot_ge_lt.
-Register Znot_gt_le as plugins.omega.Znot_gt_le.
-Register not_Zne as plugins.omega.not_Zne.
-
 (** * Equivalence and order properties *)
 
 (** Reflexivity *)
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 10ea6cc03e..369a0c46ae 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -93,11 +93,3 @@ Proof.
  apply Z.le_lt_trans with (m*n+p); trivial.
  now apply Z.add_lt_mono_l.
 Qed.
-
-Register Zegal_left as plugins.omega.Zegal_left.
-Register Zne_left as plugins.omega.Zne_left.
-Register Zlt_left as plugins.omega.Zlt_left.
-Register Zgt_left as plugins.omega.Zgt_left.
-Register Zle_left as plugins.omega.Zle_left.
-Register Zge_left as plugins.omega.Zge_left.
-Register Zmult_le_approx as plugins.omega.Zmult_le_approx.