How do I turn off the aggressive auto-indent in Proof General/Coq

I have installed Proof General via Doom Emacs' coq module, keeping most settings as whatever default that module sets. Sometimes the automatic indentation this provides gives results I dislike, and furthermore does so aggressively – even if I fix the indentation manually, Proof General is quick to revert it to automatic indentation. A particularly bad case is records: which look like this:

Record foo : Type := mkFoo {
bar : nat;
}.


I would prefer:

Record foo : Type := mkFoo {
bar : nat;
}.


Other problems include it not understanding extensions like Equations, again aggressively breaking any manual indentation.

Relevant-looking variables (ones containing substrings coq and indent) have the following values:

coq-indent-box-style             nil
coq-indent-basic                 2
coq-match-indent                 2
coq-script-indent                t
coq-indent-proofstart            2
coq-indent-modulestart           2
coq-indent-semicolon-tactical    2
coq-smie-after-bolp-indentation  2


Though I'm genuinely looking for an answer, I'm also curious as to whether this is considered on-topic. I think we should expect more gritty tooling questions, and also other acute issues (“What does this error message mean?”, “How can I make this code check?”) when we open up to the public (unless such questions are explicitly banned). An argument against these questions is that one could ask coq.zulipchat.com or wherever instead.

• I think this is on topic, but should be decorated with some specific tag like “IDE”, “editors”, or whatnot. Although there is also emacs.stackexchange.com... who knows. Nevertheless it is really an issue that could disturbing your work. This is even more relevant in the case of isabelle, since everything is done in the bundled IDE by default. Feb 17 at 0:15
• @PedroSánchezTerraf but in the case of Isabelle the IDE is basically what is shipped. Coq does not come with Doomemacs, so it is probably better suited over there. The question is quite Emacs specific and I would expect a better answer there. Feb 17 at 7:10
• I asked the Doom Emacs people, and they seemed to believe that the relevant settings would be in Proof General, and that the fix would be the same as in basic Emacs except for which file to put the relevant lines of elisp code in. Doom's coq module essentially does 3 things to Proof General: package management, setting indent sizes to the global indent size setting (hence the value 2 in most of the variables I could find), and setting some vi-like key bindings. All of these are overridable. Feb 17 at 8:12
• This is definitely on-topic because this is a question about a mode for a proof assistant. It would be ridiculous to make a distinction between IDEs that are shipped with the software and IDEs that are provided by the community. Feb 17 at 17:20

This also annoys me to no end. I have found a partial fix by adding the following to my user-config (I'm using spacemacs, but I assume it's the same):
(eval-after-load "proof-script"