[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

6 files changed, 19 insertions, 4 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 1524079f4..6d3d4b743 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -10,7 +10,7 @@ open Context.Named.Declaration
 
 let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
     : Safe_typing.private_constants Entries.const_entry_body =
-  Future.chain ~pure:true x begin fun ((b,ctx),fx) ->
+  Future.chain x begin fun ((b,ctx),fx) ->
     (f b , ctx) , fx
   end
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 1e8854249..76fcd5ec8 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -549,3 +549,12 @@ type tcc_lemma_value =
   | Undefined
   | Value of Term.constr
   | Not_needed
+
+(* We only "purify" on exceptions *)
+let funind_purify f x =
+  let st = Vernacentries.freeze_interp_state `No in
+  try f x
+  with e ->
+    let e = CErrors.push e in
+    Vernacentries.unfreeze_interp_state st;
+    Exninfo.iraise e
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 2e2ced790..d41abee87 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -123,3 +123,5 @@ type tcc_lemma_value =
   | Undefined
   | Value of Term.constr
   | Not_needed
+
+val funind_purify : ('a -> 'b) -> ('a -> 'b)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 299753766..9cb2a0a3f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -759,7 +759,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
   let map (c, u) = mkConstU (c, EInstance.make u) in
   let funs_constr = Array.map map funs  in
-  States.with_state_protection_on_exception
+  (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+  funind_purify
     (fun () ->
      let env = Global.env () in
      let evd = ref (Evd.from_env env) in 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 74c454334..76f859ed7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1595,7 +1595,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 			   spc () ++ str"is defined" )
       )
   in
-  States.with_state_protection_on_exception (fun () ->
+  (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+  funind_purify (fun () ->
     com_terminate
       tcc_lemma_name
       tcc_lemma_constr
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index bcd5b388a..0bf6e3d15 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -468,7 +468,9 @@ let register_ltac local tacl =
     let () = List.iter iter_rec recvars in
     List.map map rfun
   in
-  let defs = Future.transactify defs () in
+  (* STATE XXX: Review what is going on here. Why does this needs
+     protection? Why is not the STM level protection enough? Fishy *)
+  let defs = States.with_state_protection defs () in
   let iter (def, tac) = match def with
   | NewTac id ->
     Tacenv.register_ltac false local id tac;