Ltac2_ltac1_plugin.Tac2core_ltac1val wit_ltac2in1 : (Names.Id.t CAst.t list * Ltac2_plugin.Tac2expr.raw_tacexpr, Names.Id.t list * Ltac2_plugin.Tac2expr.glb_tacexpr, Util.Empty.t) Genarg.genarg_typeLtac2 quotations in Ltac1 code
val wit_ltac2in1_val : (Names.Id.t CAst.t list * Ltac2_plugin.Tac2expr.raw_tacexpr, Ltac2_plugin.Tac2expr.glb_tacexpr, Util.Empty.t) Genarg.genarg_typeLtac2 quotations in Ltac1 returning Ltac1 values. When ids are bound interning turns them into Ltac1.lambda.
val wit_ltac2_val : (Util.Empty.t, unit, Util.Empty.t) Genarg.genarg_typeEmbedding Ltac2 closures of type Ltac1.t -> Ltac1.t inside Ltac1. There is no relevant data because arguments are passed by conventional names.