The Coq mailing list

[Yucheng Zhang <yczhang89 AT gmail.com>]

On Nov 27, 2012, at 8:49 PM, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:
> I do not know if there is a better way, but I would tend to "clear H"
> instead of "move H at top" (or rather 'at bottom', I think).
> Most of the time, I do not want to keep the original hypothesis.
> 
> So maybe a
> 
> Ltac cleanP :=
> match goal with [ H : P _ |- _ ] => inversion H; clear H; subst end.
> 
> would help. (Note: the subst may not do what you wish, since it would
> use all already present equalities)
> 
>> H1 : P x
>> H2 : P y
>> H3 : P z
>> -------------
>> Q
> 
> repeat cleanP. (* alternatively 'do 3 cleanP.' *)
> 
> If your P predicate is recursive, you will encounter problems with
> tactic called endlessly.

Thanks for the detailed answer.

I am not satisfied with the solution though, as my P predicate is indeed
recursive, and the number of P hypotheses is not known in advance. (I should
have formulated my question more accurately..)

Maybe a solution is 'do 5 cleanP', where 5 is an arbitarily chosen finite
number that is large enough, but this looks not so elegant.