I see in the stdlib some annotations like #[universes(template)]
, is this documented anywhere?
Here: https://coq.github.io/doc/master/refman/coq-attrindex.html
Ah, so it's about universe of params. Thanks!
Note that there is an off-by-default warning when you rely on Auto Template Polymorphism
instead of putting these annotations.
Last updated: Oct 13 2024 at 01:02 UTC