Cryptic error when using comma-separated declaration syntax in SharedDefinitions

[rbohrer]

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)

MWE:
CommaSeparatedSharedDefinitionsCrypticError.kyx.txt