test-suite/bugs/closed/3654.v


1
2
3
4
5
6
7

Tactic Notation "mysimpl" "in" ne_hyp_list(hyps) := simpl in hyps.

Goal 0+0=0->0+0=0->0=0.
intros H1 H2.
mysimpl in H1 H2.
match goal with H:0=0 |- _ => exact H end.
Qed.