Символы Unicode для ключевых слов и операторов в Coq/Proof General в Emacs

Этот вопрос связан с настройкой режима Coq в Proof General в Emacs.

Я пытаюсь заставить Emacs автоматически заменять ключевые слова и обозначения в Coq соответствующими глифами Unicode.Мне удалось определить funкак строчную греческую лямбду λ, forallкак универсальный кванторный символ ∀ и т. д. У меня не было проблем с определением символов для слов.

Проблема в том, что когда я пытаюсь определить операторы =>, ->, <->и т. д. в их символ Unicode ⇒→↔ , они не заменяются соответствующими глифами Unicode в Coq. Однако они заменяются в буфере *scratch*, когда я их тестирую. Я использую тот же механизм для сопоставления глифов Unicode с нотацией Coq:

(defun define-glyph (string char-info)
  (font-lock-add-keywords
   nil
   `((,(format "\\<%s\\>" string)
      (0 (progn
       (compose-region
        (match-beginning 0) (match-end 0)
        ,(apply #'make-char char-info))
       nil))))
   ))

Я подозреваю, что проблема в том, что режим Coq помечает определенные знаки препинания как специальные, поэтому Emacs игнорирует мой код, чтобы заменить их глифами Unicode, но я Точно сказать не могу. Может кто-нибудь пролить свет на это для меня?