HoTT/coq — pull request #12 by ybertot (2013-02-03 23:56:10+00:00)
Title: 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).