I'd like a way to determine (in MetaCoq, ultimately) if a constant will eventually be removed from the nametab. Is there a way (in Ltac, Ltac2, or MetaCoq, or even a convenient way in OCaml, I guess, which I can export to MetaCoq) to determine if a given module path contains any functors in it, or, as an approximation to this, a way to determine whether or not there's currently an open functor (importantly, we must be able to distinguish between open argumentless module/module type, and open functor/functor type)?
you may have to look at the safe_typing modvariant field to tell if an open module is a functor, together with the current modpath
let rec is_open_functor senv mp = match senv.modvariant with | NONE | LIBRARY -> false | (STRUCT (params, senv') | SIG (params, senv')) -> if ModPath.equal mp senv.modpath then not (List.is_empty params) else is_open_functor senv' mp
but modvariant is internal to safe_typing
I'm not sure the info is available anywhere else
Should I open an issue for exposing this information as an OCaml interface?
Last updated: May 31 2023 at 16:01 UTC