The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 6 Feb 2006, Carlos.SIMPSON wrote:

> Dear Russell,
>   We looked closely at this and you are right, the induction principle
> for the ``parametrized type'' is the same
> as for an unparametrized type in the new case when n changes inside the
> constructors.
> (Perhaps somebody could comment on why this change was made; apparently
> it is only for questions of universes?)

Indeed it appears to be only a question of maintaining universe
consistency.  See my thread at
<http://pauillac.inria.fr/pipermail/coq-club/2005/001732.html>, and also
Gonthier's response at
<http://pauillac.inria.fr/pipermail/coq-club/2005/001743.html>.

To be honest, I would have to put some effort into restuding my problem to
understand it again.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''