Custom Query (361 matches)

Filters
 
Or
 
  
 
Columns

Show under each result:


Results (7 - 9 of 361)

1 2 3 4 5 6 7 8 9 10 11 12 13
Ticket Resolution Summary Owner Reporter
#296 fixed PG accepts garbage though Coq said "illegal begin of vernac" courtieu Matt McCutchen
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 courtieu David Aspinall
Description

Test case with example.v: process to split, then retract open proof by C-c C-RET to Goal. Modeline indicator still shows 2 open goals.

#394 fixed Coq "Library" keyword - incorrect coloring courtieu coqletsgo
Description

When using "Extraction Library <Module>", the "Library" word is not highlighted in blue like all other keywords (Extraction, Require, etc).

1 2 3 4 5 6 7 8 9 10 11 12 13
Note: See TracQuery for help on using queries.