Rewrite.apply_lemma is written in state passing style.

This removes a use of Evd.merge.
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.
Added support for interpreting hyp lists in tactic notations.
Using an or_var rather than the hack with loc for coding a pure ident
as a disjunctive intropattern.
Make eq_pattern_test/eq_test work up to the equivalence of primitive
projections with their eta-expanded constant form.
Return a Prop not an arbitrary Type, and correct a typo.
Rename eq_constr functions in Evd to not break backward compatibility
with existing ML code.
Update test-suite files.