Module Evarconv

Unification for type inference.
type unify_flags = Evarsolve.unify_flags
val default_flags_of : ?⁠subterm_ts:TransparentState.t -> TransparentState.t -> unify_flags

The default subterm transparent state is no unfoldings

type unify_fun = unify_flags -> Environ.env -> Evd.evar_map -> Evd.conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
val conv_fun : unify_fun -> Evarsolve.unifier
exception UnableToUnify of Evd.evar_map * Pretype_errors.unification_error
Main unification algorithm for type inference.
val unify_delay : ?⁠flags:unify_flags -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map
val unify_leq_delay : ?⁠flags:unify_flags -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map
val the_conv_x : Environ.env -> ?⁠ts:TransparentState.t -> EConstr.constr -> EConstr.constr -> Evd.evar_map -> Evd.evar_map

returns exception UnableToUnify with best known evar_map if not unifiable

val the_conv_x_leq : Environ.env -> ?⁠ts:TransparentState.t -> EConstr.constr -> EConstr.constr -> Evd.evar_map -> Evd.evar_map

The same function resolving evars by side-effect and catching the exception

val conv : Environ.env -> ?⁠ts:TransparentState.t -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option
val cumul : Environ.env -> ?⁠ts:TransparentState.t -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option
val unify : ?⁠flags:unify_flags -> ?⁠with_ho:bool -> Environ.env -> Evd.evar_map -> Evd.conv_pb -> EConstr.constr -> EConstr.constr -> Evd.evar_map

This function also calls solve_unif_constraints_with_heuristics to resolve any remaining constraints. In case of success the two terms are unified without condition.

The with_ho option tells if higher-order unification should be tried to resolve the constraints.

@raises a PretypeError if it cannot unify

Unification heuristics.
val solve_unif_constraints_with_heuristics : Environ.env -> ?⁠flags:unify_flags -> ?⁠with_ho:bool -> Evd.evar_map -> Evd.evar_map
val check_problems_are_solved : Environ.env -> Evd.evar_map -> unit
val check_conv_record : Environ.env -> Evd.evar_map -> Reductionops.state -> Reductionops.state -> Univ.ContextSet.t * (EConstr.constr * EConstr.constr) * EConstr.constr * EConstr.constr list * (EConstr.constr Reductionops.Stack.t * EConstr.constr Reductionops.Stack.t) * (EConstr.constr Reductionops.Stack.t * EConstr.constr Reductionops.Stack.t) * (EConstr.constr Reductionops.Stack.t * EConstr.constr Reductionops.Stack.t) * EConstr.constr * (int option * EConstr.constr)
type occurrence_match_test = Environ.env -> Evd.evar_map -> EConstr.constr -> Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.constr -> bool * Evd.evar_map
type occurrence_selection =
| AtOccurrences of Locus.occurrences
| Unspecified of Evd.Abstraction.abstraction
val default_occurrence_selection : occurrence_selection

By default, unspecified, not preferring abstraction. This provides the most general solutions.

type occurrences_selection = occurrence_match_test * occurrence_selection list
val default_occurrence_test : frozen_evars:Evar.Set.t -> TransparentState.t -> occurrence_match_test
val default_occurrences_selection : ?⁠frozen_evars:Evar.Set.t -> TransparentState.t -> int -> occurrences_selection

default_occurrence_selection n Gives the default test and occurrences for n arguments

val second_order_matching : unify_flags -> Environ.env -> Evd.evar_map -> EConstr.existential -> occurrences_selection -> EConstr.constr -> Evd.evar_map * bool
val set_solve_evars : (Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr) -> unit
val set_evar_conv : unify_fun -> unit

Override default evar_conv_x algorithm.

val evar_conv_x : unify_fun

The default unification algorithm with evars and universes.

val evar_unify : Evarsolve.unifier
val coq_unit_judge : Environ.env -> EConstr.unsafe_judgment Univ.in_universe_context_set
Functions to deal with impossible cases