diff options
| author | herbelin | 2003-11-29 17:28:49 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-29 17:28:49 +0000 |
| commit | 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 (patch) | |
| tree | 77c0021911e3696a8c98e35a51840800db4be2a9 /contrib/cc | |
| parent | 9058fb97426307536f56c3e7447be2f70798e081 (diff) | |
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
Diffstat (limited to 'contrib/cc')
| -rw-r--r-- | contrib/cc/CCSolve.v | 22 |
1 files changed, 12 insertions, 10 deletions
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. |