我正在使用 proof-general 来编写 Coq 证明。
当我C-c C-n在证明中使用时，我的光标移动到下一行，但当前行没有格式化。例如，如果我输入：
intros n. <C-c C-n>
我的光标移动到下一行，但intros n.仍然不缩进。所以我必须返回一行，走到行尾并点击<RET>自动缩进 coq 语句。此时，proof-general认为该语句已更改，我必须重新运行它。
理想情况下，我会C-c C-n自动缩进它正在运行的行，而不是转到下一行。
我怎样才能做到这一点？
我也在考虑advice-add@Clément 的建议，但实际上我相信 OP 的建议是修复错误而不是功能希望......：
当我们C-c C-n在添加换行符之前键入时RET，如果该行尚未正确缩进（如果该行不是在之前的行上键入之后RET编辑的，则可能会发生这种情况，这在实践中可能会发生），该C-c C-n动作被分心地删除......所以我们需要C-c C-n重新做一遍。
因此，我刚刚在https://github.com/ProofGeneral/PG/pull/604、@azani 和 @Clément 中打开了一个暂定 PR：如果您有时间，请随时在那里发表评论/评论。
您可以使用建议执行您所描述的操作：
(advice-add 'proof-assert-next-command-interactive :before
(lambda (&rest args) (indent-for-tab-command)))
......但我怀疑这是一个 AB 问题：C-c C-n不插入换行符，所以如果你正在写证明，你实际上RET每次按下 时大约会按下一次C-c C-n。如果在按之前按它C-c C-n，则该行将正确缩进。
intros更糟糕的是，如果您使用默认设置（电动缩进），通常不应该首先出现错误的缩进：导致intros需要缩进的父行也应该在创建其行时缩进.
如果我误解了，请使用导致您需要此功能的场景的具体示例更新 OP，我们可以查看 PG 中是否已经存在可能有所帮助的内容。