aboutsummaryrefslogtreecommitdiff
path: root/src/tac2stdlib.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-09-06 18:55:27 +0200
committerPierre-Marie Pédrot2017-09-06 18:59:02 +0200
commit841c4a028b5cf7e3cfff6b91a33db38a4b8d54df (patch)
tree6cf54e01a8ffd8221b040a47bb95c6051aaf6799 /src/tac2stdlib.ml
parent6985a2001d28ff0850198d8219d7b791a226bdac (diff)
The interp_app function now takes a closure as an argument.
Diffstat (limited to 'src/tac2stdlib.ml')
-rw-r--r--src/tac2stdlib.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 713a5f1b1c..79af41b7d0 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -18,7 +18,7 @@ module Value = Tac2ffi
let return x = Proofview.tclUNIT x
let v_unit = Value.of_unit ()
-let thaw bt f = Tac2interp.interp_app bt f [v_unit]
+let thaw bt f = Tac2interp.interp_app bt (Value.to_closure f) [v_unit]
let to_pair f g = function
| ValBlk (0, [| x; y |]) -> (f x, g y)