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: Jun 13 2024 at 07:01 UTC