[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

2 files changed, 3 insertions, 3 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 23f96b5a3..469e1a011 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -156,7 +156,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let ce =
     if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
     else { ce with
-      const_entry_body = Future.chain ~pure:true ce.const_entry_body
+      const_entry_body = Future.chain ce.const_entry_body
         (fun (pt, _) -> pt, ()) } in
   let (cb, ctx), () = Future.force ce.const_entry_body in
   let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index cd4d1dcf6..621178982 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -373,11 +373,11 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
           let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
-       fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t))
+       fun t p -> Future.split2 (Future.chain p (make_body t))
     else
       fun t p ->
         Future.from_val (univctx, nf t),
-        Future.chain ~pure:true p (fun (pt,eff) ->
+        Future.chain p (fun (pt,eff) ->
           (* Deferred proof, we already checked the universe declaration with
              the initial universes, ensure that the final universes respect
              the declaration as well. If the declaration is non-extensible,