Hi vscoq devs, Coq PR#13663 is adding a new attribute in element
goal of the XML protocol, corresponding to a new field
goal_name to the type `Interface.goal. What should be done at the vscoq side (if any) in such a case? Thanks for help.
A change that just acknowledges the existance of that new field and fixes parsing, without using the name (yet?), probably involves only shifting the array subscript positions in the
goal case of the
Ah, this means that if the field had been the last one, that would have been transparent for vscoq. I can do that if needed.
Is there a fix incoming? VSCoq is unusable with master now.
@Hugo Herbelin Can you push your fix for master? I've been unable to make much progress this week due to TYPES and this very annoying bug.
@Matthieu Sozeau : you mean a fix that moves the new field at the end? That would be trivial.
Last updated: Jun 04 2023 at 23:30 UTC