summaryrefslogtreecommitdiff
path: root/theories/NArith/Nnat.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/NArith/Nnat.v')
-rw-r--r--theories/NArith/Nnat.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 6ba6ca3d..94f50bd0 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Nnat.v 8733 2006-04-25 22:52:18Z letouzey $ i*)
+(*i $Id: Nnat.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
-Require Import Arith.
+Require Import Arith_base.
Require Import Compare_dec.
Require Import Sumbool.
Require Import Div2.
@@ -174,4 +174,4 @@ Proof.
pattern n at 1; rewrite <- (nat_of_N_of_nat n).
pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
symmetry; apply nat_of_Ncompare.
-Qed. \ No newline at end of file
+Qed.