metacoq icon indicating copy to clipboard operation
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

Open JasonGross opened this issue 2 years ago • 0 comments

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.

JasonGross avatar Feb 12 '23 05:02 JasonGross