aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/ZMicromega.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/ZMicromega.v')
-rw-r--r--plugins/micromega/ZMicromega.v3
1 files changed, 2 insertions, 1 deletions
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.