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

diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 5559e6b81..56635c801 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -22,7 +22,6 @@ type interp_state = { (* TODO: inline records in OCaml 4.03 *)
 
 val freeze_interp_state : Summary.marshallable -> interp_state
 val unfreeze_interp_state : interp_state -> unit
-val _dummy_interp_state : interp_state
 
 (** The main interpretation function of vernacular expressions *)
 val interp :
@@ -39,7 +38,9 @@ val interp :
 
 val make_cases : string -> string list list
 
-val with_fail : bool -> (unit -> unit) -> unit
+(* XXX STATE: this type hints that restoring the state should be the
+   caller's responsibility *)
+val with_fail : interp_state -> bool -> (unit -> unit) -> unit
 
 val command_focus : unit Proof.focus_kind