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.
Note: See
TracTickets for help on using
tickets.