removal of CC.v lemata in cc (deprecated)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4994 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 6 deletions

diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index 18a99056b..4c0287dc3 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -1,4 +1,3 @@
-Require CC.
 
 Theorem t1: (A:Set)(a:A)(f:A->A)
 	(f a)=a->(f (f a))=a.
@@ -40,14 +39,16 @@ Theorem dep2:(A,B:Set)(f:(A:Set)(b:bool)if b then unit else A->unit)(e:A==B)
 Intros;Rewrite e;Reflexivity.
 Save.
 
-(* example with CCSolve *)
 
-Theorem t4 :  (A:Set; P:(A->Prop); u,v:A)u=v->(P u)->(P v).
-Intros.
-CCsolve.
+(* example that CC can solve 	
+	(dependent function applied to the same argument)*) 
+
+Theorem dep3:(A:Set)(P:(A->Set))(f,g:(x:A)(P x))f=g->(x:A)(f x)=(g x).		
+Intros.	
+CC.
 Save.
 
-(* Exambles with injection rule *)
+(* Examples with injection rule *)
 
 Theorem t5 : (A:Set;a,b,c,d:A)(a,c)=(b,d)->a=b/\c=d.
 Intros.
@@ -59,3 +60,12 @@ Intros.
 CC.
 Save.
 
+(* example with CCSolve (requires CC)*)
+
+Require CC.
+
+Theorem t4 :  (A:Set; P:(A->Prop); a,b,c,d:A)a=b->c=d->
+                 (P a)->((P b)->(P c))->(P d).
+Intros.
+CCsolve.
+Save.