title: Coq: Port a Ltac tactic using CPS style to an ML tactic (OCaml plugin)
body: <p>I'm trying to port a Coq tactic (currently written in Ltac) to OCaml, in order to be able to extend that tactic more easily (and avoid the hacks I needed to emulate in Ltac some data structures that are otherwise quite standard in OCaml).</p>
  
  <p>I am currently facing with the following problems:</p>
  
  <ol>
  <li>Can we define an OCaml tactic taking as argument a Ltac expression <code>k</code> (intended to be a continuation)?</li>
  <li>How can we apply one such Ltac expression <code>k</code> to a given constr <code>v</code>?</li>
  <li>How can we call a given Ltac tactic <code>tac</code> from a plugin?</li>
  <li>Can we pass a Ltac closure to one such tactic from the plugin code? (in order to implement the Ltac idiom <code>tac ltac:(fun r =&gt; ...)</code> in OCaml)</li>
  </ol>
  
  <p>I did a grep on the Coq sources searching <code>TACTIC EXTEND</code> but did not found some example of that kind of approach...</p>
  
  <p>As a minimal example, below is a toy Ltac tactic <code>running_example</code> that I'd like to port in OCaml, relying on the existing Ltac tactic <code>tac</code>:</p>
  
  <pre><code>Require Import Reals.
  Inductive type := Cstrict (ub : R) | Clarge (ub : R).
  
  Ltac tac g k :=
    let aux c lb := k (c lb) in
    match g with
    | Rle ?x ?y =&gt; aux Clarge y
    | Rge ?x ?y =&gt; aux Clarge x
    | Rlt ?x ?y =&gt; aux Cstrict y
    | Rgt ?x ?y =&gt; aux Cstrict x
    end.
  
  Ltac running_example expr (*point 1*) k :=
    let conc := constr:((R0 &lt;= expr)%R) in
    tac (*point 3*) conc (*point 4*) ltac:(fun r =&gt; let v :=
      match r with
      | Clarge ?x =&gt; constr:((true, x))
      | Cstrict ?x =&gt; constr:((false, x))
      end in (*point 2*)
      k v).
  
  Goal True.
  running_example 12%R ltac:(fun r =&gt; idtac r).
  (* Should display (true, 12%R) *)
  </code></pre>
  
  <p>So far I've obtained the code below (which only addresses <strong>point 1</strong>):</p>
  
  <pre><code>open Ltac_plugin
  open Stdarg
  open Tacarg
  
  TACTIC EXTEND running_example
  | [ "running_example" constr(expr) tactic0(k) ] -&gt;
    [ Proofview.Goal.nf_enter begin fun gl -&gt;
      (Tacinterp.tactic_of_value ist k) end ]
  END
  </code></pre>
  
  <p>Any pointers or suggestions are very welcome.</p>