coq-insert-suggested-dependency sometimes inserts unparsable statements

[HazardousPeach]

When a proof uses a Proof with clause, and has multiple section dependencies, running the coq-insert-suggested-dependency command inserts invalid, unparsable code into the proof file.

Reproducing

Here's a simple example:

Section A.
Hypothesis H1: nat -> nat.
Hypothesis H2: nat -> nat.

Theorem T: nat.
Proof with auto.
  apply H1.
  apply H2.
  exact 0.
Qed.

If you run to the end of these commands in proof general, and then run the coq-insert-suggested-dependency command, it'll replace the Proof with auto. line with Proof using H1 H2 with auto.. However, this will immediately be flagged by flycheck, and backtracking over the proof and attempting to run this command results in the error message Error: Syntax error: '.' expected after [vernac:command] (in [vernac_aux])..

Likely Cause

PG uses suggestions from Coq about what Proof using line to insert, by setting the Suggest Proof Using. flag. In this example with this flag, after Qed, Coq will print:

The proof of T should start with one of the following command:
Proof using H1 H2.
Proof using All.
Proof using Type*.

These suggestions parse on their own, but they don't include the with auto part of the Proof command. In attempting to combine Proof using H1 H2. with Proof using auto., proof general produces Proof using H1 H2 with auto., which does not parse.

Possible Fix

You can surround the dependencies with parenthesis to fix the parse error. In this example case, you can use Proof using (H1 H2) with auto.. For tactics other than auto, flipping the order of the clauses also fixes the issue (e.g. Proof with simpl using H1 H2.). However, this doesn't work directly with auto because the auto tactic has it's own interpretation of the using clause. Surrounding auto with parenthesis allows this to work too (Proof with (auto) using H1 H2.), but the former solution looks nicer to me.