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_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.