index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
bugs
/
closed
/
4018.v
blob: c3a045943c5d977e8405808aed6864df40e10f07 (
plain
)
1
2
3
(* Catching PatternMatchingFailure was lost at some point *) Goal nat -> True. intros [=].
