Mercurial > cpdt > repo

diff src/Tactics.v @ 50:a21eb02cc7c6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Recursive predicates
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Sep 2008 11:57:15 -0400
parents 95e24b629ad9
children 9ceee967b1fc
line wrap: on
line diff
--- a/src/Tactics.v	Sun Sep 28 10:59:04 2008 -0400
+++ b/src/Tactics.v	Sun Sep 28 11:57:15 2008 -0400
@@ -12,6 +12,11 @@
 Require Omega.
 
 
+Ltac simplHyp :=
+  match goal with
+    | [ H : S _ = S _ |- _ ] => injection H; clear H; intros; subst
+  end.
+
 Ltac rewriteHyp :=
   match goal with
     | [ H : _ |- _ ] => rewrite H
@@ -23,6 +28,6 @@
 
 Hint Rewrite app_ass : cpdt.
 
-Ltac sintuition := simpl in *; intuition.
+Ltac sintuition := simpl in *; intuition; try simplHyp.
 
 Ltac crush := sintuition; rewriter; sintuition; try omega.