metacoq
metacoq copied to clipboard
Please add a function for checking if a kername is valid in the global environment, or if it will disappear when the file is finished
I want a variant of tmCurrentModPath that returns only the prefix of the current modpath which does not contain any functors. This is necessary for writing automation that tries to quote terms for long-term use.