index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
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
[
=
].
