Module `Evd.MiniEConstr`

Use this module only to bootstrap EConstr

module ESorts : sig ... end

module EInstance : sig ... end

type t = econstr

val kind : evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
val kind_upto : evar_map -> Constr.constr -> (Constr.constr, Constr.types, Sorts.t, UVars.Instance.t) Constr.kind_of_term
val whd_evar : evar_map -> t -> t
val mkLEvar : evar_map -> (Evar.t * t list) -> t
val replace_vars : evar_map -> (Names.Id.t * t) list -> t -> t
val of_kind : (t, t, ESorts.t, EInstance.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 : (t, Constr.t) Util.eq
val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt
val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
val of_case_invert : Constr.constr Constr.pcase_invert -> econstr Constr.pcase_invert
val unsafe_to_case_invert : econstr Constr.pcase_invert -> Constr.constr Constr.pcase_invert
val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt
val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
val of_named_context : (Constr.t, Constr.types) Context.Named.pt -> (t, t) Context.Named.pt
val of_rel_context : (Constr.t, Constr.types) Context.Rel.pt -> (t, t) Context.Rel.pt