metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard
verified publisher icon MetaCoq

Request: `tmOpenModule` and `tmCloseModule`

Open JasonGross opened this issue 2 years ago • 0 comments

I'd like to be able to script adding definitions in submodules of the current module

JasonGross avatar Feb 21 '23 21:02 JasonGross