aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3260.v
blob: 9f0231d91be72988bef2f4ac799619b1683f47f6 (plain)
1
2
3
4
5
6
7
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.