Custom Query (361 matches)
Results (7 - 9 of 361)
Ticket | Resolution | Summary | Owner | Reporter |
---|---|---|---|---|
#296 | fixed | PG accepts garbage though Coq said "illegal begin of vernac" | ||
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. |
|||
#386 | fixed | Coq goals counter not reset on backtracking out of proof | ||
Description |
Test case with |
|||
#394 | fixed | Coq "Library" keyword - incorrect coloring | ||
Description |
When using "Extraction Library <Module>", the "Library" word is not highlighted in blue like all other keywords (Extraction, Require, etc). |