Indentation issue: intros with `?`

[joonwonc]

The code below

Goal forall a b: nat, True.
Proof.
  intros a ?;
    trivial.
Qed.

is auto-indented to

Goal forall a b: nat, True.
Proof.
  intros a ?;
         trivial.
Qed.

If not using ? at the end of intros, PG auto-indents it correctly, like

Goal forall a b: nat, True.
Proof.
  intros a b;
    trivial.
Qed.

[Matafou]

Hi, thanks for reporting this. Note that if you split "?;" into "? ;" it works. PG does not detect that "?;" is not one token but two. By default sequences of "non letters nor digits" are considered as one token.

I could try to detect this but I don't know if this is worth the effort.

[joonwonc]

Thanks for letting me know! I indeed have been using "? ;" as a workaround.