Stream: Ltac2

Topic: Ltac2 Eval Std.unify

view this post on Zulip Jason Gross (Sep 07 2023 at 21:17):

Why (and how) does Ltac2 Eval believe that True and False are unifiable? https://github.com/coq/coq/issues/18021

view this post on Zulip Rodolphe Lepigre (Sep 07 2023 at 21:36):

I think the reason is that there is no goal when running Ltac2 Eval, and the unification function (Tactics.unify form tactics/tactics.ml) does Proofview.Goal.enter...

view this post on Zulip Rodolphe Lepigre (Sep 07 2023 at 21:44):

(I also replied in the issue: https://github.com/coq/coq/issues/18021#issuecomment-1710805593 with more details.)

Last updated: Oct 12 2024 at 13:01 UTC