The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

.vo that freezes coqchk (possibly forever).

attached are 2 .vo for Coq 8.3pl2.

j3a.vo was modified with vim so 2 [Definition] have the same name - this 
results in a freeze in a coqchk (possibly forever).

j2.vo was produced with a patched version of Coq and unfortunately doesn't 
pass coqchk, though coqtop is perfectly happy with it, especially with Lemma 
aboutfalse (True and False keep their original meanings,the only trick was 
disabling type checks, evidently coqtop does no type checks. Lemma aboutfalse 
appears to be usable with vanilla coqc)

-- 
georgi

Attachment: j3a.vo
Description: Binary data

Attachment: j2.vo
Description: Binary data