From 0ea9b2f2a972d49844a6e784d2cf19feb4dc7636 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 3 Mar 2014 14:39:25 +0100
Subject: STM: when finish a task hcons universe constraints

---
 toplevel/stm.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 12c5cafd7f..17a5b13313 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -892,11 +892,13 @@ end = struct (* {{{ *)
         match c.Declarations.const_body with
         | Declarations.OpaqueDef lc ->
             let uc = Option.get (Opaqueproof.get_constraints lc) in
+            let uc =
+              Future.chain ~greedy:true ~pure:true uc Univ.hcons_constraints in
             let pr = Opaqueproof.get_proof lc in
             let pr = Future.chain ~greedy:true ~pure:true pr discharge in
             let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
-            ignore(Future.join pr);
-            ignore(Future.join uc);
+            Future.sink pr;
+            Future.sink uc;
             u.(bucket) <- uc;
             p.(bucket) <- pr
         | _ -> assert false
-- 
cgit v1.2.3