The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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