Simplifying the use of hypinfos in Rewrite.
cleanup warning
Future: optional greedy chaining

If a Future.computation is already a value v or an exception and
is chained in a greedy way with a function f, then f v is executed
immediately (or the exception is raised).
CoqIDE: new feedback "incomplete" to signal partial Qed
Qed: feedback when type checking is done

To make this possible the state id has to reach the kernel.
Hence definition_entry has an extra field, and many files had
to be fixed.
STM: capture type checking error (Closes: 3195)

Also, the future chain that reaches the kernel is greedy.
If the user executes step by step, then the error is raised immediately.