test-suite/bugs/closed/bug_3260.v


1
2
3
4
5
6
7
8

Require Import Setoid.
Goal forall m n, n = m -> n+n = m+m.
intros.
replace n with m at 2.
lazymatch goal with
|- n + m = m + m => idtac
end.
Abort.