Unicode-Glyphen für Schlüsselwörter und Operatoren in Coq / Proof General unter Emacs

Diese Frage hat mit der Konfiguration des Coq-Modus in Proof General in Emacs zu tun.

Ich versuche, dass Emacs Schlüsselwörter und Notation in Coq automatisch durch die entsprechenden Unicode-Glyphen ersetzt. Es ist mir gelungen, fun als das griechische Kleinbuchstaben Lambda λ zu definieren, forall als das universelle Quantifizierersymbol ∀ usw. Ich hatte keine Probleme Symbole für Wörter zu definieren.

Das Problem ist, dass wenn ich versuche, die Operatoren => , -> , <-> usw. zu ihrem Unicode-Symbol ⇒ → ↔ zu definieren, werden sie nicht durch die entsprechenden Unicode-Glyphen in Coq ersetzt. Sie werden jedoch im *scratch* -Puffer ersetzt, wenn ich sie teste. Ich verwende den gleichen Mechanismus, um Unicode-Glyphen mit der Coq-Notation abzugleichen:

Ich vermute, das Problem ist, dass der Coq-Modus bestimmte Interpunktionszeichen als speziell markiert, also ignoriert Emacs meinen Code, um sie durch die Unicode-Zeichen zu ersetzen, aber ich bin mir nicht sicher. Kann mir bitte jemand etwas dazu sagen?