Ltac_plugin.TaccoerceCoercions 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.
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 ... endval coerce_to_constr_context : Value.t -> Constr_matching.contextval coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Names.Id.tval coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Names.Id.tval coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tactypes.delayed_open_constr Tactypes.intro_pattern_exprval coerce_to_intro_pattern_naming : Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_exprval coerce_to_hint_base : Value.t -> stringval coerce_to_int : Value.t -> intval coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_bindersval coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constrval coerce_to_closed_constr : Environ.env -> Value.t -> EConstr.constrval coerce_to_evaluable_ref : Environ.env -> Evd.evar_map -> Value.t -> Evaluable.tval coerce_to_constr_list : Environ.env -> Value.t -> EConstr.constr listval coerce_to_intro_pattern_list : ?loc:Loc.t -> Evd.evar_map -> Value.t -> Tacexpr.intro_patternsval coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Names.Id.tval coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Names.Id.t listval coerce_to_reference : Evd.evar_map -> Value.t -> Names.GlobRef.tval coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> Tactypes.quantified_hypothesisval coerce_to_decl_or_quant_hyp : Evd.evar_map -> Value.t -> Tactypes.quantified_hypothesisval coerce_to_int_list : Value.t -> int listval wit_constr_context : (Util.Empty.t, Util.Empty.t, Constr_matching.context) Genarg.genarg_typeval wit_constr_under_binders : (Util.Empty.t, Util.Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_typeval error_ltac_variable : ?loc:Loc.t -> Names.Id.t -> (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'atype 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_typeval pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t