State Transaction Machine

The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).

The observe id function runs the transactions necessary to reach to the
state id.  Transaction being on a merged branch are not executed but
stored into a future.

The finish function calls observe on the tip of the current branch.

Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.

This is the work described in the Coq Workshop 2012 paper.

Coq is compile with thread support from now on.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 13 deletions

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index fd074386e..7d14d1408 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1013,10 +1013,9 @@ let do_save () = Lemmas.save_named false
 *)
 
 let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) =
-  let previous_state = States.freeze ~marshallable:false in
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
   let funs_constr = Array.map mkConst funs  in
-  try
+  States.with_state_protection (fun () ->
     let graphs_constr = Array.map mkInd graphs in
     let lemmas_types_infos =
       Util.Array.map2_i
@@ -1044,7 +1043,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	  Array.of_list
 	    (List.map
 	       (fun entry ->
-		  (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
+		  (fst(Future.force entry.Entries.const_entry_body), Option.get entry.Entries.const_entry_type )
 	       )
 	       (make_scheme (Array.map_to_list (fun const -> const,GType None) funs))
 	    )
@@ -1122,16 +1121,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
 	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
-      funs;
-  with reraise ->
-    (* In case of problem, we reset all the lemmas *)
-    Pfedit.delete_all_proofs ();
-    States.unfreeze previous_state;
-    raise reraise
-
-
-
-
+      funs)
+  ()
 
 (***********************************************)