Free

Ltac2.Fresh.Free

type t

Type of sets of free variables.

val empty : t

Empty set of free variables.

val add : ident -> t -> t

add id s adds the given identifier to the set of free variables s.

val union : t -> t -> t

union s1 s2 merges the two sets of free variables.

val of_ids : ident list -> t

of_ids ids creates a set of free variables from the given list of identifiers.

val of_constr : Evd.evar_map -> constr -> t

of_constr sigma t collects all free variables of t as a set.