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 /test-suite | |
| 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 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4612.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4612.v b/test-suite/bugs/closed/4612.v new file mode 100644 index 0000000000..ce95f26acc --- /dev/null +++ b/test-suite/bugs/closed/4612.v @@ -0,0 +1,7 @@ +(* While waiting for support, check at least that it does not raise an anomaly *) + +Inductive ctype := +| Struct: list ctype -> ctype +| Bot : ctype. + +Fail Scheme Equality for ctype. |