Opened 9 years ago

#507 new defect

PG for Coq does not interpret quotes within comments like Coq does

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

Description

In a file containing e.g.:

(* " *) Definition z := 0. (* " *)

Proof General evaluates the command, while Coq considers the file to contains only a comment (because quotes are supposed to be paired when in comments).

Conversely, a file containing

(* " *) Definition z := 0.

will be processed without errors by PG for Coq, but coqc will fail with Unterminated string.

Observed with 4.3pre130111.tgz, not seen as an already reported bug, but not tested with more recent versions.

Change History (0)

Note: See TracTickets for help on using tickets.