Ltac2 @
external union :
t ->
t ->
t := "ltac2" "fresh_free_union".
Ltac2 @
external of_ids :
ident list ->
t := "ltac2" "fresh_free_of_ids".
Ltac2 @
external of_constr :
constr ->
t := "ltac2" "fresh_free_of_constr".
End Free.
Ltac2 @
external fresh :
Free.t ->
ident ->
ident := "ltac2" "fresh_fresh".
Generate a fresh identifier with the given base name which is not a
member of the provided set of free variables.