Deprecate options -dont, -lazy, -force-load-proofs.

These options no longer have any impact on the way proofs are loaded. In
other words, loading is always lazy, whatever the options. Keeping them
just so that coqc dies when the user prints some opaque symbol does not
seem worth it.
Deprecate useless option -unsafe.
Remove documentation for the unsupported options -byte and -opt.
Deprecate useless option -quality.
HoTT/coq bug #7 is closed, and the definitions can be made to go through using explicit
universes. The behavior of Hint Rewrite still differs from Hint Resolve though.
Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead of an anomaly in case
a universe inconsistency occurs when applying a coercion. The statement of the test-suite file
cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat
to Set.
- Fix xml plugin treatment of inductives.
- Move HoTT bug #30 to closed
Remove HoTT bug #33, as the stdlib won't become polymorphic in the next version.
The semantics of Variable x y : T is to have the exact same type T for x and y,
while Context gives different type to each variable, this test-suite file shows this.
Change Ltac constr matching semantics to consider universes when merging two
bindings of the same variable (fixing HoTT bug #52). Document the unification
of universes in Ltac/tactics.
Fix test-suite file
Preemptively remove files from native compilation.

Ocaml does not remove the .cmi file if compilation fails, thus causing
subsequent native compilations to fail due to mismatching interfaces.
For the sake of homogeneity, also remove the .cmo/.cmxs file along the way.
Fix spacing in error message.
HoTT bug #29 is fixed, using the correct notion of polymorphic product types.
- Add "Show Universes" to print information about universes during a proof.
- Remove dead code in evarconv.
Fixing part of HoTT bug #61 (in declare_evar_from_virtual_equation,
fix the type of the term which has to be in the signature of the evar
to declare); some problems remain though (see next commit).
Unification in HoTT_coq_061.v was looping with previous commit (while
it was failing with Not_found before previous commit). This "fixes"
the loop by expanding local defs in "imitate" rather than keeping them
explicit. The example is otherwise too large for me to be able to
understand where does the loop come from.
Checking that a library name is valid before compilation.

Fixes bug #3333.
Improve hotspot in Auto.
Existing Class now works with universe polymorphism. Fixes HoTT bug #063