The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

reaz wrote:
> Can any one tell me how to print an arbitrary string in coq-8.1.pl3?
>
> Thanks.
> --Reaz
>   
What do you mean by "printing"?  At what time do you want to print 
something?  Or do you just want to write a program that returns a string 
and evaluate this program to see its result?

For the latter just use "Eval compute".  Here is an example:

Require Import String.
Open Scope string_scope.
Eval compute in ("Hello " ++ "world!").


If you want side effects to occur in the middle of goal-directed proofs, 
you can also ask fail and idtac to display a message that you gave them 
as argument.  This is explained in the documentation for these tactics 
(pp. 197-198 in the pdf version of the reference manual).

Yves