The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

Sometimes in the middle of a proof with lots of yet-to-be-decided
meta-variables, I get strange unification errors. For example:

Error: Impossible to unify "(?1871 * ?1872)%type" with "AttrType"

where AttrType is defined as

Definition AttrType : Set := (PreType * Attr)%type.

(It would seem to me that these two types trivially unify?). Or here is
another one:

Error: Impossible to unify "list ?1908" with "FreeVars"

where FreeVars is defined as

Definition FreeVars : Set := list (FreeVar * Attr).

Am I doing something silly?

Thanks!

Edsko