Fixed some HoTT bugs, provide a proper error message when giving an ill-formed
universe instance.
Fix computation of inductive level in monomorphism + indices-matter mode.
Fixes bug #3346.