Switch the few remaining iso-latin-1 files to utf8
Setup hook to change the unification algorithm used by evarconv,
e.g. for MTac.
test-suite: few tests for ".v -> .vi -> .vo" compilation chain
typo
Using a more aggressive test for resolving pattern equations ?n = ?p:
test pattern-unification after restriction of the evars so as to
succeed earlier (no observational changes however in the examples at my
disposal).
Fixing orientation of postponed subtyping problems.
In the case of conversion, postponing by preserving the
initial orientation.

Was wrong from its initial version in Jan 2014, but was not visible
because evar-evar subtyping was approximated by evar-evar conversion.

Thanks to Enrico for a very short example highlighting the problem. In
particular, this fixes Ergo.
Revert commit that inverted the preference for FFlex/FProj problems in
kernel reduction.
Fix dummy argument use in guess_elim: there are some cases where X_ind
is not defined while X_rect is, for example in HoTT/Coq.
Adding a small lightweight thread library.
STM in LWT.
More in LWT