More test-suite cases
Update some bugs about typeclass resolution
Force the final universe context of a proof only in poly || now case.
Fix program cases and inversion tactic to correctly record universe constraints.
Fixes FingerTree contrib.
Fix computation of Type argument for Program's fix_proto.
Use full transparent state when checking well-typedness of a second order matching
infered predicate, instead of the arguments ts which might be empty (e.g. in unification).
Fixes failure in success/unification.v
Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_depends.
Also add a missing constraint when generating a fresh universe for a template polymorphic
inductive in that case.
Use the right transparent state when comparing _types_ of metas.
In exact check, use e_type_of to ensure that universe constraints necessary
to typecheck the term are not forgotten. (relieves tactic implementors from
calling e_type_of themselves, e.g. in congruence). Fixes a bug found in Containers.
cut toploop(s) out of coqtop: now they are loaded dynamically

User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/
and pass -toploop footop to customize the coq main loop.

A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to
functions respectively initializing the toploop (and parsing toploop
specific arguments) and running the main loop itself.

For backward compatibility -ideslave and -async-proofs worker do
set the toploop to coqidetop and stmworkertop respectively.
all coqide specific files moved into ide/

lib/interface split into:
 - lib/feedback
     subscribe-based feedback bus (also used by coqidetop)
 - ide/interface
     definition of coqide protocol messages
   lib/pp
     structured info/err/warn messages

lib/serialize split into:
 - lib/serialize
     generic xml serialization (list, pairs, int, loc, ...)
     used by coqide but potentially useful to other interfaces
 - ide/xmlprotocol
     serialization of protocol messages as in ide/interface

the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
In rewrite, wrong computation of the sort of the term to be rewritten in
generated an uncaught Not_found. This raises an anomaly now and the sort is
properly computed now (fixes a bug in CoLoR).
Incorrect folding of evars in let_tac_gen made remember fail to store
correct constraints (bug found in CFGV).
Putting implicit arguments of Clenv.res_pf right.
Add an Unset Standard...
Change interface of refresh universes to get a pbty argument instead of
the computed direction argument. In case pbty is conv, no refreshing is done
as the evar body must be convertible with the given term, however refreshing
of template application evar arguments can still happen.
(Re)-Closing bug #2966.
Fix test-suite file for bug # 3036, the unification has _never_ succeeded,
as this would result in an ill-scoped substitution.
Fix test-suite file for opened bug #1596
Bug #3301 is closed, the projection cannot be defined anymore.
Fix test-suite files.