Module Ltac_plugin.Taccoerce
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.
module Value : sig ... end
Coercion functions
val coerce_to_constr_context : Value.t -> EConstr.constr
val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Names.Id.t
val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Names.Id.t
val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tactypes.delayed_open_constr Tactypes.intro_pattern_expr
val coerce_to_intro_pattern_naming : Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
val coerce_to_hint_base : Value.t -> string
val coerce_to_int : Value.t -> int
val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders
val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr
val coerce_to_closed_constr : Environ.env -> Value.t -> EConstr.constr
val coerce_to_evaluable_ref : Environ.env -> Evd.evar_map -> Value.t -> Tacred.evaluable_global_reference
val coerce_to_constr_list : Environ.env -> Value.t -> EConstr.constr list
val coerce_to_intro_pattern_list : ?loc:Loc.t -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Names.Id.t
val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Names.Id.t list
val coerce_to_reference : Evd.evar_map -> Value.t -> Names.GlobRef.t
val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> Tactypes.quantified_hypothesis
val coerce_to_decl_or_quant_hyp : Evd.evar_map -> Value.t -> Tactypes.quantified_hypothesis
val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list
Missing generic arguments
val wit_constr_context : (Util.Empty.t, Util.Empty.t, EConstr.constr) Genarg.genarg_type
val wit_constr_under_binders : (Util.Empty.t, Util.Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type
val error_ltac_variable : ?loc:Loc.t -> Names.Id.t -> (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a
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
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
val wit_tacvalue : (Util.Empty.t, tacvalue, tacvalue) Genarg.genarg_type
val pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t