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.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/tac2ffi.mli')

diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 36743f3346..cb6d5a1e49 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -143,6 +143,7 @@ type ('a, 'b) fun1
 
 val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
 
+val to_fun1 : 'a repr -> 'b repr -> valexpr -> ('a, 'b) fun1
 val fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr
 
 val valexpr : valexpr repr
-- 
cgit v1.2.3