The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Thu, Apr 02, 2009 at 04:53:40PM +0200, Guillaume Melquiond wrote:
> 
>         Require Import String.
>         (* Definition my_string := "*)"%string. *)
>         Definition my_string := "let's try something else"%string.

Perhaps (* and *) should not be allowed in string literals.
You would have to write

Definition my_string := "*" ++ ")"%string.

instead (or whatever string append looks like in coq). Or in Haskell,
you could write it as, for example, "*\&)" or "\42)"; I don't know if
coq has a similar syntax.


Thanks
Ian