The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 07/03/2013 01:24 PM, t x wrote:
>   Specifically, instead of:
>
> assert ( _statement_ ) as H0 by _tactic_ .
> rewrite H0.
>
> I would like to write something closer to:
>
>   rewrite using ( _staement_ ) proved by _tactic_.

That sounds like the [replace] tactic.