coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".

This prevented the message from being silent when jumping ahead in a file. Fixes #3636.
Fix a message.
Make the retroknowledge marshalable.

Essential for parallel processing of Coq documents.

It is a fairly straightforward change but a tad tedious, I may have introduced some bugs in the process.
A new version of Hurkens.v.

Adds a more generic and modular proof of Hurkens, where a shallow embedding of U- is given in the most general way. Subsumes all the previous proofs, opens the way to new proofs.
Hurkens.v: coqdoc documentation.
Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].
Hurkens.v: show proofs in coqdoc.