aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/Zdiv.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zdiv.v')
-rw-r--r--theories/ZArith/Zdiv.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 0c4feab084..c3ebf133de 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -19,7 +19,7 @@ Then only after proves the main required property.
*)
-Require Export ZArith.
+Require Export ZArith_base.
Require Omega.
Require ZArithRing.
Require Zcomplements.