The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Dear list

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?

Alexandre Pilkiewicz