From 8769d8ec01eaca509d0ca01cb7f12a813e402919 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Nov 2003 22:34:05 +0000
Subject: ajout Pnat (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4964 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/BinInt.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 42cb3675f5..e6257b243d 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -13,10 +13,10 @@
 (***********************************************************)
 
 Require Export BinPos.
+Require Export Pnat.
 Require BinNat.
 Require Plus.
 Require Mult.
-
 (**********************************************************************)
 (** Binary integer numbers *)
 
@@ -256,8 +256,6 @@ Qed.
 (**********************************************************************)
 (** Other properties of binary integer numbers *)
 
-Hints Local Resolve compare_convert_O.
-
 Lemma ZL0 : (S (S O))=(plus (S O) (S O)).
 Proof.
 Reflexivity.
-- 
cgit v1.2.3