Proof General: script management confused, couldn't find goal span for save. when evaluating past the bottom of a module that contains a theorem with the same name as the module

[coquser]

Here is a proof script that gives "Proof General: script management confused, couldn't find goal span for save." in PG 4.3pre131011 with Coq 8.4pl3 (December 2013):

Module match_beta.
  Theorem match_beta : True.
  Proof.
    exact I.
  Defined.
End match_beta.

Module foo.

[coquser]

Can you still reproduce this? I can't in the latest CVS. --cpitcla

[courtieu]

I can. It probably comes from the lemma and the Module having the same name.

[courtieu]

Actually it came from the hacks for discriminating goal commands from others. the presence of "match" was checked (and counted compared to "with") and wrongly detected here despite the "_". Fixed.