test-suite/bugs/closed/bug_4416.v


1
2
3
4
5

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