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/indschemes.ml | |
| 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/indschemes.ml')
| -rw-r--r-- | vernac/indschemes.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index e86e108772..4c41ea657a 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -142,7 +142,8 @@ let try_declare_scheme what f internal names kn = try f internal names kn with e -> let e = CErrors.push e in - let msg = match fst e with + let rec extract_exn = function Logic_monad.TacticFailure e -> extract_exn e | e -> e in + let msg = match extract_exn (fst e) with | ParameterWithoutEquality cst -> alarm what internal (str "Boolean equality not found for parameter " ++ Printer.pr_global cst ++ @@ -176,6 +177,11 @@ let try_declare_scheme what f internal names kn = | NoDecidabilityCoInductive -> alarm what internal (str "Scheme Equality is only for inductive types.") + | ConstructorWithNonParametricInductiveType ind -> + alarm what internal + (strbrk "Unsupported constructor with an argument whose type is a non-parametric inductive type." ++ + strbrk " Type " ++ quote (Printer.pr_inductive (Global.env()) ind) ++ + str " is applied to an argument which is not a variable.") | e when CErrors.noncritical e -> alarm what internal (str "Unexpected error during scheme creation: " ++ CErrors.print e) |