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)
make a few lines fit the screen
Goal: API to get the solution of a goal
STM: code restructured to reuse task queue for tactics
STM: new "par:" goal selector, like "all:" but in parallel

par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).
Coqide: check_connection now also checks correct loading of coqide plugin +
reports errors also from stderr.
Chapter 4 of reference manual: Fixing asymmetric patterns error +
no spacing in English before ":".
Making references to Proof General and CoqIDE uniform in Reference Manual.
More proofs independent of the names generated by induction/elim over
a dependent elimination principle for Prop arguments.
A new step in the new "standard" naming policy for propositional hypotheses
obtained from case analysis or induction. Made it under experimental status.

This replaces commit bf7d2a3ad2535e7d57db79c17c81aaf67d956965 which was
acting at the level of logic.ml. Now acting in tactics.ml.

Parts of things to be done about naming (not related to Propositions):
induction on H:nat+bool produces hypotheses n and b but destruct on H
produces a and b. This is because induction takes the dependent scheme
whose names are statically inferred to be a and b while destruct
dynamically builds a new scheme.
Adding a syntax "enough" for the variant of "assert" with the order of
subgoals and the role of the "by tac" clause swapped.
Testing a replacement of "cut" by "enough" on a couple of test files.
Experimentally adding an option for automatically erasing an
hypothesis when using it in apply or rewrite (prefix ">",
undocumented), and a modifier to explicitly keep it in induction or
destruct (prefix "!", reminiscent of non-linerarity).

Also added undocumented option "Set Default Clearing Used Hypotheses"
which makes apply and rewrite default to erasing the hypothesis they
use (if ever their argument is indeed an hypothesis of the context).
Fixing a few beautifying bugs.
Testing beautifying on an example.
Preliminary re-installation of notation interpretation in beautifying mode.
Improving printing of "[]" (nil) in spite of the risk of collision
with possible further use of token "[]" + slight restructuration.