aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zhints.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zhints.v')
-rw-r--r--theories/ZArith/Zhints.v5
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v
index 8dc9069a6..6eb668a5a 100644
--- a/theories/ZArith/Zhints.v
+++ b/theories/ZArith/Zhints.v
@@ -27,11 +27,12 @@
(* Lemmas involving positive and compare are not taken into account *)
-Require fast_integer.
+Require BinInt.
Require Zorder.
Require Zmin.
Require Zabs.
-Require zarith_aux.
+Require Zcompare.
+Require Znat.
Require auxiliary.
Require Zsyntax.
Require Zmisc.