The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 8 Sep 2011 14:27:31 +0200,
Jesper Bengtson 
<jebe AT itu.dk>
 a écrit :

> Greetings Coq users.
> 
> I am trying to generate fresh names in the context from strings
> provided by the user.
> 
> If i type the command 'fresh t', where t is a variable of type
> string, I get an error message that t cannot be coerced to a fresh
> identifier. Is there a way forward here, or should I just choose a
> name at random?
> 
> Best regards
> 
> /Jesper

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.
<<<