- Fix printing of universe instances that should not be factorized blindly
- Fix handling of the universe context in program definitions by allowing the
hook at the end of an interactive proof to give back the refined universe context,
before it is transformed in the kernel.
- Fix a bug in evarconv where solve_evar_evar was not checking types of instances,
resulting in a loss of constraints in unification of universes and a growing number
of useless parametric universes.
Merge branch 'univpoly' of /Users/mat/research/coq/git into trunk