PG accepts newlines in Coq notations while this is forbidden

[erikmd]

I just noticed that PG removes newlines sometimes in a slightly aggressive way, so that is possible to parse a Coq file that doesn't compile, but is accepted by PG.

Minimal working example (mwe.v)

Parameter Under : forall (I : Type) (i : I) (R : Type), R -> R -> Prop.
Notation "i : I
−−−−−−−−−−−−−−−−−−−−−−−−−−−−
x" := (@Under I i _ x _) (at level 200, format
"'[v' i  :  I '/'
−−−−−−−−−−−−−−−−−−−−−−−−−−−−
'/' x ']'", x at level 200).

Actual result

$ coqc mwe.v
File "./mwe.v", line 2, characters 0-279:
Error: x is unbound in the notation.

Expected result

PG also rejects this file.