aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4018.v
blob: 8895e09e0262d12c235a4804a80a145aba4175af (plain)
1
2
3
(* Catching PatternMatchingFailure was lost at some point *)
Goal nat -> True.
Fail intros [=].