Skip to content

[HOWTO] Disable +default--newline-indent-and-continue-comments-a in Coq mode #2081

@Ptival

Description

@Ptival

What I want to achieve
+default--newline-indent-and-continue-comments-a is infuriating in Coq mode. Coq comments are not line comments, and I really doubt anyone writes comments like those:

(** Start of a sentence *)
(** that continues on *)
(** other lines. *)

Instead, this is enough:

(** Start of a sentence
    that continues on
    other lines. *)

and allows itself better to things like g q...

I don't know how to disable this feature, either globally, or simply in Coq mode.

Alternatively, is there a way to force a newline character? Sadly, the Ctrl V trick inserts ^M.

Metadata

Metadata

Assignees

No one assigned

    Labels

    is:featureAdds or requests new features, or extends existing onesmodule:config/defaultPertains to Doom's :config default modulemodule:lang/coqPertains to Doom's :lang coq module

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions