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.