The Coq mailing list

[frederic.blanqui AT loria.fr]

On Wed, 7 Nov 2007, Edsko de Vries wrote:

>    rewrite NatListTheory.union_comm ; assumption.
>
> to finish the proof, but that tells me
>
>  User error: Either the term NatList.union M2 M1 that must be rewritten
>  occurs in a covariant position or the goal is not made of morphism
>  applications only. You can replace only occurrences that are in a
>  contravariant position and such that the context obtained by
>  abstracting them is made of morphism applications only.
>
> and I have absolutely no idea what that means. Any pointers?

see http://coq.inria.fr/V8.1/refman/Reference-Manual024.html

Chapter 21  User defined equalities and relations

by Claudio Sacerdoti Coen