Tentative performance fix for Evd.merge_uctx.

The levels added by the context are in general much fewer than the size of the
evarmap, so it is better to add them to the latter rather than doing it the
other way around.
Cleaning up interface of ContextSet.

Names and arguments were uniformized, and some functions were redesigned to
take their typical use-case into account.
Adding a primitive to merge ContextSets which is more efficient when one
of the argument is smaller than the other one.
Using the asymmetric merging primitive in Evd.
Do early occur-check in unification to allow eta to fire (fixes bug #3477)
Allow pattern matching on the applied form of projections with primitive
applications, solving part of bug #3503.
Fix unification which was failing when unifying a primitive projection against
its expansion if it could reduce (fixes bug #3480).
Fix bug introduced by earlier commit on first-order unification of primitive
projections and their expansion, allowing unfolding when it fails.
Cleanup code in reductionops.ml
A couple of fixes/improvements in -beautify, but backtracking on
change of printing format of forall (need more thinking).
Fixing parsing of bullets after a "...".

The lexer parses bullets only at the beginning of sentence. In
particular, the lexer recognizes sentences (this feature was
introduced for the translator and it is still used for the
beautifier). It recognized "." but not "...'. I added "..." followed
by space or eol as a terminator of sentences. I hope this is
compatible with the rest of the code dealing with end of
sentences.

Fixed also parse_to_dot which was not aware of "...".

Maybe there are similar things to do with coqide or PG?
Quick fix for avoiding infinitely many respawning and Warning "Coq
died" when coqtop or coqtopide.cmxs are in inconsistent state.
In bug #2406, renouncing to test failure of parsing error.
(AFAIU, it is the table of supported unicode characters which has to
be upgraded anyway.)
Bug #3469: fixing unterminated comment.
Upgrading output tests.
output/Arguments.v
output/ArgumentsScope.v
output/Arguments_renaming.v
output/Cases.v
output/Implicit.v
output/PrintInfos.v
output/TranspModType.v

Main changes: monomorphic -> not universe polymorphic, Peano vs Nat
Bettre pretty-printing of evar maps, avoids printing universe information
for typeclass errors.
Small optimization in Cooking: do not construct identity substitutions.
Fix test-suite files according to new parsing rule for application of primitive
projections.
Fix elimschemes accessing directly the universe context of inductives (fixes test-suite
file HoTT_coq_089.v).
Restore the error-handling behavior of [change], which was silently failing
when conversion in the goal failed.
Restrict eta-conversion to inductive records, fixing bug #3310.