The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

What does this error message mean?  Consider the following code in Coq 8.3pl2:

=======
Reset Initial.
Set Implicit Arguments.

Inductive sort : Set := Name | Lam.
Definition var := (prod nat sort).

Inductive trm : sort -> Set :=
| ivar : forall (x:var), trm (snd x)
| aply : forall (K:trm Lam) (M:trm Lam), trm Lam.

Fixpoint trmFV (s:sort) (X:trm s) {struct X} : list var :=
  match X with
    | ivar x => cons x nil
    | aply K M => app (trmFV K) (trmFV M)
  end.

Inductive fsort : Set := prop | aprop.

Inductive fmla : fsort -> Set :=
| feq: forall (s:sort) (t u: trm s), fmla prop
| fand: forall (P Q:fmla prop), fmla prop.

Fixpoint fmlaFV: (fs:fsort) (X:fmla fs) {struct X} : list var :=
  match X with
    | feq t u => app (trmFV t) (trmFV u)
    | fand P Q => app (fmlaFV P) (fmlaFV Q)
  end.
=====

The definition of termFV (free variables in a term) is accepted, but
the definition of fmlaFV (free variables in a formula) is rejected
with the error message above.  I don't see the problem.

Thanks for any help.
Randy