aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Between.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith/Between.v')
-rwxr-xr-xtheories/Arith/Between.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 112edaa56..5711a81a7 100755
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -10,6 +10,7 @@
Require Le.
Require Lt.
+Import nat_scope.
Section Between.
Variables P,Q : nat -> Prop.