Fresh

Ltac2.Fresh

module Free : sig ... end

val fresh : Free.t -> ident -> ident

fresh free id generates a fresh identifier with the given base name which is not a member of free.

val next : Free.t -> ident -> ident * Free.t

next free id generates a fresh identifier with the given base name which is not a member of free, and returns the updated set. More efficient than composing fresh and Free.add.