Indentation issue: "by"

[RalfJung]

The following code:

Proof using Fcontr.
  induction k as [|k IH]; simpl.
  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
    apply (contractive_0 map).
  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
    by apply (contractive_S map).
Qed.

gets auto-indented (select it, and hit "Tab") to

Proof using Fcontr.
  induction k as [|k IH]; simpl.
  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
    apply (contractive_0 map).
  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
      by apply (contractive_S map).
Qed.

Notice how the line starting with "by" got indented, for no apparent reason.

[cpitclaudel]

for no apparent reason.

The reason is that rewrite xyz by tactic (without the dot) is also valid, and that could reasonably be considered to need indentation. (I can't comment on how easy it would be to fix the issue)

[RalfJung]

The reason is that rewrite xyz by tactic (without the dot) is also valid, and that could reasonably be considered to need indentation.

I don't understand why by would be special here. IMO indentation (by exactly 2 spaces) should happen whenever this is a continuation of the tactic on the previous line, i.e. whenever the previous line does not end in a .. rewrite X by Y is not special here, e.g. the same should happen in

rewrite X Y Z
  Q.

(imagine those being long lemma names)

[proux01]

I've added the following line to my .emacs to "fix" that issue

 '(coq-smie-user-tokens (quote (("by" . "now"))))

[Matafou]

The reason is that rewrite xyz by tactic (without the dot) is also valid, and that could reasonably be considered to need indentation.

I don't understand why by would be special here. IMO indentation (by exactly 2 spaces) should happen whenever this is a continuation of the tactic on the previous line, i.e. whenever the previous line does not end in a .. rewrite X by Y is not special here, e.g. the same should happen in

rewrite X Y Z
  Q.

(imagine those being long lemma names)

Coming back to this remark. Actually it would get indented like this(1) (both with current engine and the new one):

rewrite X Y Z
        B Q.

Whereas if "by" is known as a (infix) keyword then we have:

rewrite X Y Z
  by Q.

(1) for technical reason it is still the same in the new indentation engine.