bug_4018.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

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

blob: d7929372ad50da0400499d0fe38b4693735f3d66 (plain)

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