The Coq mailing list

[Jesper Bengtson <jebe AT itu.dk>]

> AFAIK, you cannot convert a string of the String coq library to a
> string used by tactics, but you can provide a (tactic) string to the
> tactic, so that it is used to generate identifiers.

> Ltac demo s :=
> let H := fresh s in
> intros H.
> 
> Goal forall (t u v:bool), True.
> intro.
> demo u.
> demo t.
> split.
> Qed.
> <<<

Yes, I knew this was possible. What I would want, however, is to be able to 
write 'demo "u"' instead, seeing as both 'fresh u' and 'fresh "u"' work.

From the replies I have gotten it seems that I'd have to go into the ML-level 
to achieve this though.

Thank you for your time. It's all a bit clearer now :)

/Jesper