Module Ltac_plugin.Tacsubst
val subst_tactic : Mod_subst.substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr
val subst_genarg : Mod_subst.substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument
val subst_glob_constr_and_expr : Mod_subst.substitution -> Genintern.glob_constr_and_expr -> Genintern.glob_constr_and_exprval subst_glob_with_bindings : Mod_subst.substitution -> Genintern.glob_constr_and_expr Tactypes.with_bindings -> Genintern.glob_constr_and_expr Tactypes.with_bindings