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_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 remove_subset : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.types

remove_subset env sigma t applies program mode transformations to t, recursively transforming {x : A | P} into A

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_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

type delayed_app_body
val start_app_body : Evd.evar_map -> EConstr.constr -> delayed_app_body
val push_arg : delayed_app_body -> EConstr.constr -> delayed_app_body
val force_app_body : delayed_app_body -> EConstr.constr
val reapply_coercions_body : Evd.evar_map -> coercion_trace -> delayed_app_body -> delayed_app_body
val inh_app_fun : program_mode:bool -> bool -> Environ.env -> Evd.evar_map -> delayed_app_body -> EConstr.types -> Evd.evar_map * delayed_app_body * EConstr.types * 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)