From d7611cb4c5613f807b2c9fb5efb61b7663fcc4bd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Nov 2003 22:28:33 +0000
Subject: ajout Pnat (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4963 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/NArith/BinNat.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'theories/NArith')

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 53d78d3b73..e11194a5d9 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -196,8 +196,6 @@ Qed.
 
 (** Properties of comparison *)
 
-Require Pcompare.
-
 Theorem Ncompare_Eq_eq : (n,m:entier) (Ncompare n m) = EGAL -> n = m.
 Proof.
 NewDestruct n as [|n]; NewDestruct m as [|m]; Simpl; Intro H;
-- 
cgit v1.2.3