Writing tclABSTRACT in the new monad. In particular the unsafe status is now
preserved.
Adding a [fold_map] operation on constrs.
Fix a small typo in Termops.eta_reduce_head.
Fixing various backtrace recordings.
Adding a debug printer for futures.
Fix a second, trickier, typo in Termops.eta_reduce_head.
print futures in caml toplevel too
Opaqueproofs: sink futures when interactive
Future: memory optimization when forcing a chained pure computation

Kudos to PMP for spotting that!
Removing useless try-with clauses in Goal.enter variants.
Removing Autoinstance once and for all.
Adding a stm/ folder, as asked during last workgroup. It was essentially moving
files around. A bunch of files from lib/ that were only used in the STM were
moved, as well as part of toplevel/ related to the STM.
coq_makefile: -I for the new stm/ dir
Giving true proof-terms in inversion instead of metas.
Rewriting [lapply] tactic in the new monad.
Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to
one_inductive_body so that when eta-expanding at "match" printing time
we know if a let is part of the expected signature or part of the
body.

This is an easy fix for bugs like #3293. Another fix could be to
enforce, as an invariant, or better syntactically, that
"match"/"Case"'s have the body of their branches expanded.
Fixing #3293 (eta-expansion at "match" printing time was failing
because of let-in's interpreted as being part of the expansion).
Fixing coqdoc bug #3292 (unfortunate collision betweens the relative
locations found when parsing expressions in comments and the absolute
locations in the glob file).

As now, the glob file does not parse comment, so I removed the test
for location when parsing expressions in comments, which anyway are
not linkable, precisely because not parsed by coqc.
Fix incorrect syntax highlighting after the Goal command.
Fix broken commit 2bcb2cb.