The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

I'm not on a computer with Coq installed right now (what a shame, I
know), but if this is an
exact copy/paste of your problem, I guess the : just after fmlaFV is
the problem.
What's happening if you remove it ?

Best,
Vincent

2011/9/22 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
>