Ltac_plugin.Tacargval wit_intropattern :
( Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t,
Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t,
Tacexpr.intro_pattern )
Genarg.genarg_typeTactic related witnesses, could also live in tactics/ if other users
val wit_simple_intropattern :
( Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t,
Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t,
Tacexpr.intro_pattern )
Genarg.genarg_typeval wit_quant_hyp : Tactypes.quantified_hypothesis Genarg.uniform_genarg_typeval wit_constr_with_bindings :
( Constrexpr.constr_expr Tactypes.with_bindings,
Genintern.glob_constr_and_expr Tactypes.with_bindings,
EConstr.constr Tactypes.with_bindings Tactypes.delayed_open )
Genarg.genarg_typeval wit_open_constr_with_bindings :
( Constrexpr.constr_expr Tactypes.with_bindings,
Genintern.glob_constr_and_expr Tactypes.with_bindings,
EConstr.constr Tactypes.with_bindings Tactypes.delayed_open )
Genarg.genarg_typeval wit_quantified_hypothesis :
Tactypes.quantified_hypothesis Genarg.uniform_genarg_typeGeneric arguments based on Ltac.
val wit_tactic :
( Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t )
Genarg.genarg_typeval wit_ltac :
( Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, unit )
Genarg.genarg_typewit_ltac is subtly different from wit_tactic: they only change for their toplevel interpretation. The one of wit_ltac forces the tactic and discards the result.