path: root/test-suite/bugs/closed/4416.v

Goal exists x, x.
Unset Use Unification Heuristics.
unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
(* Error: Incorrect number of goals (expected 2 tactics). *)