Derive DependentElimination produces an anomaly

[eponier]

On Coq 8.9, with coq-equations version 1.2 beta2,

From Equations Require Import Equations.
Require Import Vector.

Derive DependentElimination for t.

Anomaly "Uncaught exception Reduction.NotArity."

This seems to occur when the inductive type has parameters. It does not happen where there is no parameter:

Inductive t : nat -> Type :=
  | nil  : t 0
  | cons : forall n, nat -> t n -> t (S n).

Derive DependentElimination for t.

or when the parameter is added as a section variable:

Section test.

Variable A : Type.

Inductive t : nat -> Type :=
  | nil  : t 0
  | cons : forall n, A -> t n -> t (S n).

Derive DependentElimination for t.

End test.

[eponier]

By the way, strangely, the opam package version "1.2 beta2" is considered older than the version "1.2 beta", but no sure that it can be modified now it has been released.

[mattam82]

Indeed, that's a bug in the Derive code, still to investigate. However, for vectors you shouldn't need that instance, the default dependent eliminator of vectors produced by Coq is enough.