From b245a6c46bc3ef70142e8a165f6cde54265b941e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 May 2019 11:51:31 +0200
Subject: Statically ensure the content of delayed proofs in vio file.

Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.

This also enhances debug printing, as the latter is unable to properly
print futures.
---
 stm/stm.ml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 9e9d23ba93..30cf8a0622 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1846,13 +1846,8 @@ end = struct (* {{{ *)
         let pr = map (Option.get (Global.body_of_constant_body c)) in
         let pr = discharge pr in
         let pr = Constr.hcons pr in
-        let return c =
-          let fc = Future.from_val c in
-          let _ = Future.join fc in
-          fc
-        in
-        u.(bucket) <- return uc;
-        p.(bucket) <- return pr;
+        u.(bucket) <- Some uc;
+        p.(bucket) <- Some pr;
         u, Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
-- 
cgit v1.2.3