The following tactic decomposes all record-like structures in the context.
Tactic Notation "decompose" "records" :=
repeat (
match goal with
| H: _ |- _ => progress (decompose record H); clear H
end).
The following tactic decomposes all record-like structures in the context.
Tactic Notation "decompose" "records" :=
repeat (
match goal with
| H: _ |- _ => progress (decompose record H); clear H
end).
decompose records (tactic) (last edited 11-05-2008 00:28:31 by JeffVaughan)