From ed97a490501de3693a8990b0f53deae43dba01a7 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 27 Sep 2001 13:00:06 +0000
Subject: and_rec redondant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2081 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Specif.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 7143f8a346..3bbb9ba7e2 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -203,10 +203,12 @@ Proof.
   Apply (h2 h1).
 Qed.
 
+(*i is now generated 
 Theorem and_rec : (A,B:Prop)(C:Set)(A->B->C)->(A/\B)->C.
 Proof.
   Intros A B C F AB; Apply F; Elim AB; Auto.
-Qed.
+Qed. 
+i*)
 
 (*i is now a theorem
 Axiom eq_rec : (A:Set)(a:A)(P:A->Set)(P a)->(b:A) a=b -> (P b).
-- 
cgit v1.2.3