Typos in comment.
In Ltac's exact tactic: avoid checking the type of the term twice.

Following a remark by Jason Gross and Daniel Grayson.
Removing the [Require "file"] syntax.
Fixing bug #3226.
Fixing backtrace reporting.
Allocation friendly map-handling functions in Dag.
Allocation-friendly mapping functions in Nametab.
Tracking memory misallocation by trying to improve sharing.
The constructor tactic now returns several successes.
Tactic extensions do not need to be classified by the STM, as
they never produce a VernacExtend entry.
FinFun.v: results about injective/surjective/bijective fonctions over finite domains

 + Some extra results about NoDup, Fin.t, ...
Less dependencies in Omega.
Small optimizations in Closure:

1. Only apply last Zupdates
2. Better smartmap with state.
Tentative fixup for the previous commit. It seems I have broken something
nasty relating memory management triggering random segfaults. But this seemed
really unlikely...
fake_ide: ported to spawn
STM: be conservative w.r.t. proofs containing global side effects
STM: when a worker is canceled mark the proof as broken
STM: fix valid_id coming from Qed errors
Timeout and Set Default Timeout fixed (closes: #3229)
Made Pre_env.lazy_val opaque.