Module Ltac_plugin.Tacarg
val 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_intro_pattern : (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_bindings : (Constrexpr.constr_expr Tactypes.bindings, Genintern.glob_constr_and_expr Tactypes.bindings, EConstr.constr Tactypes.bindings Tactypes.delayed_open) Genarg.genarg_typeval wit_quantified_hypothesis : Tactypes.quantified_hypothesis Genarg.uniform_genarg_type
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_ltacis subtly different fromwit_tactic: they only change for their toplevel interpretation. The one ofwit_ltacforces the tactic and discards the result.