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

(* Catching PatternMatchingFailure was lost at some point *)
Goal nat -> True.
Fail intros [=].