summaryrefslogtreecommitdiff
path: root/src/reporting_basic.mli
diff options
context:
space:
mode:
authorPeter Sewell2017-02-01 18:11:53 +0000
committerPeter Sewell2017-02-01 18:11:53 +0000
commit672be2d89e8a0784f7abf9e48d943c9d6c4c60a5 (patch)
tree1cdf9143aa4a74c0a40a102ff31e1edcb8a847be /src/reporting_basic.mli
parentf8d6a50596a73ee050d3493fd9751074504eece1 (diff)
document coercions
Diffstat (limited to 'src/reporting_basic.mli')
0 files changed, 0 insertions, 0 deletions