The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

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.