Notation in the where part of an Inductive command is not prettified.

[Lysxia]

The following snippet

Reserved Notation " t '-->' t' " (at level 40).

Inductive step : nat -> nat -> Prop :=
  where " t '-->' t' " := (step t t').

renders as follows

The last --> is not prettified!

[cpitclaudel]

Snap! Good catch.
The place to fix would be this snippet:

(defun company-coq-features/prettify-symbols--predicate-1 (pos)
  "Check if POS should be prettified."
  (save-excursion
    (goto-char pos)
    (let ((pp (syntax-ppss)))
      (or (company-coq--in-code-p-1 pp)
          (company-coq--in-notation-string-1 pp)
          ;; Add something here
          ))))