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 -> ?use_coercions:bool -> 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)

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

inh_conv_coerce_to resolve_tc Loc.t env isevars j t coerces j to an object of type t; i.e. it inserts a coercion into j, if needed, in such a way t and j.uj_type are convertible; it fails if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing)

val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> resolve_tc:bool -> ?use_coercions: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 -> resolve_tc:bool -> ?use_coercions:bool -> Environ.env -> Evd.evar_map -> ?flags:Evarconv.unify_flags -> EConstr.unsafe_judgment -> EConstr.types -> Evd.evar_map * EConstr.unsafe_judgment * coercion_trace option

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

val register_hook : name:string -> ?override:bool -> hook -> unit

A plugin can override the coercion mechanism by registering a hook here. Note that these hooks will only be trigerred when no direct or reversible coercion applies. Newly registered hooks are not active by default, see activate_hook below. The same hook cannot be registered twice, except if override is true. Beware that this addition is not persistent, it is up to the plugin to use libobject if needed.

val activate_hook : name:string -> unit

Activate a previously registered hook. Most recently activated hooks are tried first.

val deactivate_hook : name:string -> unit

Deactivate a hook. If the hook wasn't registered/active, this does nothing.

type delayed_app_body
val start_app_body : Evd.evar_map -> 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 -> resolve_tc:bool -> ?use_coercions: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)