Opened 13 years ago

Closed 13 years ago

#410 closed defect (fixed)

coq parsing broken since Jun 04 20:12:40

Reported by: coquser Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.1
Component: 2:pg-emacs Keywords:
Cc:

Description (last modified by David Aspinall)

Hi,

the commit ​http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/rev/d3cf65e2d4e4 brakes parsing in Coq. Try 

Require Export Coq.Lists.List.
Notation "[ ]" := nil : list_scope.
Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.

Bye,

Hendrik

Change History (2)

comment:1 Changed 13 years ago by David Aspinall

Description: modified (diff)
Status: new → accepted

comment:2 Changed 13 years ago by courtieu

Resolution: → fixed
Status: accepted → closed

Fixed in cvs, thanks.

Note: See TracTickets for help on using tickets.