Module Pretyping

This file implements type inference. It maps glob_constr (i.e. untyped terms whose names are located) to constr. In particular, it drives complex pattern-matching problems ("match") into elementary ones, insertion of coercions and resolution of implicit arguments.

val add_bidirectionality_hint : Names.GlobRef.t -> int -> unit

A bidirectionality hint `n` for a global `g` tells the pretyper to use typing information from the context after typing the `n` for arguments of an application of `g`.

val get_bidirectionality_hint : Names.GlobRef.t -> int option
val clear_bidirectionality_hint : Names.GlobRef.t -> unit
val interp_known_glob_level : ?⁠loc:Loc.t -> Evd.evar_map -> Glob_term.glob_sort_name -> Univ.Level.t
val search_guard : ?⁠loc:Loc.t -> Environ.env -> int list list -> Constr.rec_declaration -> int array
type typing_constraint =
| OfType of EConstr.types
| IsType
| WithoutTypeConstraint
type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> Evd.evar_map * EConstr.constr
type inference_flags = {
use_typeclasses : bool;
solve_unification_constraints : bool;
fail_evar : bool;
expand_evars : bool;
program_mode : bool;
polymorphic : bool;
}
val default_inference_flags : bool -> inference_flags
val no_classes_no_fail_inference_flags : inference_flags
val all_no_fail_flags : inference_flags
val all_and_fail_flags : inference_flags
val understand_tcc : ?⁠flags:inference_flags -> Environ.env -> Evd.evar_map -> ?⁠expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
val understand_tcc_ty : ?⁠flags:inference_flags -> Environ.env -> Evd.evar_map -> ?⁠expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr * EConstr.types

As understand_tcc but also returns the type of the elaborated term. The expand_evars flag is not applied to the type (only to the term).

val understand_ltac : inference_flags -> Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t
val understand : ?⁠flags:inference_flags -> ?⁠expected_type:typing_constraint -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> EConstr.constr Evd.in_evar_universe_context

Standard call to get a constr from a glob_constr, resolving implicit arguments and coercions, and compiling pattern-matching; the default inference_flags tells to use type classes and heuristics (but no external tactic solver hook), as well as to ensure that conversion problems are all solved and that no unresolved evar remains, expanding evars.

val solve_remaining_evars : ?⁠hook:inference_hook -> inference_flags -> Environ.env -> ?⁠initial:Evd.evar_map -> Evd.evar_map -> Evd.evar_map
val check_evars_are_solved : program_mode:bool -> Environ.env -> ?⁠initial:Evd.evar_map -> Evd.evar_map -> unit
val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit

check_evars env initial_sigma extended_sigma c fails if some new unresolved evar remains in c