diff options
| author | Brian Campbell | 2018-01-30 17:57:23 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-01-30 18:28:10 +0000 |
| commit | 31f142f122d0a5e5fc0ab95c96ba93c4ddd17d30 (patch) | |
| tree | 343b60792e70cc52ca99687f603ec630a31d347c /src/util.mli | |
| parent | d0a2e63c3c6f00a29ce9ecb529ea4fb1c49b4caa (diff) | |
Optionally give *all* monomorphisation errors at once
(and stop afterwards unless asked)
Diffstat (limited to 'src/util.mli')
0 files changed, 0 insertions, 0 deletions