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".
Ltac2
of_goal () :=
of_ids (
List.map (
fun (
id,
_,
_) =>
id) (
Control.hyps ())).
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.