Mercurial > cpdt > repo

comparison src/CpdtTactics.v @ 417:539ed97750bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for Coq trunk version intended for final 8.4 release
author Adam Chlipala <adam@chlipala.net>
date Tue, 17 Jul 2012 16:37:58 -0400
parents 76e1dfcb86eb
children ed829eaa91b2
comparison
equal deleted inserted replaced
416:ded318830bb0 417:539ed97750bb
212 The weird introduction of [x] helps get around limitations of [dependent destruction], in terms of which sorts of arguments it will accept (e.g., variables bound to hypotheses within Ltac [match]es). *) 212 The weird introduction of [x] helps get around limitations of [dependent destruction], in terms of which sorts of arguments it will accept (e.g., variables bound to hypotheses within Ltac [match]es). *)
213 Ltac dep_destruct E := 213 Ltac dep_destruct E :=
214 let x := fresh "x" in 214 let x := fresh "x" in
215 remember E as x; simpl in x; dependent destruction x; 215 remember E as x; simpl in x; dependent destruction x;
216 try match goal with 216 try match goal with
217 | [ H : _ = E |- _ ] => rewrite <- H in *; clear H 217 | [ H : _ = E |- _ ] => try rewrite <- H in *; clear H
218 end. 218 end.
219 219
220 (** Nuke all hypotheses that we can get away with, without invalidating the goal statement. *) 220 (** Nuke all hypotheses that we can get away with, without invalidating the goal statement. *)
221 Ltac clear_all := 221 Ltac clear_all :=
222 repeat match goal with 222 repeat match goal with