Iris context line break incorrectly formatted

[rongcuid]

See also: https://gitlab.mpi-sws.org/iris/iris/-/issues/581

With Iris, the context output is incorrectly formatted.

Lemma asm (P : iProp Σ) : P ⊢ P.
Proof.
  (**
    To enter the Iris Proof Mode, we can use the tactic [iStartProof].
    However, most Iris tactics will automatically start the Iris Proof
    Mode for you, so we can directly introduce [P].
  *)
  iIntros "H".
  (**
    This adds [P] to the spatial context with the identifier ["H"]. To
    finish the proof, one would normally use either [exact] or [apply].
    So in Iris, we use either [iExact] or [iApply].
  *)
  iApply "H".
Qed.

Output:

The separator --- should be on its own line.

[rongcuid]

coqtop seems to be generating the correct output:

asm <   iIntros "H".
1 goal

  Σ : gFunctors
  P : iProp Σ
  ============================
  "H" : P
  --------------------------------------∗
  P

This makes Iris very hard to use

Maybe related to #852.

[gares]

Looks loke a bug, thanks for reporting