Module Evd.MiniEConstr

Use this module only to bootstrap EConstr

module ESorts : sig ... end
module EInstance : sig ... end
type t = econstr
val whd_evar : evar_map -> t -> t
val of_kind : (ttESorts.tEInstance.t) Constr.kind_of_term -> t
val of_constr : Constr.t -> t
val of_constr_array : Constr.t array -> t array
val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
val to_constr_opt : evar_map -> t -> Constr.t option
val unsafe_to_constr : t -> Constr.t
val unsafe_to_constr_array : t array -> Constr.t array
val unsafe_eq : (tConstr.t) Util.eq
val of_named_context : (Constr.tConstr.types) Context.Named.pt -> (tt) Context.Named.pt
val of_rel_context : (Constr.tConstr.types) Context.Rel.pt -> (tt) Context.Rel.pt