The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

If I remember well, comments can also be nested. Ie. if you write "(* foo (* bar *) baz *)", all that will count for a single comment. The "baz *)" part is considered to be commented. This behavior is the same as Ocaml one, but different from C programming language.

2014-04-11 14:49 GMT+02:00 Guillaume Melquiond <guillaume.melquiond AT inria.fr>:

On 11/04/2014 14:32, bhandalc AT tcd.ie wrote:

I noticed a bug in the CoqIDE commenting. If you begin quotations within a
comment that are not closed then the comment fails to close.

This is not a bug; this is on purpose. ``*)'' is not recognized inside quoted strings, even if such a string happens in a comment. That way, if one puts a well-formed Coq script in a comment, then one gets a well-formed (empty) script, even if there are strings in it.

Best regards,

Guillaume

--
.../Sedrikov\...