metacoq
metacoq copied to clipboard
"tm* must take n arguments" errors are incorrect
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)