Misparsed tactic leads to two commands being exeucted at once

[RalfJung]

To reproduce, consider:

Lemma L (P Q R: Prop) :
  (P -> Q -> R) -> P -> Q -> R.
Proof.
  intros Himpl HP HQ. (* Process proof until here *)
  speciaalize (Himpl HP HQ) as Goo.

Qed.

Now hit Alt-down. I would expect vscoq to try to process the next tactic, which has a typo in it and therefore doesn't parse. However, processing actually skips all the way to after the Qed and I get two errors:

That is quite confusing. Worse, the Coq proof state window only shows the second error, making the actual underlying cause of the problem invisible:

I can see it thanks to the error-lens addon, but if one does not have that installed, one has to notice the error in the "problems" panel.

The fact that according to the last screenshot, L got declared is concerning, since there can't even have been a complete proof.

This is with Coq 8.18.0.

[rtetley]

This is a duplicate of #877. I am busy working on a fix ! I will keep open because of the L is declared thing. This is probably related to the separation of interp and synterp phases.