The Coq mailing list

[S�bastien Hinderer <Sebastien.Hinderer AT ens-lyon.fr>]

Dear Coq users,

Assume we have the following definitions :

Inductive variable : Set := V : nat -> variable.
Inductive function : Set := F : nat -> function.
Definition signature := function -> nat.
Definition arity := [s:signature;f:function] (s f).

Then the following declaration is not accepted by Coq :

Inductive term [s:signature] : Set :=
  | Var : variable -> (term s)
  | Fun : 
    (f:function) (l:(list (term s))) (H:(length l)=(arity s f)) (term s).

Coq 7.4 returns the following error message :

Error: Non strictly positive occurrence of _UNBOUND_REL_6 in
 (f:function; l:(list (term s)))(length l)=(arity s f)->(term s)

Does someone have an idea about what is wrong with the definition of term ?

Thanks in advance,
Sébastien.