Accepting conversion on inner closed subterms while looking for
matching subterm destruct/induction on a partially applied
pattern. AFAICS, there is only such instance of destruct that needs
this in the contrins (in EuclideanGeometry/G3_ParticularAngle.v), but
while a more global decision is taken, I prefer at the current time to
adopt this approximation of 8.4 semantics, even if the flags are not
the same when the pattern is fully applied or not. Only so little
cases are concerned because in most cases, destruct/induction on a
partially applied pattern is of the form "destruct cst"
(e.g. "destruct eq_dec") and no conversion is needed anyway.

Not being uniform whether the pattern is fully applied or not is a bit
unsatisfactory, but hopefully, this is temporary.
Cleaner interfaces for linking locations of native compiler.

Stop sharing those references across constants of the same
module, which was triggering some bugs when using native_compute
in interactive mode in a functor declaration.
Adding a terminal library.
Adding a new tag for pretty-printer, based on string lists.
Tentative tag for keyword
tentative plugging of the highlighting mechanism.
More in Terminal