Opened 15 years ago
Last modified 12 years ago
#296 closed defect
PG accepts garbage though Coq said "illegal begin of vernac" — at Initial Version
Reported by: | Matt McCutchen | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-4.2 |
Component: | 2:pg-emacs | Keywords: | |
Cc: | greenrd@… |
Description
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.
Note: See
TracTickets for help on using
tickets.