From 67b85b04d6d78d8e4bbec58eab4b0630abfcd67d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 25 Apr 2014 17:04:33 +0200
Subject: Opaqueproofs: sink futures when interactive

---
 kernel/opaqueproof.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 50208e28a0..102dcf99f3 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -52,7 +52,7 @@ let turn_indirect o = match o with
   | Direct (d,cu) ->
       let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
       match !mk_indirect (d,cu) with
-      | None -> NoIndirect([],cu)
+      | None -> Future.sink cu; NoIndirect([],cu)
       | Some (dp,i) -> Indirect ([],dp,i)
 
 let subst_opaque sub = function
-- 
cgit v1.2.3