Printing of the sequence operator `;;`
The first Coq example that comes with the Iris lecture notes shows how to prove a lemma with the following proof goal:
{{{ ℓ ↦ #n }}} (incr ℓ) ||| (incr ℓ) ;; !#ℓ {{{m, RET #m; ⌜n ≤ m⌝ }}}
However, in the interactive proof mode, the goal is displayed as
{{{ ℓ ↦ #n }}} (Lam <> ! #ℓ) (incr ℓ ||| incr ℓ) {{{ (m : Z), RET #m; ⌜n ≤ m⌝}}}
I.e. Coq automatically desugars the ;;
notation.