Michael Soegtrop (Mar 08 2022 at 16:31): 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.
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.
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: Apr 19 2024 at 12:02 UTC