Unicode glyphs for keywords and operators in Coq/Proof General under Emacs

This question has to do with configuring the Coq mode within Proof General, in Emacs.

I'm trying to have Emacs automatically replace keywords and notation in Coq with the corresponding Unicode glyphs. I managed to define fun to be the Greek lowercase lambda λ, forall to be the universal quantifier symbol ∀, etc. I've had no problems defining symbols for words.

The problem is that when I try to define operators =>, ->, <->, etc. to their Unicode symbol ⇒→↔, they are not replaced with the corresponding Unicode glyphs in Coq. They are, however, replaced in the *scratch* buffer, when I test them. I'm using the same mechanism to match Unicode glyps with Coq notation:

(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))))
   ))

I suspect the problem is that Coq mode marks certain punctuation marks as special, so Emacs ignores my code to replace them with the Unicode glyphs, but I'm not sure. Can someone please shed some light on this for me?

Those operators are probably symbols, not words, according to the mode specific syntax table. Try

(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))))))