aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-06-07 18:44:59 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-06-07 18:44:59 +0000
commit5d82773fdad88ab93baf713888248da4ee8185a9 (patch)
treec33cf6bdf4619df5dd30c9200ae85a9ceb5978ae /theories/Arith
parentcb25f49dc87eb4a25cbc0a08fdc90c02d4bae373 (diff)
Extension of NArith: Nminus, Nmin, etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith')
-rw-r--r--theories/Arith/Max.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index a3d658d0c..75e1cdf0c 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -8,7 +8,7 @@
(*i $Id$ i*)
-Require Import Arith.
+Require Import Le.
Open Local Scope nat_scope.