Module Ltac_plugin.Taccoerce

exception CannotCoerceTo of string

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.

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