Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).
check_for_interrupt: better (but slower) in threading mode

Experimenting with PIDE I discovered that yield is not sufficient
to have a rescheduling, hence the delay.
more APIs in TQueue and CThread

These are now sufficient to implement PIDE
CoqIDE: on win32 the old interrputer code (SIGINT) is still needed
option to always delegate futures to workers
Overlooked to remove a change in kernel/closure that made reducing under
a primitive projection impossible.
Better handling of the universe context in case of Admitted proof obligations.
MSetRBT: unfortunate typo in compare_height (fix #3413)
make the standard logging facility stm aware
Export type_of_global_ref (useful for external users of glob files)
Feedback: LoadedFile + Goals

LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
STM: export the observe function (useful for pide)
STM: add optionally takes the id of the new tip
STM: flag to turn off branch reopening

This is useful if a UI does not support that
STM: let toploop plugins specify the flags for STM workers
An outdated comment + comment layout.
Properly add a Set lower bound on any polymorphic inductive in Type with
more than one constructor.
Fix Funind test-suite file after patch by Pierre.
Adding a "time" tactical for benchmarking purposes. In case the tactic
backtracks, print time spent in each of successive calls.
Mentioning the incompatibility due to fixing bug #2996 (see #3418).