Opened 17 years ago

Closed 17 years ago

Last modified 17 years ago

#116 closed defect (fixed)

Coq syntax highlighting: identifiers starting with "fun" are wrongly coloured

Reported by: Robin Green Owned by: David Aspinall
Priority: trivial Milestone: PG-Emacs-3.7
Component: 2:pg-emacs Keywords:
Cc:

Description (last modified by David Aspinall)

In my Coq file, identifiers beginning with "fun" have the "fun" in black and the rest of the identifier coloured.

Emacs: GNU Emacs 22.0.95.1 (x86_64-redhat-linux-gnu, GTK+ Version 2.10.9)

of 2007-03-06 on hs20-bc1-5.build.redhat.com

Proof General Version 3.7pre070511.

Change History (2)

comment:1 Changed 17 years ago by David Aspinall

Resolution: → fixed
Status: new → closed

Here's a test case: 

forall (funA B: Prop)     (* funA should be all magenta *)
fun (forallA B: Prop)     (* forallA should be all magenta *)

This has been fixed in CVS head now. Thanks for the report.

comment:2 Changed 17 years ago by David Aspinall

Description: modified (diff)
Note: See TracTickets for help on using tickets.