aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/global.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-08 18:51:35 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-08 18:51:35 +0000
commitb2f2727670853183bfbcbafb9dc19f0f71494a7b (patch)
tree8d9cea5ed2713ab2bfe3b142816a48c5ba615758 /library/global.ml
parent1f48326c7edf7f6e7062633494d25b254a6db82c (diff)
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
Diffstat (limited to 'library/global.ml')
-rw-r--r--library/global.ml12
1 files changed, 11 insertions, 1 deletions
diff --git a/library/global.ml b/library/global.ml
index 28b691769..5425e5930 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -14,7 +14,17 @@ open Safe_typing
(* We introduce here the global environment of the system, and we declare it
as a synchronized table. *)
-let global_env = Summary.ref empty_environment ~name:"Global environment"
+let global_env = ref empty_environment
+
+let join_safe_environment () =
+ global_env := Safe_typing.join_safe_environment !global_env
+
+let () =
+ Summary.declare_summary "Global environment"
+ { Summary.freeze_function = (fun b ->
+ if b then join_safe_environment (); !global_env);
+ unfreeze_function = (fun fr -> global_env := fr);
+ init_function = (fun () -> global_env := empty_environment) }
let safe_env () = !global_env