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