diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-06 14:54:23 -0400 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-17 10:27:12 +0100 |
| commit | 633ed9c528c64dc2daa0b3e83749bc392aab7fd2 (patch) | |
| tree | eb29fb1c4694b299e2747b9d975ca4f8b1dd0ac2 /test-suite/bugs/closed/4772.v | |
| parent | a553126c9e0984f38b1a15f2db60458813a177c9 (diff) | |
Add test suite files for 4700-4785
I didn't add any test-cases for timing-based bugs (4707, 4768, 4776,
4777, 4779, 4783), nor CoqIDE bugs (4700, 4751, 4752, 4756), nor
bugs about printing (4709, 4711, 4720, 4723, 4734, 4736, 4738, 4741,
4743, 4748, 4749, 4750, 4757, 4758, 4765, 4784). I'm not sure what to
do with 4712, 4714, 4732, 4740.
Diffstat (limited to 'test-suite/bugs/closed/4772.v')
| -rw-r--r-- | test-suite/bugs/closed/4772.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4772.v b/test-suite/bugs/closed/4772.v new file mode 100644 index 000000000..c3109fa31 --- /dev/null +++ b/test-suite/bugs/closed/4772.v @@ -0,0 +1,6 @@ + +Record TruncType := BuildTruncType { + trunctype_type : Type +}. + +Fail Arguments BuildTruncType _ _ {_}. (* This should fail *) |