Hello! Would there be a way to make the display of the coqtop instruction a bit better in these examples ? The code I used is
.. example:: Dynamic nature of mutable cells .. coqtop:: all Ltac2 mutable x := true. Ltac2 y := x. Ltac2 Eval y. Ltac2 Set x := false. Ltac2 Eval y.
and the non
Eval lines produce empty lines that do not look good...
@Kenji Maillard A bug was recently introduced in a PR attempting to improve the output. Cf. https://github.com/coq/coq/pull/12272#issuecomment-626387244. This should hopefully be solved soon, and in any case before the release.
putting a double line as you indicate in the issue helps a bit, but it still displays the empty lines: nothing we can do about them ?
Please comment in the issue so that the other people involved are aware.
Last updated: Feb 05 2023 at 23:30 UTC