package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct