test-suite/bugs/opened/3849.v


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.
Fail bar n3 n4.