Phantom type for typed closures.

2 files changed, 13 insertions, 0 deletions

diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index ede4836750..5460643bb5 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -280,6 +280,10 @@ let reference = {
   r_id = false;
 }
 
+type ('a, 'b) fun1 = closure
+
+let fun1 (r0 : 'a repr) (r1 : 'b repr) : ('a, 'b) fun1 repr = closure
+
 let rec apply : type a. a arity -> a -> valexpr list -> valexpr Proofview.tactic =
   fun arity f args -> match args, arity with
   | [], arity -> Proofview.tclUNIT (ValCls (MLTactic (arity, f)))
@@ -311,3 +315,6 @@ let abstract n f =
   let () = assert (n > 0) in
   let NClosure (arity, f) = abstract n f in
   MLTactic (arity, f [])
+
+let app_fun1 cls r0 r1 x =
+  apply cls [r0.r_of x] >>= fun v -> Proofview.tclUNIT (r1.r_to v)
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index ed63f2d4a6..af854e2d07 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -122,6 +122,12 @@ val of_ext : 'a Val.tag -> 'a -> valexpr
 val to_ext : 'a Val.tag -> valexpr -> 'a
 val repr_ext : 'a Val.tag -> 'a repr
 
+type ('a, 'b) fun1
+
+val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
+
+val fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr
+
 val valexpr : valexpr repr
 
 (** {5 Dynamic tags} *)