package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b
doc/coq-core.pretyping/Coercion/index.html
Module CoercionSource
Coercions.
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_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)
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 optionval 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 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
val reapply_coercions_body :
Evd.evar_map ->
coercion_trace ->
delayed_app_body ->
delayed_app_bodyval 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_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)