package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
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 =
(Constrexpr.explicitation
* 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 ->
Names.Name.t 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 list