我正在尝试在 OCaml 中开发 Coq 策略，我在其中构建了一个constr术语，现在想用这个术语在目标中实例化一个存在变量。我正在尝试调用该Evar_tactic.instantiate策略；但它需要一个类型的参数 Tacinterp.interp_sign * Glob_term.glob_constr。反正有没有转换constr成这种类型？或者我可以从 OCaml 级别实例化 evas 的任何其他方式？
其次，在 Coq 中有一种叫做setand的策略。pose我找不到它们的定义位置。如果我想从 OCaml 使用它们，我应该怎么做？