aboutsummaryrefslogtreecommitdiffhomepage
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 f3cf93e0c..ce1bd0335 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -23,7 +23,7 @@ Require Export ZArith_base.
Require Omega.
Require ZArithRing.
Require Zcomplements.
-Import Z_scope.
+V7only [Import Z_scope.].
(**