PG accepts garbage though Coq said "illegal begin of vernac"

[Matt McCutchen]

If I type the following complete garbage and press "C-c C-RET" at the end of the line, Proof General accepts it, even though I see in the *coq* buffer that Coq has said "illegal begin of vernac":

Check nat.&!&*\:,.:<*&^!)@)$.

I'm guessing that Proof General doesn't recognize the first period as a command separator and there's a miscommunication between Coq and Proof General regarding how much of the text was processed.

I'm using GNU Emacs 23.1.1 and Proof General 3.7.1, though I checked that the problem still exists in the latest Proof General from CVS.

[David Aspinall]

Many thanks for the report. Script management for Coq is still somewhat broken in current CVS, I'll try to have a look at this problem too when fixing it.