The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Looks like load is broken, you can report the bug on github.

Gaëtan Gilbert

On 08/01/2020 09:55, Jeremy Dawson wrote:
> Hi,
>
> I don't understand this behaviour
>
> Given a file sup.v as follows:
>
> Set Universe Polymorphism.
> Test Universe Polymorphism.
> Set Printing Universes.
> Test Printing Universes.
> Definition relationT (A : Type) := A -> A -> Type.
> About relationT.
> Test Universe Polymorphism.
> Test Printing Universes.
> Print relationT.
>
> when I load the file the flag Universe Polymorphism doesn't apply to the
> definition of relationT, and gets turned off (though another flag I
> tried doesn't get turned off)
>
> [jeremy@localhost modal]$ coqtop -color no
> Welcome to Coq 8.8.2 (January 2019)
>
> Coq < Load sup.
> The universe polymorphism mode is on
> The printing of universes mode is on
> relationT is defined
> relationT : Type@{Top.1} -> Type@{max(Top.1,Top.2+1)}
>
> Argument scope is [type_scope]
> relationT is transparent
> Expands to: Constant Top.relationT
> The universe polymorphism mode is off
> The printing of universes mode is on
> relationT =
> fun A : Type@{Top.1} => A -> A -> Type@{Top.2}
>        : Type@{Top.1} -> Type@{max(Top.1,Top.2+1)}
> (* {Top.2 Top.1} |=  *)
>
> Argument scope is [type_scope]
>
> whereas when I compile the file I get (as I would have expected)
>
> [jeremy@localhost modal]$ coqc sup.v
> The universe polymorphism mode is on
> The printing of universes mode is on
> relationT@{sup.1 sup.2} :
> Type@{sup.1} -> Type@{max(sup.1,sup.2+1)}
> (* sup.1 sup.2 |=  *)
>
> relationT is universe polymorphic
> Argument scope is [type_scope]
> relationT is transparent
> Expands to: Constant sup.relationT
> The universe polymorphism mode is on
> The printing of universes mode is on
> relationT@{sup.1 sup.2} =
> fun A : Type@{sup.1} => A -> A -> Type@{sup.2}
>        : Type@{sup.1} -> Type@{max(sup.1,sup.2+1)}
> (* sup.1 sup.2 |=  *)
>
> relationT is universe polymorphic
> Argument scope is [type_scope]
>
> What is happening here?
>
> Thanks
>
> Jeremy