Is there a good way to figure out what's giving
Error: Anomaly "in retyping: unbound local variable." in a MetaCoq template program?
That's the retyping from Coq I guess, you could try to pretty-print the term before it's sent to Coq's kernel I guess
Last updated: Jun 01 2023 at 12:01 UTC