OCaml で Coq タクティックを開発しようとしています。ここで用語を作成constrし、この用語を使用してゴール内の存在変数をインスタンス化したいと考えています。Evar_tactic.instantiate私は戦術を発動しようとしています。しかし、 type の引数が必要です Tacinterp.interp_sign * Glob_term.glob_constr。とにかくconstrこのタイプに変換する方法はありますか? または、OCaml レベルから evar をインスタンス化できる他の方法はありますか?
次に、Coq にはsetand と呼ばれるタクティックがあります。poseそれらが定義されている場所が見つかりませんでした。それらを OCaml から使いたい場合、どうすればよいですか?