The Coq mailing list

[Valentin ROBERT <valentin.robert AT inria.fr>]

As for the list archive: https://sympa.inria.fr/sympa/arc/coq-club

- Valentin

On Sat, Jul 21, 2012 at 4:00 AM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> Hi,
> I noticed that Coq seems to have had universe polymorphism at one point, but
> no longer does (see commit message at the bottom of the message).  Is there
> somewhere that I can find an explanation of why this was removed, or can
> someone respond with an explanation?  (If it was discussed on coq-club
> before, are there archives of coq-club@, and can someone point me to them?)
>
> Thanks.
>
> -Jason
>
> commit 60bc3cbe72083f4fa1aa759914936e4fa3d6b42e
> Author: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
> Date:   Wed Apr 13 14:29:02 2011 +0000
>
>     Revert "Add [Polymorphic] flag for defs"
>
>     This reverts commit 33434695615806a85cec88452c93ea69ffc0e719.
>
>     Conflicts:
>
>         kernel/term_typing.ml
>         test-suite/success/polymorphism.v
>
>     git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998
> 85f007b7-540e-0410-9357-904b9bb8a0f7