Merge PR #11976: Deprecate the omega tactic

Reviewed-by: Zimmi48

4 files changed, 45 insertions, 35 deletions

diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v
index 478bc434ad..d9eea2f89d 100644
--- a/theories/Logic/WKL.v
+++ b/theories/Logic/WKL.v
@@ -25,7 +25,7 @@
 Require Import WeakFan List.
 Import ListNotations.
 
-Require Import Omega.
+Require Import Arith.
 
 (** [is_path_from P n l] means that there exists a path of length [n]
     from [l] on which [P] does not hold *)
diff --git a/theories/micromega/ZArith_hints.v b/theories/micromega/ZArith_hints.v
new file mode 100644
index 0000000000..a6d3d92a99
--- /dev/null
+++ b/theories/micromega/ZArith_hints.v
@@ -0,0 +1,43 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+Require Import Lia.
+Import ZArith_base.
+
+Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
+  Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_r
+  Z.mul_add_distr_l: zarith.
+
+Require Export Zhints.
+
+Hint Extern 10 (_ = _ :>nat) => abstract lia: zarith.
+Hint Extern 10 (_ <= _) => abstract lia: zarith.
+Hint Extern 10 (_ < _) => abstract lia: zarith.
+Hint Extern 10 (_ >= _) => abstract lia: zarith.
+Hint Extern 10 (_ > _) => abstract lia: zarith.
+
+Hint Extern 10 (_ <> _ :>nat) => abstract lia: zarith.
+Hint Extern 10 (~ _ <= _) => abstract lia: zarith.
+Hint Extern 10 (~ _ < _) => abstract lia: zarith.
+Hint Extern 10 (~ _ >= _) => abstract lia: zarith.
+Hint Extern 10 (~ _ > _) => abstract lia: zarith.
+
+Hint Extern 10 (_ = _ :>Z) => abstract lia: zarith.
+Hint Extern 10 (_ <= _)%Z => abstract lia: zarith.
+Hint Extern 10 (_ < _)%Z => abstract lia: zarith.
+Hint Extern 10 (_ >= _)%Z => abstract lia: zarith.
+Hint Extern 10 (_ > _)%Z => abstract lia: zarith.
+
+Hint Extern 10 (_ <> _ :>Z) => abstract lia: zarith.
+Hint Extern 10 (~ (_ <= _)%Z) => abstract lia: zarith.
+Hint Extern 10 (~ (_ < _)%Z) => abstract lia: zarith.
+Hint Extern 10 (~ (_ >= _)%Z) => abstract lia: zarith.
+Hint Extern 10 (~ (_ > _)%Z) => abstract lia: zarith.
+
+Hint Extern 10 False => abstract lia: zarith.
diff --git a/theories/omega/Omega.v b/theories/omega/Omega.v
index 10a5aa47b3..5c52284621 100644
--- a/theories/omega/Omega.v
+++ b/theories/omega/Omega.v
@@ -19,38 +19,6 @@
 Require Export ZArith_base.
 Require Export OmegaLemmas.
 Require Export PreOmega.
-Require Import Lia.
+Require Export ZArith_hints.
 
 Declare ML Module "omega_plugin".
-
-Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
-  Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_r
-  Z.mul_add_distr_l: zarith.
-
-Require Export Zhints.
-
-Hint Extern 10 (_ = _ :>nat) => abstract lia: zarith.
-Hint Extern 10 (_ <= _) => abstract lia: zarith.
-Hint Extern 10 (_ < _) => abstract lia: zarith.
-Hint Extern 10 (_ >= _) => abstract lia: zarith.
-Hint Extern 10 (_ > _) => abstract lia: zarith.
-
-Hint Extern 10 (_ <> _ :>nat) => abstract lia: zarith.
-Hint Extern 10 (~ _ <= _) => abstract lia: zarith.
-Hint Extern 10 (~ _ < _) => abstract lia: zarith.
-Hint Extern 10 (~ _ >= _) => abstract lia: zarith.
-Hint Extern 10 (~ _ > _) => abstract lia: zarith.
-
-Hint Extern 10 (_ = _ :>Z) => abstract lia: zarith.
-Hint Extern 10 (_ <= _)%Z => abstract lia: zarith.
-Hint Extern 10 (_ < _)%Z => abstract lia: zarith.
-Hint Extern 10 (_ >= _)%Z => abstract lia: zarith.
-Hint Extern 10 (_ > _)%Z => abstract lia: zarith.
-
-Hint Extern 10 (_ <> _ :>Z) => abstract lia: zarith.
-Hint Extern 10 (~ (_ <= _)%Z) => abstract lia: zarith.
-Hint Extern 10 (~ (_ < _)%Z) => abstract lia: zarith.
-Hint Extern 10 (~ (_ >= _)%Z) => abstract lia: zarith.
-Hint Extern 10 (~ (_ > _)%Z) => abstract lia: zarith.
-
-Hint Extern 10 False => abstract lia: zarith.
diff --git a/theories/setoid_ring/Rings_Z.v b/theories/setoid_ring/Rings_Z.v
index f489b00145..372bba7926 100644
--- a/theories/setoid_ring/Rings_Z.v
+++ b/theories/setoid_ring/Rings_Z.v
@@ -11,7 +11,6 @@
 Require Export Cring.
 Require Export Integral_domain.
 Require Export Ncring_initial.
-Require Export Omega.
 
 Instance Zcri: (Cring (Rr:=Zr)).
 red. exact Z.mul_comm. Defined.