diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 17:37:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 17:37:31 +0000 |
| commit | fdd84089a127e7f12f43a5dd02547594effd0964 (patch) | |
| tree | 4070d8a969e6287a0094540d91bd24a1dc195eb6 /test-suite/failure/ClearBody.v | |
| parent | ea4180b729f90630941b5501ef83f94b6c8ecd6b (diff) | |
Uminus.v : prepare this test file for the use of Fail
- Highlight the fact that the line defining "up" is the one which
should fail.
- Factor code with stdlib's Hurkens.v
- This way, this test could become a "shouldnotfail" test by placing
two final "Fail" (before the definitions of "up" and "paradox").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16791 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/failure/ClearBody.v')
0 files changed, 0 insertions, 0 deletions