Mercurial > cpdt > repo

comparison src/Tactics.v @ 65:21bb59c56b98

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove [done] markers after enhancement phase finishes
author Adam Chlipala <adamc@hcoop.net>
date Wed, 01 Oct 2008 09:32:36 -0400
parents 739c2818d6e2
children b52204928c7d
comparison
equal deleted inserted replaced
64:739c2818d6e2 65:21bb59c56b98
100 end 100 end
101 end 101 end
102 end 102 end
103 end. 103 end.
104 104
105 Ltac un_done :=
106 repeat match goal with
107 | [ H : done _ |- _ ] => clear H
108 end.
109
105 Ltac crush' lemmas invOne := 110 Ltac crush' lemmas invOne :=
106 let sintuition := simpl in *; intuition; subst; repeat (simplHyp invOne; intuition; subst); try congruence 111 let sintuition := simpl in *; intuition; subst; repeat (simplHyp invOne; intuition; subst); try congruence
107 in (sintuition; rewriter; 112 in (sintuition; rewriter;
108 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); 113 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
109 repeat (simplHyp invOne; intuition)); 114 repeat (simplHyp invOne; intuition));
110 sintuition; try omega). 115 un_done; sintuition; try omega).
111 116
112 Ltac crush := crush' tt fail. 117 Ltac crush := crush' tt fail.