Module EClause

Evar-based clauses
type hole = {
hole_evar : EConstr.constr;

The hole itself. Guaranteed to be an evar.

hole_type : EConstr.types;

Type of the hole in the current environment.

hole_deps : bool;

Whether the remainder of the clause was dependent in the hole. Note that because let binders are substituted, it does not mean that it actually appears somewhere in the returned clause.

hole_name : Names.Name.t;

Name of the hole coming from its binder.

}
type clause = {
cl_holes : hole list;
cl_concl : EConstr.types;
}
val make_evar_clause : Environ.env -> Evd.evar_map -> ?⁠len:int -> EConstr.types -> Evd.evar_map * clause

An evar version of make_clenv_binding. Given a type t, evar_environments env sigma ~len t bl tries to eliminate at most len products of the type t by filling it with evars. It returns the resulting type together with the list of holes generated. Assumes that t is well-typed in the environment.

val solve_evar_clause : Environ.env -> Evd.evar_map -> bool -> clause -> EConstr.constr Tactypes.bindings -> Evd.evar_map

solve_evar_clause env sigma hyps cl bl tries to solve the holes contained in cl according to the bl argument. Assumes that bl are well-typed in the environment. The boolean hyps is a compatibility flag that allows to consider arguments to be dependent only when they appear in hypotheses and not in the conclusion. This boolean is only used when bl is of the form ImplicitBindings _.

val check_bindings : 'a Tactypes.explicit_bindings -> unit
val explain_no_such_bound_variable : Names.Id.t list -> Names.Id.t CAst.t -> 'a
val error_not_right_number_missing_arguments : int -> 'a