manual proof mode should never result in a state where "There are no more subgoals" but Qed claims there are remaining open goals

[JasonGross]

The only way to fix this seems to be reloading the document, which makes working on slow files incredibly painful.

[rtetley]

I think this could somewhat be linked to #1048. It seems there is some sort of race condition in the parsing of the file which ends up having an incorrect internal state.