The Coq mailing list

[Frédéric Tuong <frederic.tuong AT inria.fr>]

Wed, 18 Apr 2012 15:31:30 +0200, Stéphane Glondu :
> This is not a bug for me, merely an unfortunate convention.
Because this is clearly documented in the manual, this could not be a bug...
...as long as one does not attempt to extract :
https://coq.inria.fr/bugs/show_bug.cgi?id=843
> "Type" in this position means "infer", whereas most of the time it means
> "a new universe". As far as I know, there is no syntax for "a new
> universe" in this position. The "infer" semantics is needed for universe
> polymorphism.
As example, the OCaml syntax "_ : _" looks so identical to the Coq 
syntax "_ : _", that it can happen that one will not look at the 
semantic of the "_ ≤βδιζ _" conversion rule, described after the 
Ind-Family in the Coq manual section 4.5.3.

Frédéric