Stream: Coq devs & plugin devs

Topic: API to know if we are in a functor


view this post on Zulip Enrico Tassi (Apr 26 2021 at 10:26):

Is there a way to know if we are in the middle of a functor?

view this post on Zulip Pierre-Marie Pédrot (Apr 26 2021 at 10:29):

not that I know of

view this post on Zulip Pierre-Marie Pédrot (Apr 26 2021 at 10:29):

you might try your luck hacking with the closing functions in Lib

view this post on Zulip Enrico Tassi (Apr 26 2021 at 10:39):

And if I wanted to add it? There is a Safe_typing.sections_are_opened, but I don't get what I should look at to implement a similar one for functors.

view this post on Zulip Enrico Tassi (Apr 26 2021 at 10:39):

I would like to give a nice error if you put elpi code in a functor...

view this post on Zulip Pierre-Marie Pédrot (Apr 26 2021 at 10:40):

Yes, you can add it as well. Safe_typing has access to the list of parameters of the current functor so you could rely on that

view this post on Zulip Enrico Tassi (Apr 26 2021 at 11:02):

https://github.com/coq/coq/pull/14172


Last updated: Mar 28 2024 at 14:01 UTC