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

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 7ca033383..210d601fb 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -26,6 +26,15 @@ type safe_environment
 
 val env_of_safe_env : safe_environment -> Environ.env
 
+val sideff_of_con : safe_environment -> constant -> side_effect 
+
+val is_curmod_library : safe_environment -> bool
+
+
+(* safe_environment has functional data affected by lazy computations,
+ * thus this function returns a new safe_environment *)
+val join_safe_environment : safe_environment -> safe_environment
+
 val empty_environment : safe_environment
 val is_empty : safe_environment -> bool
 
@@ -109,6 +118,8 @@ val export : safe_environment -> DirPath.t
 val import : compiled_library -> Digest.t -> safe_environment
       -> module_path * safe_environment * Nativecode.symbol array
 
+val join_compiled_library : compiled_library -> unit
+
 (** {6 Typing judgments } *)
 
 type judgment