Module Unification.Meta

Metas

type t
type instance_typing_status =
| CoerceToType
| TypeNotProcessed
| TypeProcessed
val empty : t
val meta_opt_fvalue : t -> Constr.metavariable -> Evd.econstr freelisted option
val meta_name : t -> Constr.metavariable -> Names.Name.t
val meta_declare : Constr.metavariable -> Evd.etypes -> ?name:Names.Name.t -> t -> t
val meta_instance : t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
val meta_merge : t -> t -> t

meta_merge evd1 evd2 returns evd2 extended with the metas of evd1

val map_metas : (Evd.econstr -> Evd.econstr) -> t -> t
val evar_source_of_meta : Constr.metavariable -> t -> Evar_kinds.t Loc.located
val fold : (Constr.metavariable -> 'a -> 'a) -> t -> 'a -> 'a
val pr_metaset : Metaset.t -> Pp.t
val pr_metamap : Environ.env -> Evd.evar_map -> t -> Pp.t