Stream: Coq users

Topic: #[universes(template)]?


view this post on Zulip Shea Levy (Oct 12 2020 at 15:16):

I see in the stdlib some annotations like #[universes(template)], is this documented anywhere?

view this post on Zulip Enrico Tassi (Oct 12 2020 at 15:21):

Here: https://coq.github.io/doc/master/refman/coq-attrindex.html

view this post on Zulip Shea Levy (Oct 12 2020 at 15:28):

Ah, so it's about universe of params. Thanks!

view this post on Zulip Théo Zimmermann (Oct 12 2020 at 20:11):

Note that there is an off-by-default warning when you rely on Auto Template Polymorphism instead of putting these annotations.


Last updated: Jan 29 2023 at 06:02 UTC