Patterns for local ghost values too restrictive
The parser seems to be too restrictive for patterns when defining local ghost values
let ghost PATTERN = EXPR in EXPR. Each of the lines marked with a-c are
refused with error "illegal ghost qualifier":
let constant u : unit = let e = (0, 0) in let ghost _ = e in (* a *) let ghost _, y = e in (* b *) let ghost (x, y) = e in (* c *) ()
But the lines marked with e-g are accepted.
let constant u : unit = let e = (0, 0) in let ghost _x = e in (* e *) let ghost _x, y = e in (* f *) let ghost x, y = e in (* g *) ()
I would expect all lines a-g syntactically valid in Why3 (as they were in version 0.88).