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.
Ltac's idtac is now implemented using the new API.
Ltac's [idtac] is now interpreted outside of a goal if possible.

It avoids printing several times the same things when no constr are involved in the message. It also allows to print messages even after all goals have been solved.
Documentation: a simple example for [numgoals].

Now that [idtac] can print a single message for several goals, printing the number of goals is readable.
Ring: prevent an error message to show in case of success.

Since [idtac] can, now, be used even if no goal is left, this error message which assumed that the goal was still open would run at every call of the [ring] tactic. Which lead to comically many nonsensical messages on the console during Coq's compilation.
Coqide: annoying popups with GTK errors only in debug mode
STM: Classify Let as non asynchronous (Closes: #3486)