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

not that I know of

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

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.

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

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

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

Last updated: Dec 05 2023 at 06:01 UTC