From 8cb5e072d095981aa0664ca9b6f3db8983e18437 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Wed, 17 Aug 2005 12:56:38 +0000
Subject: new congruence

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7298 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib7/cc/CCSolve.v | 20 --------------------
 1 file changed, 20 deletions(-)
 delete mode 100644 contrib7/cc/CCSolve.v

(limited to 'contrib7')

diff --git a/contrib7/cc/CCSolve.v b/contrib7/cc/CCSolve.v
deleted file mode 100644
index 0f771ee5ef..0000000000
--- a/contrib7/cc/CCSolve.v
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-Tactic Definition CCsolve :=
- Repeat (Match Context With
- [ H: ?1 |- ?2] -> 
-  Let Heq = FreshId "Heq" In
- (Assert Heq:(?2==?1);[Congruence|(Rewrite Heq;Exact H)])
- |[ H: ?1; G: ?2 -> ?3 |- ?] ->                        
-  Let Heq = FreshId "Heq" In
- (Assert Heq:(?2==?1) ;[Congruence|                              
-     (Rewrite Heq in G;Generalize (G H);Clear G;Intro G)])).  
-
-- 
cgit v1.2.3