diff options
| author | Pierre-Marie Pédrot | 2017-10-01 19:10:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-01 19:18:59 +0200 |
| commit | 0145084daa86b35a1d2a8285c4e16a9a231e3652 (patch) | |
| tree | 5a589caf12c346ec9a1ac17521d35a07191eddd5 /src/tac2ffi.mli | |
| parent | 95f0ba81363a464e416fa2fdba3e4170accd4d96 (diff) | |
Using Ltac2 native closures in some tactic APIs.
Diffstat (limited to 'src/tac2ffi.mli')
| -rw-r--r-- | src/tac2ffi.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |