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 /vernac/auto_ind_decl.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 'vernac/auto_ind_decl.mli')
| -rw-r--r-- | vernac/auto_ind_decl.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli index 11f26c7c36..8ecc09b7d1 100644 --- a/vernac/auto_ind_decl.mli +++ b/vernac/auto_ind_decl.mli @@ -27,6 +27,7 @@ exception ParameterWithoutEquality of GlobRef.t exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported exception NoDecidabilityCoInductive +exception ConstructorWithNonParametricInductiveType of inductive val beq_scheme_kind : mutual scheme_kind val build_beq_scheme : mutual_scheme_object_function |