Closing a {…} badly jams the prover.

[adud]

Consider the following erroneous code:

Goal True /\ True.
  split.
  2:{  tauto.}
  tauto.
Qed.

There should be a space between tauto. and }, but instead of returning an error ProofGeneral gets stuck.

[Matafou]

Yes. It is a known bug however since The user can interrupt Coq and fix the missing space it is an acceptable behavior imho, although not perfect.