Fix test-suite script for HoTT coq bug #34
The test-suite file couldn't typecheck as it rightly introduces a universe inconsistency.
One needs to use a universe level lower than eq's parameter for this to be consistent.
The uses of the funext axiom forced levels to Set, relaxing its use doesn't.
Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.
Fix semantics of change p with c to typecheck c at each specific occurrence of p,
avoiding unwanted universe constraints in presence of universe polymorphic constants.
Fixing HoTT bugs # 36, 54 and 113.
Oops, I fixed the .ml's
Removing opens to Clenvtac to track its use more easily.
Clenvtac.unify is in the new monad.
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.
Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)

Every time you use abstract a kitten dies, please stop.
Clenvtac.res_pf is in the new tactic monad.
Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it
exhibits the "useless goal" behaviour: there is code out there depending on
the fact that goals cannot be solved by side effects.