Module Ltac_plugin.Tacarg

val wit_intropattern : (Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.tGenintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.tTacexpr.intro_pattern) Genarg.genarg_type

Tactic related witnesses, could also live in tactics/ if other users

val wit_simple_intropattern : (Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.tGenintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.tTacexpr.intro_pattern) Genarg.genarg_type
val wit_intro_pattern : (Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.tGenintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.tTacexpr.intro_pattern) Genarg.genarg_type
val wit_quant_hyp : Tactypes.quantified_hypothesis Genarg.uniform_genarg_type
val wit_constr_with_bindings : (Constrexpr.constr_expr Tactypes.with_bindingsGenintern.glob_constr_and_expr Tactypes.with_bindingsEConstr.constr Tactypes.with_bindings Tactypes.delayed_open) Genarg.genarg_type
val wit_open_constr_with_bindings : (Constrexpr.constr_expr Tactypes.with_bindingsGenintern.glob_constr_and_expr Tactypes.with_bindingsEConstr.constr Tactypes.with_bindings Tactypes.delayed_open) Genarg.genarg_type
val wit_bindings : (Constrexpr.constr_expr Tactypes.bindingsGenintern.glob_constr_and_expr Tactypes.bindingsEConstr.constr Tactypes.bindings Tactypes.delayed_open) Genarg.genarg_type
val wit_quantified_hypothesis : Tactypes.quantified_hypothesis Genarg.uniform_genarg_type
val wit_tactic : (Tacexpr.raw_tactic_exprTacexpr.glob_tactic_exprGeninterp.Val.t) Genarg.genarg_type
val wit_ltac : (Tacexpr.raw_tactic_exprTacexpr.glob_tactic_expr, unit) Genarg.genarg_type

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

val wit_destruction_arg : (Constrexpr.constr_expr Tactypes.with_bindings Tactics.destruction_argGenintern.glob_constr_and_expr Tactypes.with_bindings Tactics.destruction_argTactypes.delayed_open_constr_with_bindings Tactics.destruction_arg) Genarg.genarg_type