Opened 14 years ago

Closed 14 years ago

#348 closed defect (fixed)

Need to update in coq-syntax.el the keywords containing the word Local

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

The Coq keywords that contain the word Local should be updated in coq/coq-syntax.el:

More precisely, the keywords "Open Local Scope", "Close Local Scope" and "Notation Local" should be replaced with: "Local Open Scope", "Local Close Scope" and "Local Notation", since Coq complains if we process the former keywords which are currently defined in coq-syntax.el: 

Warning: Obsolete syntax: use "Local" as a prefix.

I use GNU-Emacs-23.2.1 and Coq-8.2pl2.

Kind regards, Erik Martin-Dorel.

Change History (1)

comment:1 Changed 14 years ago by David Aspinall

Resolution: → fixed
Status: new → closed

Fixed, many thanks. I also tweaked the abbrevs to match, hopefully won't annoy too many legions of power users.

Please feel free (i.e. encouraged!) to upload patches for fixes such as these.

Note: See TracTickets for help on using tickets.