From 0145084daa86b35a1d2a8285c4e16a9a231e3652 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 1 Oct 2017 19:10:11 +0200
Subject: Using Ltac2 native closures in some tactic APIs.

---
 src/tac2ffi.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/tac2ffi.ml')

diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 7960d4d45f..923a29e5c5 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -329,6 +329,7 @@ let reference = {
 type ('a, 'b) fun1 = closure
 
 let fun1 (r0 : 'a repr) (r1 : 'b repr) : ('a, 'b) fun1 repr = closure
+let to_fun1 r0 r1 f = to_closure f
 
 let rec apply : type a. a arity -> a -> valexpr list -> valexpr Proofview.tactic =
   fun arity f args -> match args, arity with
-- 
cgit v1.2.3