[stm] Remove state-handling from Futures.

We make Vernacentries.interp functional wrt state, and thus remove
state-handling from `Future`. Now, a future needs a closure if it
wants to preserve state.

Consequently, `Vernacentries.interp` takes a state, and returns the
new one.

We don't explicitly thread the state in the STM yet, instead, we
recover the state that was used before and pass it explicitly to
`interp`.

I have tested the commit with the files in interactive, but we aware
that some new bugs may appear or old ones be made more apparent.
However, I am confident that this step will improve our understanding
of bugs.

In some cases, we perform a bit more summary wrapping/unwrapping. This
will go away in future commits; informal timings for a full make:

- master:
  real	2m11,027s
  user	8m30,904s
  sys	1m0,000s

- no_futures:
  real	2m8,474s
  user	8m34,380s
  sys	0m59,156s

1 files changed, 8 insertions, 8 deletions

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 5e20c1b51..400f9feee 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -78,12 +78,12 @@ let subst_opaque sub = function
 let iter_direct_opaque f = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
-      Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
+      Direct (d,Future.chain cu (fun (c, u) -> f c; c, u))
 
 let discharge_direct_opaque ~cook_constr ci = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
-      Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
+      Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
 
 let join_opaque { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) -> ignore(Future.join cu)
@@ -105,7 +105,7 @@ let force_proof { opaque_val = prfs; opaque_dir = odp } = function
   | Indirect (l,dp,i) ->
       let pt =
         if DirPath.equal dp odp
-        then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+        then Future.chain (snd (Int.Map.find i prfs)) fst
         else !get_opaque dp i in
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
@@ -120,20 +120,20 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp } = function
         | Some u -> Future.force u
 
 let get_constraints { opaque_val = prfs; opaque_dir = odp } = function
-  | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd)
+  | Direct (_,cu) -> Some(Future.chain cu snd)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
-      then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd)
+      then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
       else !get_univ dp i
 
 let get_proof { opaque_val = prfs; opaque_dir = odp } = function
-  | Direct (_,cu) -> Future.chain ~pure:true cu fst
+  | Direct (_,cu) -> Future.chain cu fst
   | Indirect (l,dp,i) ->
       let pt =
         if DirPath.equal dp odp
-        then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+        then Future.chain (snd (Int.Map.find i prfs)) fst
         else !get_opaque dp i in
-      Future.chain ~pure:true pt (fun c ->
+      Future.chain pt (fun c ->
         force_constr (List.fold_right subst_substituted l (from_val c)))
  
 module FMap = Future.UUIDMap