aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zwf.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zwf.v')
-rw-r--r--theories/ZArith/Zwf.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 56baf1782..d93a6ea44 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -11,6 +11,7 @@
Require ZArith_base.
Require Export Wf_nat.
Require Omega.
+Import Z_scope.
(** Well-founded relations on Z. *)