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, 14 insertions, 0 deletions

diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index c4d67ba52..635b8c47a 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -28,6 +28,19 @@ val body_of_constant : constant_body -> Term.constr option
 
 val is_opaque : constant_body -> bool
 
+(** Side effects *)
+
+val string_of_side_effect : side_effect -> string
+
+type side_effects
+val no_seff : side_effects
+val iter_side_effects : (side_effect -> unit) -> side_effects -> unit
+val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a
+val uniquize_side_effects : side_effects -> side_effects
+val union_side_effects : side_effects -> side_effects -> side_effects
+val flatten_side_effects : side_effects list -> side_effects
+val side_effects_of_list : side_effect list -> side_effects
+val cons_side_effects : side_effect -> side_effects -> side_effects
 
 (** {6 Inductive types} *)
 
@@ -45,6 +58,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
 
+val join_constant_body : constant_body -> unit
 
 (** {6 Hash-consing} *)