Notation `(⊢@{PROP})` and `(⊣⊢@{PROP} )` broken
Apparently !384 (merged) did break these notations...
Minimized example. The following works:
Notation "(⊢@{ PROP } )" := (eq (A:=PROP)) (only parsing).
Definition test PROP := (⊢@{PROP}).
But the following doesn't:
Notation "('⊢@{' PROP } )" := (eq (A:=PROP)) (only parsing).
Definition test PROP := (⊢@{PROP}).
(* Syntax Error: Lexer: Undefined token *)