The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le jeudi 02 avril 2009 à 08:36 -0400, Chris Casinghino a écrit :
> I know it is partially documented [1], but are the coq developers
> aware that this "feature" can be exploited in this way?  All joking
> aside, it seems deceptive that this file compiles.

While this syntax can be abused, I believe it is necessary. Consider the
following script:

        Require Import String.
        Definition my_string := "*)"%string.

How would you comment it out, if comments were allowed to stop right in
the middle of a lexical entity?

Best regards,

Guillaume