diff options
| author | Hugo Herbelin | 2018-09-19 22:47:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 13:28:36 +0200 |
| commit | 82a3fb5d5c0d0c5660effec59f3800ee5e8a125d (patch) | |
| tree | daf3db3f650308c37d65b285788e4e034f1d04ad /dev | |
| parent | 0e225553a2ee1c39e0f070edb6528d109dd878ac (diff) | |
Fixing #4859 (anomaly with Scheme called on inductive type with indices).
We raise a normal error instead of an anomaly.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions