Mark notation as "only printing"

Unfortunately, we currently have to keep the unicode-space hack because Coq still complains about the notation otherwise