aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorJason Gross2016-06-06 14:54:23 -0400
committerMaxime Dénès2016-11-17 10:27:12 +0100
commit633ed9c528c64dc2daa0b3e83749bc392aab7fd2 (patch)
treeeb29fb1c4694b299e2747b9d975ca4f8b1dd0ac2 /dev/base_include
parenta553126c9e0984f38b1a15f2db60458813a177c9 (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 'dev/base_include')
0 files changed, 0 insertions, 0 deletions