Opened 14 years ago

Closed 14 years ago

#356 closed defect (fixed)

Coq identifiers are unexpectedly colorized

Reported by: Erik Martin-Dorel Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-4.0
Component: 7:prover-coq Keywords:
Cc: 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.

Change History (3)

comment:1 Changed 14 years ago by courtieu

Resolution: → fixed
Status: new → closed

This should be fixed in cvs now. Thanks a lot for reporting.

comment:2 Changed 14 years ago by Erik Martin-Dorel

Resolution: fixed
Status: closed → reopened

Thanks for the fix.

But I reopen the ticket since it seems to me there is still a similar issue about "complex identifiers" when they contain Prop, Set or Type, as in Section SubType., though this residual bug was certainly present for a while.

comment:3 Changed 14 years ago by courtieu

Resolution: → fixed
Status: reopened → closed

Hello,

Thanks! This is (re)fixed in cvs. I hope there are no other problem of this kind now. Regards, Pierre

Note: See TracTickets for help on using tickets.