@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.
If this was fixed in Coq it should also be fixed in vscoq? I don't remember what could have fixed it though.
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: Dec 05 2023 at 05:01 UTC