Mercurial > cpdt > repo

diff src/Tactics.v @ 160:56e205f966cc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Interderivability of big and small step
author Adam Chlipala <adamc@hcoop.net>
date Mon, 03 Nov 2008 14:47:46 -0500
parents ee676bf3d681
children 7fd470d8a788
line wrap: on
line diff
--- a/src/Tactics.v	Mon Nov 03 09:50:22 2008 -0500
+++ b/src/Tactics.v	Mon Nov 03 14:47:46 2008 -0500
@@ -48,8 +48,9 @@
   match goal with
     | [ H : ex _ |- _ ] => destruct H
 
-    | [ H : ?F _ = ?F _ |- _ ] => injection H;
+    | [ H : ?F ?X = ?F ?Y |- _ ] => injection H;
       match goal with
+        | [ |- F X = F Y -> _ ] => fail 1
         | [ |- _ = _ -> _ ] => try clear H; intros; try subst
       end
     | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;