The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Apr 18, 2011 at 11:41:13AM -0400, Randy Pollack wrote:
> Matita (from Bologna) has some kind of explicit universe notation.

And this is the most up-to-date description of them (pages 2 and 3):
 
  http://matita.cs.unibo.it/docs/tutorial/igft.pdf

We were also pondering on quantifiers (as proposed earlier on this list) but 
we never tried to prototype them, nor study their theory. 

The closest thing that was (partially) implemented was a command to
duplicate CIC objects applying to them a sort-substitution (without
manually duplicating .v files of course).

Cheers
-- 
Enrico Tassi