Opened 13 years ago

Closed 13 years ago

#412 closed defect (fixed)

coq parsing broken since Jun 04 20:12:40 (II)

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

Description

Here is another piece of Coq code that doesn't parse anymore: 

Record a : Type := make_a { aa : nat }.

Change History (1)

comment:1 Changed 13 years ago by courtieu

Resolution: → fixed
Status: new → closed

I removed { and } as command terminators. This should be fixed in cvs.

Note: See TracTickets for help on using tickets.