aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4214.v
blob: 2e620fce2aee8b5f3abfa0ac598a9a7f0d75b00e (plain)
1
2
3
4
5
6
(* Check that subst uses all equations around *)
Goal forall A (a b c : A), b = a -> b = c -> a = c.
intros.
subst.
reflexivity.
Qed.