Disable long indention under quantifiers?

[coquser]

At some point (I think related to emacs 24) Proof General changed its way for indenting lines under quantifiers. E.g.

Lemma foo_bar_baz : forall x y z,

x = y -> y = z -> x = z.

Is there a way to revert to the previous 2-space indent from the indent at the beginning of the line?

[coquser]

The following patch does what you want. It's for Pierre to decide whether this should be applied to trunk or not :)

--- coq-smie.el.~11.21.~	2015-04-21 17:55:18.203475436 -0400
+++ coq-smie.el	2015-04-27 13:12:10.283113723 -0400
@@ -927,7 +927,7 @@
        ((and (member token '("forall" "quantif exists"))
 	     (not coq-indent-box-style)
 	     (not (smie-rule-bolp)))
-	(smie-rule-parent 2))
+	(smie-rule-parent 0))
 
        ;; trying to indent "{" at the end of line for records, but the
        ;; parent is not what I think.

[courtieu]

Hi,

The idea (from smie) of the 4 space characters is the following:

Lemma foo_bar_baz : forall x y z,

x = y -> y = z -> x = z.

indents the last line at the same column than in :

Lemma foo_bar_baz :

forall x y z,

x = y -> y = z -> x = z.

I will try to have an option for that.

[courtieu]

done.