From a305642ea1bd5389b08f7a1d29d55a1587919bbd Mon Sep 17 00:00:00 2001
From: emakarov
Date: Wed, 14 Mar 2007 13:23:43 +0000
Subject: Removed an unnecessary argument (p : positive) in Prect_base.

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

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 8123d8d85e..dc6156d6a7 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -578,7 +578,7 @@ trivial.
 Qed.
 
 Theorem Prect_base : forall (P:positive->Type) (a:P xH) 
-  (f:forall p, P p -> P (Psucc p)) (p:positive), Prect P a f xH = a.
+  (f:forall p, P p -> P (Psucc p)), Prect P a f xH = a.
 Proof.
 trivial.
 Qed.
-- 
cgit v1.2.3