STM: VtQuery holds the id of the state it refers to
STM: encapsulate Pp.message in Feedback.feedback
STM: use a real priority queue
STM: generate Feedback message for parsing errors
STM: when looking up in the cache catch Expired exc
Fixing semantics of Univ.Level.equal.
Fix an exponential behavior in guard checker for cofixpoints.

I had introduced it by mistake due to my OCaml dyslexia :)
Thanks to Enrico and Arnaud for saving my day!
More optimization in guard checking.

When dynamically computing the recarg tree, we now prune it according to the
inferred tree. Compilation of CompCert is now ok.
One more optimization for guard checking of cofixpoints.

In check_one_cofix, we now avoid calling dest_subterms each time we meet a
constructor by storing both the current tree (needed for the new criterion)
and a precomputed array of trees for subterms.
Better fix of e5c025
Fix [uconstr] name for argextend.
Properly declare uconstr as an argument for TACTIC EXTEND.
Small refactoring: use [uconstr] instead of [constr] when relevant in grammar rules.
The [refine] tactic now accepts [uconstr].

Arguments of refine can hence be built by tactics instead of given in their entirety in one go.
Fix interpretation bug in [uconstr].

Substitution of the Ltac variables would only occur if the internalised [uconstr] was of the form [glob, Some expr], which is the case only in tactics defined inside a proof, but not in tactics defined in [Ltac].
Doc: uconstr now has a tactic notation entry.
Documentation: refine accept uconstr arguments.
Documentation of [uconstr]: typesetting.
Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].

When "entering" in a goal, the environment observed by [tclENV] is changed (in the scope of the goal) to be that of the goal.

I'm not entirely sure it is the right semantics. But it allows to write tactics which are agnostic of whether they are run in a goal or not.
Tacinterp: [interp_message] and associate now only require an environment rather than an entire goal.