MiniEConstr (coq-core.Evd.MiniEConstr)

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, Univ.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