Fix compilation error in some configurations.

This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select".

Fixes #3877.
Remove compatibility layer from Ltac's [fail].
A global [gfail] tactic which works like [fail] except that it fails even if there is no focused goal.

The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
Minor modification of CHANGE.
Vi2vo: fix handling of univ constraints coming from the body
STM: cleanup code for Admitted
Adding a small lightweight thread library.
STM in LWT.