In alectryon.el
, going from reST mode to Coq mode (or saving a file while opened in reST mode) does not handle tab characters that appear in coq
blocks. Instead Alectryon seems to begin a new prose block.
Sample input (in reST mode). Note that auto
here is indented with a hard tab character.
.. coq::
Goal True.
Proof.
auto.
Qed.
Sample output from saving or switching to Coq mode:
Goal True.
Proof.
(*|
auto.
Qed.
|*)
Output obtained if the tab is replaced with spaces:
Goal True.
Proof.
auto.
Qed.