Module Impargs

Implicit Arguments
val make_implicit_args : bool -> unit
val make_strict_implicit_args : bool -> unit
val make_strongly_strict_implicit_args : bool -> unit
val make_reversible_pattern_implicit_args : bool -> unit
val make_contextual_implicit_args : bool -> unit
val make_maximal_implicit_args : bool -> unit
val is_implicit_args : unit -> bool
val is_strict_implicit_args : unit -> bool
val is_strongly_strict_implicit_args : unit -> bool
val is_reversible_pattern_implicit_args : unit -> bool
val is_contextual_implicit_args : unit -> bool
val is_maximal_implicit_args : unit -> bool
val with_implicit_protection : ('a -> 'b) -> 'a -> 'b
...
type argument_position =
| Conclusion
| Hyp of int
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

type maximal_insertion = bool

true = maximal contextual insertion

type force_inference = bool

true = always infer, never turn into evar/subgoal

type implicit_status = (Names.Id.t * implicit_explanation * (maximal_insertion * force_inference)) option

None = Not implicit

type implicit_side_condition
type implicits_list = implicit_side_condition * implicit_status list
val is_status_implicit : implicit_status -> bool
val is_inferable_implicit : bool -> int -> implicit_status -> bool
val name_of_implicit : implicit_status -> Names.Id.t
val maximal_insertion_of : implicit_status -> bool
val force_inference_of : implicit_status -> bool
val positions_of_implicits : implicits_list -> int list
type manual_implicits = (Names.Name.t * bool) option CAst.t list
val compute_implicits_with_manual : Environ.env -> Evd.evar_map -> EConstr.types -> bool -> manual_implicits -> implicit_status list
val compute_implicits_names : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t list
Computation of implicits (done using the global environment).
val declare_var_implicits : Names.variable -> impl:Glob_term.binding_kind -> unit
val declare_constant_implicits : Names.Constant.t -> unit
val declare_mib_implicits : Names.MutInd.t -> unit
val declare_implicits : bool -> Names.GlobRef.t -> unit
val declare_manual_implicits : bool -> Names.GlobRef.t -> ?⁠enriching:bool -> manual_implicits -> unit
val maybe_declare_manual_implicits : bool -> Names.GlobRef.t -> ?⁠enriching:bool -> manual_implicits -> unit
type implicit_kind =
| Implicit
| MaximallyImplicit
| NotImplicit
val set_implicits : bool -> Names.GlobRef.t -> implicit_kind list list -> unit

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

val implicits_of_global : Names.GlobRef.t -> implicits_list list
val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list
val make_implicits_list : implicit_status list -> implicits_list list
val drop_first_implicits : int -> implicits_list -> implicits_list
val projection_implicits : Environ.env -> Names.Projection.t -> implicit_status list -> implicit_status list
val select_impargs_size : int -> implicits_list list -> implicit_status list
val select_stronger_impargs : implicits_list list -> implicit_status list