Fixing bug 3951
Correction of error message (bug 3359)
adds general facts in the Reals library, whose need was detected in
experiments about computing PI
Fix bug in setoid_rewrite introduced by PMP's commits, which was creating
two versions of the rewriting lemma, keeping useless evars around. This
can now happen only when the rewrite lemma is used under binders... Fix
to do next.
ATBR can't compile without the fix, as it uses setoid_rewrite to rewrite
under binders. This might incur a significant time penalty.
Fix bug #3656.

Maintain the user-level view of primitive projections,
disallow manual unfolding and do not let hnf give the eta-expanded
form.
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.