The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 4 oct. 2012, at 09:54, Jonas Oberhauser 
<s9joober AT gmail.com>
 wrote:

> Hi all,
> 
> is there such a thing like a replace at?
> 
>  Goal forall X (x y : X) P, P x y -> x = y -> P x x.
>  intros.
>  replace x with y at 2. (* doesn't work ? *)
>  rewrite H at 2. (* supposedly requries Setoid ? *)

Hi,
  indeed the at requires Setoid, and there is a variant
[setoid_replace] defined in theories/Classes/SetoidTactics.v.
It will rewrite with standard leibniz equality just as well
as rewrite.

Best,
-- Matthieu