package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/coq-core.tactics/EClause/index.html
Module EClauseSource
Evar-based clauses
The following code is an adaptation of the Clenv.make_clenv_* functions, except that it uses evars instead of metas, and naturally fits in the new refinement monad. It should eventually replace all uses of the aforementioned functions.
A clause is constructed as follows: assume a type t := forall (x1 : A1) ... (xn : An), T, we instantiate all the xi with a fresh evar ei and return T(xi := ei) together with the ei enriched with a bit of additional data. This is the simple part done by make_evar_clause.
The problem lies in the fact we want to solve such holes with some constr bindings. This entails some subtleties, because the provided terms may only be well-typed up to a coercion, which we can only infer if we have enough typing information. The meta machinery could insert coercions through tricky instantiation delays. The only solution we have now is to delay the tentative resolution of clauses by providing the solve_evar_clause function, to be called at a smart enough time.
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.
*)
}val make_evar_clause :
Environ.env ->
Evd.evar_map ->
?len:int ->
EConstr.types ->
Evd.evar_map * clauseAn 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_mapsolve_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 _.