package coq

  1. Overview
  2. Docs
On This Page
  1. Coercions.
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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

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)