Module `Coercion`

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)

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 -> 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
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 hook = Environ.env -> Evd.evar_map -> flags:Evarconv.unify_flags -> EConstr.constr -> inferred:EConstr.types -> expected:EConstr.types -> (Evd.evar_map * EConstr.constr) option

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.

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