Fixing bug #3493.

Coq now accepts the [Universes u1 ... un] syntax.
Removing spurious tclWITHHOLES.

Indeed [tclWITHHOLES false tac sigma x] is equivalent to [tclEVARS sigma <*> tac x]
and we should try to reduce the use of this tactical, because it is mostly
a legacy tactic.
Protect against "it's unifiable, if you solve some unsolvable constraints" behavior of evar_conv_x,
getting more common after patch on evars and eta. The main problem is that ?X = C[?X] problems get
postponed now, when they failed earlier before (rendering the algorithm incomplete, e.g. on ?X = \y. ?X y).
A notion of "rigid/strongly rigid" occurrences would give a better fix.
Fixing bug #3541.

All superscript numbers are now symbols instead of parts of identifiers.
This disallows some identifiers, but hopefully not a lot of people were
using superscripts as part of identifiers, weren't they?
Adding test-suite for bug #3212.
Cleaning and documenting a bit the Proofview.Refine module.
Fixing an unnatural selection of subterms larger than expected in the
presence of let-ins.
There are some occurs-check cases that can be handled by imitation (using pruning),
hence do not entirely prevent solve_simple_eqn in case of apparent occurs-check but
backtrack to eqappr on OccurCheck failures (problem found in Ssreflect).
Fix bugs #3484 and #3546.
The unification oracle now prefers unfolding the eta-expanded form of a
projection over the primitive projection, and allows first-order
unification on applications of constructors of primitive records,
in case eta-conversion fails (disabled by previous patch on eta).
Change the way primitive projections are declared to the kernel.

Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
Simplification of the tclCHECKINTERRUPT tactic.
Fixing bug #3528.
Fix bug when defining primitive projections mixing defined and abstracts fields.
Add test-suite file. Compute the name for the record binder in the
eta-expanded version of a projection as before.
Fixing commit 50237af2.

Indeed, generalized binders are unnamed, because their name is generated on the
fly.
Not using a "cut" in descend_in_conjunctions induced more success. We
at least remove the successes obtained by trivial unification of a
meta with the goal, so as to avoid surprising results. We generalize
this to variables which will only eventually be replaced by metas.
Simplification of Genarg unpackers.

Instead of having a version of unpackers for each level, we use a dummy argument
to force unification of types.
Type-safe version of genarg list / pair / opt functions.
Simplify even further the declaration of primitive projections,
now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.
Moving code of tactic interpretation from Tacenv to Vernacentries.

This allows to directly register globtactics in the Tacenv API, without
having to resort to any internalization function.