Restore the possibility to give a name to a universe in an inductive definition

In standard Coq, it is possible to define a new constant whose value is a sort, and then use this constant in inductive definitions.  This fails if the option -indices-matter is on.  The proposed patch restores this possibility.

Here is an example of program that fails without the correction.

Definition UU := Type. Inductive toto (B : UU) : UU := c (x : B).