The Coq mailing list

[Dominic Mulligan <dominic.p.mulligan AT googlemail.com>]

Hi,

I've come across an "Error: unknown exception during scheme creation"
message when trying to automatically derive a decidable equality
function for an inductive data type in Coq v8.4.  The data type:

Inductive t : Type := C1 : t | C2 : nat -> t.
Scheme Equality for t.

extracts t_beq fine.  However, the following:

Definition num := nat.
Inductive t : Type := C1 : t | C2 : num -> t.
Scheme Equality for t.

produces the unknown exception.  Is this an intended limitation of the
decidable equality generation, where the types of constructors must be
in a normal form?  Or is this a bug (in either case a better error
message should be provided, presumably)?

Thanks,
Dom