Enrico Tassi (Apr 26 2021 at 10:26): Enrico Tassi (Apr 26 2021 at 10:26):Is there a way to know if we are in the middle of a functor?
Pierre-Marie Pédrot (Apr 26 2021 at 10:29):not that I know of
Pierre-Marie Pédrot (Apr 26 2021 at 10:29):you might try your luck hacking with the closing functions in Lib
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.
Enrico Tassi (Apr 26 2021 at 10:39):I would like to give a nice error if you put elpi code in a functor...
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
Enrico Tassi (Apr 26 2021 at 11:02):https://github.com/coq/coq/pull/14172
Last updated: Sep 15 2024 at 13:02 UTC