`Constr`#

Ltac2.Constr

type t = constr

val type_ : Environ.env -> Evd.evar_map -> t -> Evd.evar_map * t

type_ env sigma t returns the type of t in the given environment and evar map, along with the updated evar map.

val equal : Evd.evar_map -> t -> t -> bool

equal sigma t1 t2 performs a strict syntactic comparison between t1 and t2, only up to α-conversion and evar expansion.

module Binder : sig ... end

module Relevance : sig ... end

module Unsafe : sig ... end

Low-level access to kernel terms. Use with care!

module Cast : sig ... end

module Pretype : sig ... end

val has_evar : Evd.evar_map -> t -> bool

has_evar sigma t returns true if t contains an evar.

Constr#