diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-18 13:52:10 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-18 13:52:10 +0000 |
| commit | 020aa7a8e9bca88631e6d7fa68d1ff462f5af25a (patch) | |
| tree | fbd29a9da01f1de8b290547fd64596a56ef83aed /library/global.ml | |
| parent | 27bbbdc0ef930b1efca7b268e859d4e93927b365 (diff) | |
Future: ported to Ephemeron + exception enhancing
A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.
A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost. This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/library/global.ml b/library/global.ml index fd6cce46f..3b0e504d8 100644 --- a/library/global.ml +++ b/library/global.ml @@ -26,15 +26,12 @@ let global_env = ref Safe_typing.empty_environment let join_safe_environment () = global_env := Safe_typing.join_safe_environment !global_env -let prune_safe_environment env = Safe_typing.prune_safe_environment env -(* XXX TODO pass args so that these functions can stop at the current - * file boundaries *) let () = Summary.declare_summary "Global environment" { Summary.freeze_function = (function | `Yes -> join_safe_environment (); !global_env | `No -> !global_env - | `Shallow -> prune_safe_environment !global_env); + | `Shallow -> !global_env); unfreeze_function = (fun fr -> global_env := fr); init_function = (fun () -> global_env := Safe_typing.empty_environment) } |