package coq-core

  1. Overview
  2. No Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz
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.

Sourceval make_implicit_args : bool -> unit
Sourceval make_strict_implicit_args : bool -> unit
Sourceval make_strongly_strict_implicit_args : bool -> unit
Sourceval make_reversible_pattern_implicit_args : bool -> unit
Sourceval make_contextual_implicit_args : bool -> unit
Sourceval make_maximal_implicit_args : bool -> unit
Sourceval is_implicit_args : unit -> bool
Sourceval is_strict_implicit_args : unit -> bool
Sourceval is_strongly_strict_implicit_args : unit -> bool
Sourceval is_reversible_pattern_implicit_args : unit -> bool
Sourceval is_contextual_implicit_args : unit -> bool
Sourceval is_maximal_implicit_args : unit -> bool
Sourceval with_implicit_protection : ('a -> 'b) -> 'a -> 'b
...

An implicits_list is a list of positions telling which arguments of a reference can be automatically inferred

Sourcetype argument_position =
  1. | Conclusion
  2. | Hyp of int
Sourcetype implicit_explanation =
  1. | 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)

    *)
  2. | 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)

    *)
  3. | 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)

    *)
  4. | 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.

Sourcetype maximal_insertion = bool

true = maximal contextual insertion

Sourcetype force_inference = bool

true = always infer, never turn into evar/subgoal

Sourcetype implicit_position = Names.Name.t * int * int option

None = Not implicit

Sourcetype implicit_side_condition
Sourcetype implicits_list = implicit_side_condition * implicit_status list
Sourceval is_status_implicit : implicit_status -> bool
Sourceval binding_kind_of_status : implicit_status -> Glob_term.binding_kind
Sourceval is_inferable_implicit : bool -> int -> implicit_status -> bool
Sourceval name_of_implicit : implicit_status -> Names.Id.t
Sourceval match_implicit : implicit_status -> Constrexpr.explicitation -> bool
Sourceval maximal_insertion_of : implicit_status -> bool
Sourceval force_inference_of : implicit_status -> bool
Sourceval is_nondep_implicit : int -> implicit_status list -> bool
Sourceval positions_of_implicits : implicits_list -> int list
Sourcetype manual_implicits = (Names.Name.t * bool) option CAst.t list
Sourceval compute_implicits_with_manual : Environ.env -> Evd.evar_map -> EConstr.types -> bool -> manual_implicits -> implicit_status list
Sourceval compute_implicits_names : Environ.env -> Evd.evar_map -> EConstr.types -> implicit_position list
Computation of implicits (done using the global environment).
Sourceval declare_var_implicits : Names.variable -> impl:Glob_term.binding_kind -> unit
Sourceval declare_constant_implicits : Names.Constant.t -> unit
Sourceval declare_mib_implicits : Names.MutInd.t -> unit
Sourceval declare_implicits : bool -> Names.GlobRef.t -> unit

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.

Sourceval declare_manual_implicits : bool -> Names.GlobRef.t -> ?enriching:bool -> manual_implicits -> unit

If the list is empty, do nothing, otherwise declare the implicits.

Sourceval maybe_declare_manual_implicits : bool -> Names.GlobRef.t -> ?enriching:bool -> manual_implicits -> unit
Sourceval set_implicits : bool -> Names.GlobRef.t -> (Names.Name.t * Glob_term.binding_kind) list list -> unit

set_implicits local ref l Manual declaration of implicit arguments. l is a list of possible sequences of implicit statuses.

Sourceval implicits_of_global : Names.GlobRef.t -> implicits_list list
Sourceval extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list
Sourceval make_implicits_list : implicit_status list -> implicits_list list
Sourceval drop_first_implicits : int -> implicits_list -> implicits_list
Sourceval projection_implicits : Environ.env -> Names.Projection.t -> implicit_status list -> implicit_status list
Sourceval select_impargs_size : int -> implicits_list list -> implicit_status list
Sourceval select_stronger_impargs : implicits_list list -> implicit_status list
Sourceval 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.union
Sourceval impargs_for_proj : nexpectedparams:int -> nextraargs:int -> implicit_status list -> implicit_status list * implicit_status list