Derive EqDec fails in the HoTT version

[co-dan]

I am using the newly released version for 8.13, and Derive EqDec fails for me on this example:

Require Import Equations.HoTT.All.

Inductive A : Type :=
| foo : A
| bar : A -> A -> A.

Derive NoConfusion for A.
Derive EqDec for A.

When I compile it from the command line (with -noinit and -indices-matter) I get the following error:

File "./test.v", line 8, characters 0-19:
Error:
The term "A_eqdec" has type "forall x y : A, dec_eq x y"
while it is expected to have type "EqDec A".

However, in coqtop the error message is less comprehensible:

Toplevel input, characters 0-19:
> Derive EqDec for A.
> ^^^^^^^^^^^^^^^^^^^
Error:
<in exception printer>:<original exception:Anomaly
                                           "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.

[mattam82]

Thanks for the report! Probably a mismatch with the Prop setup that is easy to fix.