Module EConstr.Expand

type t

A variant of EConstr.t where evar substitution is performed on the fly. The handle type below is a kind of substitution that is needed to make sense of the delayed term. Such representation is more efficient than EConstr.t when iterating over a whole term.

Caveat: the kind function below only returns the expanded head of the term. This means that when it returns Evar (evk, inst), evk is guaranteed to be undefined in the evar map but inst is, in general, not the same as you would get after expansion. You must call expand_instance before performing any operation on it.

type handle
val make : Evd.econstr -> handle * t
val repr : Evd.evar_map -> handle -> t -> Evd.econstr
val liftn_handle : int -> handle -> handle
val kind : Evd.evar_map -> handle -> t -> handle * kind
val expand_instance : skip:bool -> Evd.undefined Evd.evar_info -> handle -> t SList.t -> t SList.t
val iter : Evd.evar_map -> (handle -> t -> unit) -> handle -> kind -> unit
val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> handle -> t -> unit) -> 'a -> handle -> kind -> unit