package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/coq-core.interp/Impargs/index.html
Module ImpargsSource
Implicit Arguments
Here we store the implicit arguments. Notice that we are outside the kernel, which knows nothing about implicit arguments.
...
An implicits_list is a list of positions telling which arguments of a reference can be automatically inferred
type implicit_explanation = | DepRigid of argument_position(*means that the implicit argument can be found by unification along a rigid path (we do not print the arguments of this kind if there is enough arguments to infer them)
*)| DepFlex of argument_position(*means that the implicit argument can be found by unification along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind)
*)| DepFlexAndRigid of argument_position * argument_position(*means that the least argument from which the implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application)
*)| Manual(*means the argument has been explicitly set as implicit.
*)
We remember various information about why an argument is inferable as implicit
We also consider arguments inferable from the conclusion but it is operational only if conclusion_matters is true.
true = maximal contextual insertion
true = always infer, never turn into evar/subgoal
type implicit_status =
(implicit_position
* implicit_explanation
* (maximal_insertion * force_inference))
optionNone = Not implicit
val compute_implicits_with_manual :
Environ.env ->
Evd.evar_map ->
EConstr.types ->
bool ->
manual_implicits ->
implicit_status listval compute_implicits_names :
Environ.env ->
Evd.evar_map ->
EConstr.types ->
implicit_position listComputation of implicits (done using the global environment).
declare_manual_implicits local ref enriching l Manual declaration of which arguments are expected implicit. If not set, we decide if it should enrich by automatically inferd implicits depending on the current state. Unsets implicits if l is empty.
val declare_manual_implicits :
bool ->
Names.GlobRef.t ->
?enriching:bool ->
manual_implicits ->
unitIf the list is empty, do nothing, otherwise declare the implicits.
val maybe_declare_manual_implicits :
bool ->
Names.GlobRef.t ->
?enriching:bool ->
manual_implicits ->
unitval set_implicits :
bool ->
Names.GlobRef.t ->
(Names.Name.t * Glob_term.binding_kind) list list ->
unitset_implicits local ref l Manual declaration of implicit arguments. l is a list of possible sequences of implicit statuses.
val extract_impargs_data :
implicits_list list ->
((int * int) option * implicit_status list) listval projection_implicits :
Environ.env ->
Names.Projection.t ->
implicit_status list ->
implicit_status listval select_impargs_size_for_proj :
nexpectedparams:int ->
ngivenparams:int ->
nextraargs:int ->
implicits_list list ->
(implicit_status list * implicit_status list, int list Lazy.t) Util.unionval impargs_for_proj :
nexpectedparams:int ->
nextraargs:int ->
implicit_status list ->
implicit_status list * implicit_status list