The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Alexandre Pilkiewicz wrote:
> I would like to iterate *once* on all the hypothesis of the current
> goal. Something like
>
> repeat
> (match goal with
>   | H : _ |- _ =>  ....
> end).
>
> would not work because I don't want to clear H and the action I want
> to associate won't fail if repeated, so it loops forever.
>
> Are they any better solution?
>    

You can build a list of candidate hypotheses by getting each hypothesis 
out of the way as you first select it.  For instance, run [generalize 
dependent H] inside your loop, and then [intros] all the hypotheses back 
into place afterward, once you've built a list of hypotheses (say, as a 
tuple).