Stream: MetaCoq

Topic: Debugging anomalies

view this post on Zulip Jason Gross (Oct 31 2022 at 23:34):

Is there a good way to figure out what's giving Error: Anomaly "in retyping: unbound local variable." in a MetaCoq template program?

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:38):

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