Error messages of Searchxxx are coherent with goal selector.

If a goal is given and wrong, exception is raised. If no goal is
given, then goal 1 is tried but no failure if goal 1 does not exist,
just fall back to gloab env.
Getting rid of Exninfo hacks.

Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.

To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.

The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
Proper thread-safe implementation for Exninfo.

This is the second part of the Exninfo patch. It introduces dependency in
the Thread library in all Coq files.
msg_info now puts infomsg tag in emacs mode.

Fixes the idtac "string" not appearing in proofgeneral because
printined *before* the goal.
Fixing CAMLP4 compilation.
fix bug #2447 in congruence
fix bug #2447 in congruence
Test for #3654.
More printers for ltac signatures.
In CHANGES, alerting about stronger check on notation level modifiers.
Moving #2447 (congruence) to fixed.
#3828 is solved.
Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must have x permission"

This reverts commit 607503b28fca50f4b76b2237d5ca13802b8252fa.
CoqIDE: better messages
Arguments: warn only if no option is given (Close 3860)
Dyn: add API to check of two Dyn.t are ==

A Dyn.t boxes a type tag with the original object, so calling
== on the Dyn.t does not work, hence this extra API.
Global: export the name of the summary entry

In this way one can make surgery on the system states, like
checking if two frozen states have the same environment (i.e.
no running "abstract" in between)
Summary: more surgery functions

API to let one forge a frozen state out of another frozen state
plus some frozen bits
CThread: use a different type for thread friendly in_channels
Spawn: fix request of Gc statistics