lia: depend only on ZArith_base

7 files changed, 9 insertions, 8 deletions

diff --git a/plugins/micromega/DeclConstant.v b/plugins/micromega/DeclConstant.v
index 0288728504..7ad5e313e3 100644
--- a/plugins/micromega/DeclConstant.v
+++ b/plugins/micromega/DeclConstant.v
@@ -51,7 +51,7 @@ Instance GT_APP2 {T1 T2 T3: Type} (F : T1 -> T2 -> T3)
          GT A1 -> GT A2 -> GT (F A1 A2).
 Defined.
 
-Require Import ZArith.
+Require Import QArith_base.
 
 Instance DO : DeclaredConstant O := {}.
 Instance DS : DeclaredConstant S := {}.
@@ -64,6 +64,4 @@ Instance DZneg: DeclaredConstant Zneg := {}.
 Instance DZpow_pos : DeclaredConstant Z.pow_pos := {}.
 Instance DZpow     : DeclaredConstant Z.pow     := {}.
 
-Require Import QArith.
-
 Instance DQ : DeclaredConstant Qmake := {}.
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 3351c7ef8a..55a93eade7 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -15,7 +15,7 @@
 (************************************************************************)
 
 Require Import ZMicromega.
-Require Import ZArith.
+Require Import ZArith_base.
 Require Import RingMicromega.
 Require Import VarMap.
 Require Import DeclConstant.
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index f93fe021f9..6db62e8401 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -15,7 +15,7 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import ZArith.
+Require Import ZArith_base.
 Require Import Coq.Arith.Max.
 Require Import List.
 Set Implicit Arguments.
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index 26970faf0c..08f3f39204 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -12,9 +12,10 @@
 
 Require Import OrderedRing.
 Require Import RingMicromega.
-Require Import ZArith.
+Require Import ZArith_base.
 Require Import InitialRing.
 Require Import Setoid.
+Require Import ZArithRing.
 
 Import OrderedRingSyntax.
 
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index c160e11467..d709fdda14 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -21,7 +21,8 @@ Require Import RingMicromega.
 Require  FSetPositive FSetEqProperties.
 Require Import ZCoeff.
 Require Import Refl.
-Require Import ZArith.
+Require Import ZArith_base.
+Require Import ZArithRing.
 Require PreOmega.
 (*Declare ML Module "micromega_plugin".*)
 Local Open Scope Z_scope.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index 9e9481341f..aba064a556 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -15,6 +15,7 @@ Require Export DoubleType.
 Require Import Lia.
 Require Import Zpow_facts.
 Require Import Zgcd_alt.
+Require ZArith.
 Import Znumtheory.
 
 Register bool as kernel.ind_bool.
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index cc216b21f8..e889150d92 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Import OrderedType.
-Require Import ZArith.
+Require Import ZArith_base.
 Require Import PeanoNat.
 Require Import Ascii String.
 Require Import NArith Ndec.