Module Coercion

Coercions.
type coercion_trace
val empty_coercion_trace : coercion_trace
val reapply_coercions : Evd.evar_map -> coercion_trace -> EConstr.t -> EConstr.t
val inh_app_fun : program_mode:bool -> bool -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> Evd.evar_map * EConstr.unsafe_judgment * coercion_trace

inh_app_fun resolve_tc env isevars j coerces j to a function; i.e. it inserts a coercion into j, if needed, in such a way it gets as type a product; it returns j if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing)

val inh_coerce_to_sort : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> Evd.evar_map * EConstr.unsafe_type_judgment

inh_coerce_to_sort env isevars j coerces j to a type; i.e. it inserts a coercion into j, if needed, in such a way it gets as type a sort; it fails if no coercion is applicable

val inh_coerce_to_base : ?⁠loc:Loc.t -> program_mode:bool -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> Evd.evar_map * EConstr.unsafe_judgment

inh_coerce_to_base env isevars j coerces j to its base type; i.e. it inserts a coercion into j, if needed, in such a way it gets as type its base type (the notion depends on the coercion system)

val inh_coerce_to_prod : ?⁠loc:Loc.t -> program_mode:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.types

inh_coerce_to_prod env isevars t coerces t to a product type

val inh_conv_coerce_to : ?⁠loc:Loc.t -> program_mode:bool -> bool -> Environ.env -> Evd.evar_map -> ?⁠flags:Evarconv.unify_flags -> EConstr.unsafe_judgment -> EConstr.types -> Evd.evar_map * EConstr.unsafe_judgment * coercion_trace option
val inh_conv_coerce_rigid_to : ?⁠loc:Loc.t -> program_mode:bool -> bool -> Environ.env -> Evd.evar_map -> ?⁠flags:Evarconv.unify_flags -> EConstr.unsafe_judgment -> EConstr.types -> Evd.evar_map * EConstr.unsafe_judgment * coercion_trace option
val inh_conv_coerces_to : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> ?⁠flags:Evarconv.unify_flags -> EConstr.types -> EConstr.types -> Evd.evar_map

inh_conv_coerces_to loc env isevars t t' checks if an object of type t is coercible to an object of type t' adding evar constraints if needed; it fails if no coercion exists

val inh_pattern_coerce_to : ?⁠loc:Loc.t -> Environ.env -> Glob_term.cases_pattern -> Names.inductive -> Names.inductive -> Glob_term.cases_pattern

inh_pattern_coerce_to loc env isevars pat ind1 ind2 coerces the Cases pattern pat typed in ind1 into a pattern typed in ind2; raises Not_found if no coercion found