The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Of course. Thanks. --Kevin

On Wed, Mar 5, 2014 at 2:23 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 03/05/2014 02:16 PM, Kevin Sullivan wrote:

Separately, I'd note that the error message produced for the last line of this short code segment is this: Error: The term "append_nil" has type "Monoid" while it is expected to have type "Monoid". This doesn't seem quite right.

The message sounds right to me, considering normal Coq conventions, because the parameter to [Monoid] is marked as implicit.  Try the usual fix of running [Set Printing All], or another command to trigger a less verbose printing mode that still includes what you need.