Jason Gross (Oct 06 2022 at 13:11): 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?
Enrico Tassi (Oct 06 2022 at 20:12):How do you assign evars?
Enrico Tassi (Oct 06 2022 at 20:12):because "unification" does occur check...
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: Jun 04 2023 at 19:30 UTC