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, 10 insertions, 8 deletions

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index aecbbfe856..be661587ad 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -176,7 +176,7 @@ let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
 let dummy_goal env =
   let (gl,_,sigma) = 
     Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in
-  {Evd.it = gl;
+  {Evd.it = gl; Evd.eff=Declareops.no_seff;
    Evd.sigma = sigma}
 
 let exec_tactic env n f args =
@@ -679,8 +679,10 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
   let lemma1 = constr_of params.(3) in
   let lemma2 = constr_of params.(4) in
 
-  let lemma1 = decl_constant (Id.to_string name^"_ring_lemma1") lemma1 in
-  let lemma2 = decl_constant (Id.to_string name^"_ring_lemma2") lemma2 in
+  let lemma1 =
+    decl_constant (Id.to_string name^"_ring_lemma1") (Future.from_val ( lemma1,Declareops.no_seff)) in
+  let lemma2 =
+    decl_constant (Id.to_string name^"_ring_lemma2") (Future.from_val ( lemma2,Declareops.no_seff)) in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
@@ -1030,11 +1032,11 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi
     match inj with
       | Some thm -> mkApp(constr_of params.(8),[|thm|])
       | None -> constr_of params.(7) in
-  let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") lemma1 in
-  let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") lemma2 in
-  let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") lemma3 in
-  let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") lemma4 in
-  let cond_lemma = decl_constant (Id.to_string name^"_lemma5") cond_lemma in
+  let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") (Future.from_val (lemma1,Declareops.no_seff)) in
+  let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") (Future.from_val (lemma2,Declareops.no_seff)) in
+  let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") (Future.from_val (lemma3,Declareops.no_seff)) in
+  let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") (Future.from_val (lemma4,Declareops.no_seff)) in
+  let cond_lemma = decl_constant (Id.to_string name^"_lemma5") (Future.from_val (cond_lemma,Declareops.no_seff)) in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =