Mercurial > cpdt > repo
comparison src/Tactics.v @ 118:ee676bf3d681
Up to Streicher
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 18 Oct 2008 12:04:28 -0400 |
parents | 8c7d9b82a4a4 |
children | 56e205f966cc |
comparison
equal
deleted
inserted
replaced
117:d176595cf46e | 118:ee676bf3d681 |
---|---|
161 end | 161 end |
162 in match type of E with | 162 in match type of E with |
163 | _ _ ?A => doit A | 163 | _ _ ?A => doit A |
164 | _ ?A => doit A | 164 | _ ?A => doit A |
165 end. | 165 end. |
166 | |
167 Ltac clear_all := | |
168 repeat match goal with | |
169 | [ H : _ |- _ ] => clear H | |
170 end. |