[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, 2 deletions

diff --git a/API/API.mli b/API/API.mli
index d4f0872a39..a41009fa2f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1914,7 +1914,11 @@ module Summary :
 sig
 
   type frozen
-  type marshallable
+
+  type marshallable =
+    [ `Yes       (* Full data will be marshalled to disk                        *)
+    | `No        (* Full data will be store in memory, e.g. for Undo            *)
+    | `Shallow ] (* Only part of the data will be marshalled to a slave process *)
 
   type 'a summary_declaration =
     { freeze_function : marshallable -> 'a;
@@ -2062,7 +2066,6 @@ module States :
 sig
   type state
 
-  val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b
   val with_state_protection : ('a -> 'b) -> 'a -> 'b
 end
 
@@ -5799,6 +5802,9 @@ sig
     shallow : bool                 (* is the state trimmed down (libstack) *)
   }
 
+  val freeze_interp_state : Summary.marshallable -> interp_state
+  val unfreeze_interp_state : interp_state -> unit
+
   val dump_global : Libnames.reference Misctypes.or_by_notation -> unit
   val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
                             Evd.evar_map * Redexpr.red_expr) Hook.t