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, 4 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1b460b060..d8e03265d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1046,7 +1046,7 @@ let mk_open_constr_value ist gl c =
 let mk_hyp_value ist gl c = Value.of_constr (mkVar (interp_hyp ist gl c))
 let mk_int_or_var_value ist c = in_gen (topwit wit_int) (interp_int_or_var ist c)
 
-let pack_sigma (sigma,c) = {it=c;sigma=sigma}
+let pack_sigma eff (sigma,c) = {it=c;sigma=sigma;eff=eff}
 
 let extend_gl_hyps { it=gl ; sigma=sigma } sign =
   Goal.V82.new_goal_with sigma gl sign
@@ -1317,7 +1317,7 @@ and interp_letin ist gl llc u =
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist goal lz lr lmr =
   let (gl,sigma) = Goal.V82.nf_evar (project goal) (sig_it goal) in
-  let goal = { it = gl ; sigma = sigma } in
+  let goal = { it = gl ; sigma = sigma; eff = sig_eff goal } in
   let hyps = pf_hyps goal in
   let hyps = if lr then List.rev hyps else hyps in
   let concl = pf_concl goal in
@@ -1457,11 +1457,11 @@ and interp_genarg ist gl x =
            (snd (out_gen (glbwit (wit_open_constr_gen casted)) x)))
     | ConstrWithBindingsArgType ->
       in_gen (topwit wit_constr_with_bindings)
-        (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl)
+        (pack_sigma (sig_eff gl) (interp_constr_with_bindings ist (pf_env gl) (project gl)
 		       (out_gen (glbwit wit_constr_with_bindings) x)))
     | BindingsArgType ->
       in_gen (topwit wit_bindings)
-        (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
+        (pack_sigma (sig_eff gl) (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
     | ListArgType ConstrArgType ->
         let (sigma,v) = interp_genarg_constr_list ist gl x in
 	evdref := sigma;