coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] replace ... at?

From: Jonas Oberhauser <s9joober AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] replace ... at?
Date: Thu, 4 Oct 2012 15:54:59 +0200

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 ? *)

replace is too eager.
I have fallen back to:

pattern x at 2.
replace x with y.

Kind regards,

jonas

[Coq-Club] replace ... at?, Jonas Oberhauser, 10/04/2012
- Re: [Coq-Club] replace ... at?, Lucian M. Patcas, 10/04/2012
  - Re: [Coq-Club] replace ... at?, Jonas Oberhauser, 10/05/2012
- Re: [Coq-Club] replace ... at?, Matthieu Sozeau, 10/04/2012
  - Re: [Coq-Club] replace ... at?, Jonas Oberhauser, 10/05/2012