aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3849.v
blob: a8dc3af9cfb995a7ef4db9a4e0886b5b0a32acb3 (plain)
1
2
3
4
5
6
7
8
Tactic Notation "foo" hyp_list(hs) := clear hs.

Tactic Notation "bar" hyp_list(hs) := foo hs.

Goal True.
do 5 pose proof 0 as ?n0.
foo n1 n2.
bar n3 n4.