aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/ZArith.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/ZArith.v')
-rw-r--r--theories/ZArith/ZArith.v6
1 files changed, 4 insertions, 2 deletions
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index ed47539e1e..5490044ac7 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -16,9 +16,11 @@ Require Export ZArith_base.
Require Export Zpow_def.
-(** Extra modules using [Omega] or [Ring]. *)
+(** Extra modules using [Ring]. *)
-Require Export Omega.
+Require Export OmegaLemmas.
+Require Export PreOmega.
+Require Export ZArith_hints.
Require Export Zcomplements.
Require Export Zpower.
Require Export Zdiv.