title: Calling instantiate tactic from OCaml in Coq
body: <p>I am trying to develop a Coq tactic in OCaml, where I have constructed a <code>constr</code> term and now want to instantiate an existential variable in the goal with this term. I m trying to invoke the <code>Evar_tactic.instantiate</code> tactic ; but it expects an argument of type  <code>Tacinterp.interp_sign * Glob_term.glob_constr</code>. Is there anyway to convert <code>constr</code> to this type? Or any other way by which I can instantiate evars from OCaml level?</p>
  
  <p>Secondly, there are tactics called <code>set</code> and <code>pose</code> in Coq. I could not find where they are defined. If I want to use them from OCaml, how should I do it?</p>