package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c
doc/coq-core.pretyping/Coercion/index.html
Module CoercionSource
Coercions.
val inh_app_fun :
program_mode:bool ->
bool ->
Environ.env ->
Evd.evar_map ->
EConstr.unsafe_judgment ->
Evd.evar_map * EConstr.unsafe_judgment * coercion_traceinh_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_judgmentinh_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_judgmentinh_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.typesinh_coerce_to_prod env isevars t coerces t to a product type
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 ->
bool ->
Environ.env ->
Evd.evar_map ->
?flags:Evarconv.unify_flags ->
EConstr.unsafe_judgment ->
EConstr.types ->
Evd.evar_map * EConstr.unsafe_judgment * coercion_trace optionval 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 optionval inh_pattern_coerce_to :
?loc:Loc.t ->
Environ.env ->
Glob_term.cases_pattern ->
Names.inductive ->
Names.inductive ->
Glob_term.cases_patterninh_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