Changed syntax of explicit universes.
Fix test-suite script for subst working with let-ins, the following proof was rightly failing.
Fix for bug 1951, allowing at least fully-applied inductives types to be used
for building polymorphic instances of template polymorphic inductives.
Add some compatibility notes on the changes to [change] and unification in general.