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.

Change History (0)

Note: See TracTickets for help on using tickets.