Newly-merged support for 8.5 often hangs

[pqwy]

Broadly, coquille causes vim to hang near the middle or towards the end of files in Software Foundations.

Repro:

• Unpack the sources.
• coqc Basics.v
• vim Induction.v
• Go to line 475 (beginning of plus_assoc'', the last theorem in the file).
• :CoqToCursor; should run Coq over everything up to the theorem.
• :CoqNext. At this point vim gets stuck.

Using Coq 8.5pl3 on OCaml 4.03.0. Happens both with vim (8.0) and neovim (0.1.7).

I'll see if I can dig out more details, but this repro seems reliable.

[trefis]

I fixed the hanging problem.
But I think, though I might be wrong, that the current implementation of the protocol is broken in the sense that it doesn't seem to handle at all the asynchronous messages from Coq.
i.e. it might be marking proof as checked while they haven't been processed by Coq yet, and then will ignore the messages confirming whether the proof is correct or not.

This is just speculation, I haven't read the code carefuly.