ZArith: move lia hints to a dedicated module

4 files changed, 46 insertions, 34 deletions

diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 67d0b37e81..65c88ed8d5 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -44,6 +44,7 @@ theories/micromega/Refl.v
 theories/micromega/RingMicromega.v
 theories/micromega/Tauto.v
 theories/micromega/VarMap.v
+theories/micromega/ZArith_hints.v
 theories/micromega/ZCoeff.v
 theories/micromega/ZMicromega.v
 theories/micromega/ZifyInst.v
diff --git a/test-suite/bugs/closed/bug_1912.v b/test-suite/bugs/closed/bug_1912.v
index 987a541778..0228abbb9b 100644
--- a/test-suite/bugs/closed/bug_1912.v
+++ b/test-suite/bugs/closed/bug_1912.v
@@ -1,4 +1,4 @@
-Require Import ZArith.
+Require Import Omega.
 
 Goal forall x, Z.succ (Z.pred x) = x.
 intros x.
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.