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