Fixing wrong notation level in #3295.
Back to the preferred ?n1:=?n2 order of evar-evar unification which got accidentally mixed up in 9aa416c0c6.
Better doc and a few fixes for Proof using.
Fix sigsegv in checker
update md5 sums to make "make check" work
Fixing checker representation of values.
Fixing performance issue of checker validation.

The validation process was passing most of its time in the construction of
the name of the current context.
When pretyping [uconstr] closures, don't use the local Ltac variable environment.

A closure is supposedly closed: all the relevant Ltac variables should be then. The last field [ltac_genargs], if I'm not mistaken, is there to represent the Ltac variables which are bound but not to something which makes sense in a term. They should be irrelevant at this point, since the uconstr has already been interpreted and these checks are supposed to have happened. (though I'm not entirely sure they do, it can be an interesting exercise to try and make [uconstr] behave weirdly)

I'm not quite sure why it caused #3679, though. But it still seems to be solved.
Add a backtracking version of Ltac's [match].

[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
Install .v and .glob files too

PIDE based user interfaces use glob files and source files to
implement hyperlinks
Win32: fix installer

Still unsure about .o file (should they be shipped for the native_compute
machinery or .cmxs suffice?)
Dead code in Univ.
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