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