Stream: Ltac2

Topic: Go back and forth issue in VsCoq


view this post on Zulip Michael Soegtrop (Mar 08 2022 at 16:31):

@Pierre-Marie Pédrot : do you remember (https://github.com/coq/coq/issues/12575) - the issue that going back and forth over the Ltac2 require messed up things? Do you remember how this was fixed? The issue is still open, but it is fixed in 8.14 and 8.15. I am asking because VsCoq has the same issue.

view this post on Zulip Pierre-Marie Pédrot (Mar 08 2022 at 17:05):

If this was fixed in Coq it should also be fixed in vscoq? I don't remember what could have fixed it though.

view this post on Zulip Michael Soegtrop (Mar 08 2022 at 17:56):

One might think so, yes, but apparently it isn't. It could of course be a different issue but I would say this is unlikely.


Last updated: Jan 31 2023 at 09:01 UTC