metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard

"tm* must take n arguments" errors are incorrect

Open JasonGross opened this issue 2 years ago • 0 comments

run_template_program (@tmQuote) (fun v => pose v). tells me tmQuote takes 3 arguments (it only takes 2) run_template_program (@tmQuoteModule) (fun v => pose v). tells me tmQuoteModule takes 0 argument (the pluralization is wrong) (any it takes 1)

JasonGross avatar Feb 14 '23 02:02 JasonGross