The Coq mailing list

[Yucheng Zhang <yczhang89 AT gmail.com>]

Hello,

Suppose I have a goal:

H1 : P x
H2 : P y
H3 : P z
-------------
Q

where P is an inductive predicate. I want to do 'inversion' on each of the 
hypothesis automatically.
I know I can do like this:

do 3 match goal with
  | [ H : P _ |- _ ] => inversion H; move H at top
end

But is there a 'better' way?

Thanks


Yucheng Zhang