Ltac2_plugin.Tac2substval subst_type : Mod_subst.substitution -> 'a Tac2expr.glb_typexpr -> 'a Tac2expr.glb_typexprval subst_expr : Mod_subst.substitution -> Tac2expr.glb_tacexpr -> Tac2expr.glb_tacexprval subst_quant_typedef : Mod_subst.substitution -> Tac2expr.glb_quant_typedef -> Tac2expr.glb_quant_typedefval subst_type_scheme : Mod_subst.substitution -> Tac2expr.type_scheme -> Tac2expr.type_schemeval subst_rawexpr : Mod_subst.substitution -> Tac2expr.raw_tacexpr -> Tac2expr.raw_tacexpr