Test case for the buggy commutative cut subterm rule.
Notations can now accept dummy arguments. If ever a bound variable is not
used, they are automatically flagged as only parsing. CAVEAT: unused
arguments are not typechecked, because they are dropped before the
interpretation phase.
Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at
internalization time.
Notation variables are now taken into account as possible ltac bound variables
when internalizing a term.
Adding a finer-grained -bt flag to coqtop only triggering backtraces.
Adding -bt to coqc.
Slight code cleaning ensuring more static invariants in Rewrite.
Do not pass unification flags around in Rewrite.
Rewrite.ml: removing direction flag from hypinfo.
Simplifying the use of hypinfos in Rewrite.
cleanup warning
Future: optional greedy chaining

If a Future.computation is already a value v or an exception and
is chained in a greedy way with a function f, then f v is executed
immediately (or the exception is raised).
CoqIDE: new feedback "incomplete" to signal partial Qed
Qed: feedback when type checking is done

To make this possible the state id has to reach the kernel.
Hence definition_entry has an extra field, and many files had
to be fixed.
STM: capture type checking error (Closes: 3195)

Also, the future chain that reaches the kernel is greedy.
If the user executes step by step, then the error is raised immediately.
Removing native_name reference from constant_body.

For now, this reference (renamed to link_info) has been moved to the
environment (for constants and inductive types). But this is only a first step
towards making the native compiler more functional.
Revert "Partial revert of r16711"

The sharing introduced by this commit is now correct, since a reference used by
the native compiler has been removed from constant_body.

This reverts commit 413f5fcd4bf581ff3ea4694c193d637589c7d54f.
Got rid of unused lazy flag in the native compiler.
Avoid generating .ml files in native compiler.
Support for evars and metas in native compiler.

Experimental. Turned out to be much harder to implement than I thought. The main
issue is that the reification in the native compiler and the VM is not quite
untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence,
when reifying an application u = t a1 ... an, the type of t has to be known or
reconstructed. It is always possible to do so in plain CIC, when u is in normal
form and its type is known. However, with partial terms this may no longer be
the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of
evars and metas.

This still has to be tested more extensively, but the correction of the kernel
native conversion (on terms without evars or metas) should not be impacted.

Much of this could be reused for the VM.