Coq: нотация не напечатана

Question

Я определил индуктивный тип, минимальный пример ниже. Я хотел бы использовать обозначения, такие как ~ или =. Синтаксис распознается, но не печатается в целях верхней правой панели.

Пример:

Inductive num : Set :=
  | O : num
  | S : num -> num.

Theorem test (n : num) : ~ (S n) = O.

Панель говорит:

1 subgoal
n : num
______________________________________(1/1)
not (@eq num (S n) O)

Пока ожидаю

1 subgoal
n : num
______________________________________(1/1)
~ (S n) = O

Я попытался переопределить = как это без успеха:

Notation "x = y" := (@eq num x y) (at level 70).

Или определите новый символ, но безуспешно:

Notation "x =n y" := (@eq num x y) (at level 50).
Theorem test (n : num) : ~ (S n) =n O.

Это проблема с настройками? Я использую CoqIde 8.7.2 на Mac.