The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Hello,

I have used coqdoc with --html option to get "documentation" for my file and the output, when viewed with a browser, has strange coloring behavior. Here is an example:

Theorem isapropneg (X:UU): isaprop (X -> empty).
Proof. intro. apply (impredfun (S O) X empty isapropempty). Qed.

Corollary isapropdneg (X:UU): isaprop (dneg X).
Proof. intro. apply (isapropneg (neg X)). Defined.

Definition isaninvprop (X:UU):= isweq _ _ (todneg X).

Theorem isaninvpropneg (X:UU): isaninvprop (neg X).
Proof. intros.
set (f:= todneg (neg X)). set (g:= negf _ _ (todneg X)). set (is1:= isapropneg X). set (is2:= isapropneg (dneg X)). apply(isweqimplimpl _ _ f g is1 is2). Defined.

 Any ideas on how to make it behave properly?

Thanks!

Vladimir.