Make the library work with the current version of HoTT/coq trunk

The library needs to be modified for two reasons
- In file Universe.v , there is a definition that does not go through.  It used to be written as non-dependent pattern matching, but it is in fact dependent, and therefore it should have a "return" clause.

- The new version of Coq has a native compiler, but it does not react well to empty files.  New options need to be added to the packaging scripts (hoqtop, hoqtop.byte, etc) and to the Makefile to deactivate this native compiler.