From b2f2727670853183bfbcbafb9dc19f0f71494a7b Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 8 Aug 2013 18:51:35 +0000
Subject: 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
---
 pretyping/evd.ml  | 7 ++++++-
 pretyping/evd.mli | 6 +++++-
 2 files changed, 11 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 50d8b0c8cd..3b4aa094f9 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -683,10 +683,15 @@ type open_constr = evar_map * constr
   type ['a] *)
 type 'a sigma = {
   it : 'a ;
-  sigma : evar_map}
+  eff : Declareops.side_effects;
+  sigma : evar_map
+}
 
 let sig_it x = x.it
+let sig_eff x = x.eff
 let sig_sig x = x.sigma
+let emit_side_effects eff x =
+  { x with eff = Declareops.union_side_effects eff x.eff }
 
 (**********************************************************)
 (* Failure explanation *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index f29a676c6b..e67b1f81bd 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -246,10 +246,14 @@ type open_constr = evar_map * constr
   type ['a] *)
 type 'a sigma = {
   it : 'a ;
-  sigma : evar_map}
+  eff : Declareops.side_effects;
+  sigma : evar_map
+}
 
 val sig_it  : 'a sigma -> 'a
+val sig_eff : 'a sigma -> Declareops.side_effects
 val sig_sig : 'a sigma -> evar_map
+val emit_side_effects : Declareops.side_effects -> 'a sigma -> 'a sigma
 
 (*********************************************************
    Failure explanation *)
-- 
cgit v1.2.3