package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
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
type hook =
Environ.env ->
Evd.evar_map ->
flags:Evarconv.unify_flags ->
EConstr.constr ->
inferred:EConstr.types ->
expected:EConstr.types ->
(Evd.evar_map * EConstr.constr) optionA 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.
Activate a previously registered hook. Most recently activated hooks are tried first.
Deactivate a hook. If the hook wasn't registered/active, this does nothing.
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)