aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Min.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith/Min.v')
-rwxr-xr-xtheories/Arith/Min.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 8a5de8703..650b95380 100755
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -9,6 +9,7 @@
(*i $Id$ i*)
Require Arith.
+Import nat_scope.
(** minimum of two natural numbers *)