aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Wf_Z.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Wf_Z.v')
-rw-r--r--theories/ZArith/Wf_Z.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 56f8485da..452855a11 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -9,6 +9,7 @@
(*i $Id$ i*)
Require fast_integer.
+Require Zorder.
Require zarith_aux.
Require auxiliary.
Require Zsyntax.