aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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 2d4b9f3720..87fbe0f19c 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -19,7 +19,7 @@ Then only after proves the main required property.
*)
-Require ZArith.
+Require Export ZArith.
Require Omega.
Require ZArithRing.