package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3
doc/ltac_plugin/Ltac_plugin/Taccoerce/index.html
Module Ltac_plugin.Taccoerce
Source
Coercions from highest level generic arguments to actual data used by Ltac interpretation. Those functions examinate dynamic types and try to return something sensible according to the object content.
Exception raised whenever a coercion failed.
High-level access to values
The of_*
functions cast a given argument into a value. The to_*
do the converse, and return None
if there is a type mismatch.
Coercion functions
Source
val coerce_to_intro_pattern :
Evd.evar_map ->
Value.t ->
Tactypes.delayed_open_constr Tactypes.intro_pattern_expr
Source
val coerce_to_intro_pattern_naming :
Evd.evar_map ->
Value.t ->
Namegen.intro_pattern_naming_expr
Source
val coerce_to_evaluable_ref :
Environ.env ->
Evd.evar_map ->
Value.t ->
Tacred.evaluable_global_reference
Source
val coerce_to_intro_pattern_list :
?loc:Loc.t ->
Evd.evar_map ->
Value.t ->
Tacexpr.intro_patterns
Source
val coerce_to_quantified_hypothesis :
Evd.evar_map ->
Value.t ->
Tactypes.quantified_hypothesis
Missing generic arguments
Source
val wit_constr_under_binders :
(Util.Empty.t, Util.Empty.t, Ltac_pretype.constr_under_binders)
Genarg.genarg_type
Source
val error_ltac_variable :
?loc:Loc.t ->
Names.Id.t ->
(Environ.env * Evd.evar_map) option ->
Value.t ->
string ->
'a
Source
type appl =
| UnnamedAppl
(*For generic applications: nothing is printed
*)| GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list
(*For calls to global constants, some may alias other.
*)
Abstract application, to print ltac functions
Source
type tacvalue =
| VFun of appl * Tacexpr.ltac_trace * Loc.t option * Geninterp.Val.t Names.Id.Map.t * Names.Name.t list * Tacexpr.glob_tactic_expr
| VRec of Geninterp.Val.t Names.Id.Map.t Stdlib.ref * Tacexpr.glob_tactic_expr
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page