The Coq mailing list

[Adam Chlipala <adamc AT argus.EECS.Berkeley.EDU>]

I know that the Calculus of Inductive Constructions was created because 
the Calculus of Constructions was insufficient to represent some inductive 
types.  Can anyone on this list give a short characterization of which 
types require this extension, and/or perhaps the simplest example of such 
a type?

I'm interested in this in the context of trying to minimize the trusted 
code base needed to use results proved with Coq.  If compiled developments 
can be translated to the Calculus of Constructions, then I imagine it's 
possible to use a significantly simpler checker.