From 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Nov 2003 17:28:49 +0000
Subject: Remplacement des fichiers .v ancienne syntaxe de theories, contrib et
 states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/cc/CCSolve.v | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

(limited to 'contrib/cc')

diff --git a/contrib/cc/CCSolve.v b/contrib/cc/CCSolve.v
index 30622aeaa8..c80ba16ec3 100644
--- a/contrib/cc/CCSolve.v
+++ b/contrib/cc/CCSolve.v
@@ -8,13 +8,15 @@
 
 (* $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)])).  
-
+Ltac CCsolve :=
+  repeat
+   match goal with
+   | H:?X1 |- ?X2 =>
+       let Heq := fresh "Heq" in
+       (assert (Heq : X2 = X1); [ congruence | rewrite Heq; exact H ])
+   | H:?X1,G:(?X2 -> ?X3) |- _ =>
+       let Heq := fresh "Heq" in
+       (assert (Heq : X2 = X1);
+         [ congruence
+         | rewrite Heq in G; generalize (G H); clear G; intro G ])
+   end.  
-- 
cgit v1.2.3