aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--theories/ZArith/Zdiv.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index a61df305dd..ee6987215c 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -20,6 +20,7 @@ Then only after proves the main required property.
*)
Require Export ZArith_base.
+Require Zbool.
Require Omega.
Require ZArithRing.
Require Zcomplements.