The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

BTW, the following works with Ssreflect:

rewrite {1}A.


On Thu, Dec 13, 2012 at 9:00 AM, Gert Smolka 
<smolka AT ps.uni-saarland.de>
 wrote:
> Why does the following application of "rewrite at" fail?
>
> Require Import Setoid.
>
> Lemma test X (f : X -> X -> Prop) x :
>   f x = (fun y => ~f y y) -> f x x = ~f x x.
>
> Proof. intros A. rewrite A at 1.
>
> (I know that I can use pattern)
>
> Gert