The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Mon, May 30, 2011 at 11:39:07AM -0400, Adam Chlipala wrote:
> Georgi Guninski wrote:
> >how a client should check a Coq proof for cheating?
> >[...]
> >
> >all of a sudden, coqtop doesn't see a contradiction, possibly due to
> >what coq fanboys call "Anomaly" in your source.
> >
> >the error message coqtop gives is borderline insane "X is not X" (or sthg 
> >very close to this).
> >
> >which parts of coq should i trust?
> 
> I think you're discovering that Coq hasn't been engineered to
> provide a separate, trustworthy proof checker.  However, there is no
> deep technical reason why that wouldn't be easy to put together.  If
> you have an application where this is important, you could be the
> first to spend the few days (my estimate) needed to produce what's
> needed.

I got email which settled this thread for me.

Pollack-inconsistency
Freek Wiedijk

http://www.cs.ru.nl/~freek/pubs/rap.pdf
5 Coq is weakly Pollack-super-inconsistent
page 11

The construction involves coercion.

Thank you all for the replies.