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.