Cryptic error when using comma-separated declaration syntax in SharedDefinitions #76
Description
See attached MWE. When I use comma-separated syntax to declare multiple uninterpreted symbols in a single declaration in the SharedDefinitions section, I get the following error message, which was less clear than expected. This only occurred with the SharedDefinitions section. The other sections worked fine.
I know there's a special step in KeYmaera X that takes the shared definitions and turns them into regular definitions that get duplicated across each theorem. If I had to guess, maybe something goes wrong at that step. But I have not checked at all, it's merely a guess.
Got: parser error message:
At line -1:-1: Even though archive parses, extracted problem does not parse (try reformatting): SharedDefinitions Real x, , y. End. Theorem "ReproduceCrypticErrorForCommaSeparatedConstantDeclarations" Problem. (x()+y())^2 >= 0 End. End.
Expected: Either the syntax is supported or the error message is more specific (e.g. points to the comma and says it's invalid syntax)