Stream: Coq devs & plugin devs

Topic: ✔ Changes to Declarations.universes from Coq 8.9 to 8.10

view this post on Zulip Arpan Agrawal (Aug 07 2023 at 20:01):

Okay, thanks a lot! One last question, what does the new names array in the Polymorphic_entry constructor represent? It doesn't exist in the previous version

view this post on Zulip Gaëtan Gilbert (Aug 07 2023 at 20:33):

the names of the bound universes for printing
they were in some global reference before

view this post on Zulip Arpan Agrawal (Aug 07 2023 at 20:40):

Got it. Thanks again!

view this post on Zulip Notification Bot (Aug 07 2023 at 20:40):

Arpan Agrawal has marked this topic as resolved.

Last updated: Dec 05 2023 at 12:01 UTC