From da349d639dee435ab9668059a99547fe0419639d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Sep 2005 13:43:30 +0000
Subject: Suppression test CCSolve car remplaçé par Congruence mais qui ne
 traite pas les connecteurs propositionnels (pour Pierre C.)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7359 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/cc.v | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index 4d898da97d..940aa75075 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -71,13 +71,3 @@ Theorem discr2 : (Some ? true)=(Some ? false)->False.
 Intros.
 Congruence.
 Save.
-
-(* example with Congruence.Solve (requires CCSolve.v)*)
-
-Require CCSolve.
-
-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.
-- 
cgit v1.2.3