Ltac_plugin.TacsubstSubstitution of tactics at module closing time
val subst_tactic : Mod_subst.substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_exprFor generic arguments, we declare and store substitutions in a table
val subst_genarg : Mod_subst.substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argumentMisc
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_bindingsval subst_glob_red_expr : Mod_subst.substitution -> Genredexpr.glob_red_expr -> Genredexpr.glob_red_expr