Ltac2_plugin.Tac2extffi
val qhyp : Tac2types.quantified_hypothesis Tac2ffi.repr
val bindings : Tac2types.bindings Tac2ffi.repr
val constr_with_bindings : Tac2types.constr_with_bindings Tac2ffi.repr