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 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 -> Evd.evar_map * (EConstr.constr * EConstr.constr) * EConstr.constr * EConstr.constr list * (EConstr.t list * EConstr.t list) * (EConstr.t list * EConstr.t list) * (Reductionops.Stack.t * Reductionops.Stack.t) * EConstr.constr * (int option * EConstr.constr)
val compare_heads : Environ.env -> Evd.evar_map -> nargs:int -> EConstr.t -> EConstr.t -> Evarsolve.unification_result

Compares two constants/inductives/constructors unifying their universes. It required the number of arguments applied to the c/i/c in order to decided the kind of check it must perform.

type occurrence_match_test = Environ.env -> Evd.evar_map -> 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 : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test
val default_occurrences_selection : ?⁠allowed_evars:Evarsolve.AllowedEvars.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 -> Evd.evar_map -> Evd.evar_map * EConstr.unsafe_judgment
Functions to deal with impossible cases