Nosub goals

[Matafou]

Coq team is considering (coq/coq#13656) changing all messages containing "subgoal[s]" into "goal[s]". This PR should makes PG compatible with this.
Making this change as early as possible so that as much users as possible have a compatible PG when this lands on coq master (if it does, since this change is still discussed).

[Matafou]

Will merge after rebasing this correctly.

[Matafou]

@erik @cpitclaudel
For the record if this happens again: test step_wise.el #081_coq-test-regression-show-proof-diffs had failed but succeeded when rerun. My (weak) guess is a timing problem: this test does a proof-shell-wait and then tests the content of coq-response a bit too fast while it was not yet filled, so it ended up checking that the empty string was equal to some pattern (this I could confirm in the log).

[hendriktews]

For the record if this happens again: test step_wise.el #081_coq-test-regression-show-proof-diffs had failed but succeeded when rerun.

See #538. Please download the log from the failed testrun and attach the relevant part to #538, because after rerun the logs of the failed test are not accessible any more.

[Matafou]

Sorry I don't have the log of the failed testrun. All I can say is that the message said that "" did not match the regexp. Which suggests that when the coq-response buffer was read it was not yet filled with the coq output. But since this output needs to be processed to interpret xml for background coloring, this may explain a small delay?

[hendriktews]

Sure. I should have written "next time please consider to download the log and ...". The log that I attached last there hat the same test failing with the same empty string.