aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Minus.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith/Minus.v')
-rwxr-xr-xtheories/Arith/Minus.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 0f435a560..42f44083a 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -12,6 +12,7 @@
Require Lt.
Require Le.
+Import nat_scope.
Fixpoint minus [n:nat] : nat -> nat :=
[m:nat]Cases n m of