(* This used to raise an anomaly *)

Fail Reserved Notation "x +++ y" (at level 70, x binder).