diff options
| author | Hugo Herbelin | 2018-09-19 22:23:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 13:28:36 +0200 |
| commit | 0e225553a2ee1c39e0f070edb6528d109dd878ac (patch) | |
| tree | 603c2b631db1fa410f20b3258065ab6732410bd2 /kernel/nativecode.mli | |
| parent | 49e9fe1c4666beda099872988144d12138dc6349 (diff) | |
Fixing #4612 (anomaly with Scheme called on unsupported inductive type).
We raise a normal error instead of an anomaly.
This fixes also #2550, #8492.
Note in passing: While the case of a type "Inductive I := list I -> I"
is difficult, the case of a "Inductive I := list nat -> I" should be
easily doable.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions