Fix backtracking issue in Defined (Close 3780)
Better error messages when unfreezing summary entries
Show_script called only if in coqtop mode
STM: reorganize code and file names

- proofworkertop to deal with proof tasks
- tacworkertop   to deal with par: tactics
- queryworkertop to deal with queries (next commit)
STM: new worker for queries

With the options -async-queries-always-delegate queries are
always delegated to a worker process (Eval, Check, ...).

Users of PIDE based UIs (in Denmark) reported that the current
behavior of processing query synchronously is rather unexpected
when one is used to get proofs processed asynchronously.

Non instantaneous queries are part of many scripts and are there
as "tests" for testing the execution of recursive functions.
A standard proof script shape in an ongoing work by Appel and Bengtson
is made of blocks like:
- recursive function definition,
- some tests,
- some proofs
And one cannot quickly jump over the tests (only the proofs).
Enclosing the queries into dummy proofs to recover a reactive UI
is just annoying.  Hence this patch.

Currently CoqIDE is not able to integrate the asynchronous feedback
of the query workers into the document, hence if one passes the option
to CoqIDE one only gets a boolean out of queries (processed/error).
Feedback message: hold extra info to help routing

PIDE based GUIs can take advantage of multiple panels and get
some feedback routed there. E.g. query panel
Avoid "destruct H" to apply on H itself when H is a section variable.

Need some contorsion for not using the general scheme of naming based
which uses the hypothesis name as base ident, and for instead keeping
a name generated on the type of the section variable, as it was before
for section variables (example of incompatibility in FMapPositive).
Listing a few examples of destruct showing unsatisfactory behaviors.
Enlarge the cases where the like first selection is used in destruct.

This is now a "like first" strategy iff there is no occurrences
selected in either the goal or in one of the hypotheses possibly given
in an "in" clause. Before, it was "like first" if and only if no "in"
clause was given at all.
More "open" by default for trace debugging.
Reorganization of the test for generic selection of occurrences in
clause; extended it so that an induction over "x" is considered
generic when the clause has the form "in H |-" (w/o the conclusion)
and x does not occur in the conclusion.
An API for info traces.
Add [Info] command.

Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
Info: dispatching-branches are declared as such in the info trace.

Hence dispatches are printed as dispatches rather than sequences.
Info: print a name for the primitive tactics in [Proofview].

The name is chosen in accordance to Ltac's syntax. In particular [refine] prints as Ltac's refine, which is not entirely correct (Ltac's refine does some βι-reduction after refinement). Maybe it would be better to give make it clear that it is a different refine. Still in refine, the constr is printed without taking into account the new evars, which, apart from potentially getting the order of the goals wrong, prints new evars as ?x instead of ?[x]. A printer for terms with new evars will be necessary.

In the case of [V82.tactic], the name is just <unknown> because there is no way to retrieve any information. It won't appear in the first level of info in Ltac, however, if the user would require a deeper trace, he may see internal tactics (Tactics defined with TACTIC EXTEND also have weird, unparsable, internal names).
Info: Ltac's idtac logs its message in the info trace.
Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.

Re-add, in fact, since it was there in v8.3 but was dead code in v8.4 hence was deleted. It is necessary for printing info traces, however. A lot of the code had changed since v8.3, so adapting the code was non-trivial and some thing may be printed wrong.

It require re-adding a [tacexpr] argument to [gen_tactic_expr]. It had been made obsolete by the deletion of [pr_tactic] in v8.4 (even though printing [glob_tactic_expr] in a [tactic_expr] is only an approximation of the appropriate behaviour).

A new kind of argument, [delayed_constr], has made an appearance between v8.4 and trunk, and it differs from [constr] in the typed level. So it required its own parameter in [gen_tactic_expr]. At this point [delayed_constr] are printed in the globalised level because they are interpreted as closures. Maybe a better approximation is warranted.

Both in the printing of rewrite and induction, I changed a [pr_lconstr] (note the 'l') by a [pr_dconstr]. It is probably not quite correct, and may need fixing (adding a [pr_dlconstr] to [Pptactics] I guess?).
Info: print the name of atomic tactics.

The printing uses the printer for interpreted tactics. It only works for tactics which are defined in the new style. There are still a few atomic tactics in tacinterp which are defined in [V82] style. Namely:

exact, apply, clear, rename, reduce, change, (mutual variant of) fix, (mutual variant of) cofix

These print placeholder names which are never reparsable and not as useful.
Info: Tactics coming from [TACTIC EXTEND] print their names.

Since PMP's intervention, the [TACTIC EXTEND] tactics are not uniform: some are syntax, and some are just an internal name for an Ltac definition. The latter kind prints an internal name. It may be better to avoid printing them in the trace altogether. But I haven't figured out how to detect that properly yet.
Info: tactic notations (TacAlias) print their names.

Empirically it works better on some notations than on others and I have no idea why. I've seen notations not printing their arguments, for instance, and other printing perfectly.