The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Andrej Bauer wrote:
> Dear Victor,
>
> I have sent you a message like this one privately, but it did not
> work, so I am going to say this publicly.
>
> You are flooding the list with trivialities. In addition, your
> messages are arrogant because you keep saying things like "Coq can't
> compare dependent records" where in reality the source of trouble is
> (in most cases) your ignorance. There is nothing wrong with being
> ignorant, and we're happy to help, but not if you keep implying that
> everyone on this list, the designers of Coq included, are so dumb that
> they can't even get the basic things right and that the design
> decisions made in Coq are obviously bad. (This _is_ what you are
> implying, even if you are not aware of it.)
>
> There is another source of help for beginners which might work better
> for you, namely the IRC #coq channel irc://irc.freenode.net/#coq where
> you can get help immediately.
>    

Also, it looks like the first e-mail of this thread is almost an exact 
duplicate of Victor's previous question.  He seems to have reposted it 
in hopes that the repost would get more replies.  This is a serious 
breach of mailing list etiquette, the sort of thing that would IMO 
justify banning a person from participating in the list.  If people 
don't reply, it's because they don't want to reply; you're not paying 
them anything, so you should respect their decisions.

P.S.: The meta-answer to your question is to run [Set Printing All.], 
instead of just [Set Printing Implicit.].  That will remove all cases of 
confusing messages about terms not being equal, even though they are 
rendered in the same way.