Stream: Coq devs & plugin devs

Topic: Debugging cyclicly defined evars


view this post on Zulip Jason Gross (Oct 06 2022 at 13:11):

I wrote some Ltac2 code. It succeeds. However, Show Proof, Optimize Proof, and Qed all stack overflow instantly. How do I track down the issue?

view this post on Zulip Enrico Tassi (Oct 06 2022 at 20:12):

How do you assign evars?

view this post on Zulip Enrico Tassi (Oct 06 2022 at 20:12):

because "unification" does occur check...

view this post on Zulip Jason Gross (Oct 13 2022 at 16:27):

(Belatedly) I assign goal evars with refine and some other evars with unification. I managed to bypass the issue by using Ltac2.Control.new_goal instead of Ltac2.Control.refine for evar assignment


Last updated: Feb 05 2023 at 20:03 UTC