Custom Query (361 matches)

Filters
 
Or
 
  
 
Columns

Show under each result:


Results (61 - 63 of 361)

Ticket Resolution Summary Owner Reporter
#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.

#356 fixed Coq identifiers are unexpectedly colorized David Aspinall Erik Martin-Dorel
Description

I have just done a cvs update, and the Coq font lock seems to be broken: when an identifier contain a reserved tactic as a substring, such as ring_scope, simpl_pred or Section Predicates., it is wrongly colorized (viz. because of ring, simpl and red).

Kind regards, Erik Martin-Dorel.

#302 invalid Coq mode requires hilit19.el which is not in Emacs 23 David Aspinall Ilmari Vacklin
Description

On Ubuntu 9.10, the emacs23 package does not include hilit19.el, which the Coq mode requires. Downloading the file and placing it on load-path gives "Invalid font or font-spec".

Note: See TracQuery for help on using queries.