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)

Cocorico!WikiLicense