diff options
| author | Jim Fehrle | 2020-10-16 21:12:49 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-19 11:49:31 -0700 |
| commit | 48e0d4112cdf23ec89e8044387bd8484cb026b92 (patch) | |
| tree | b50fda16e2e1343f632937d213b99ba9f54e9742 /kernel/type_errors.ml | |
| parent | 07a199ffa640b9eb94235ebc3732c4b2981ca525 (diff) | |
Better message and avoid an infinite SPLICE loop
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions