From 020aa7a8e9bca88631e6d7fa68d1ff462f5af25a Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Fri, 18 Oct 2013 13:52:10 +0000 Subject: 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 --- kernel/safe_typing.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index a56bb8578..b16d5b63d 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -43,8 +43,6 @@ 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 -(* future computations are just dropped by this function *) -val prune_safe_environment : safe_environment -> safe_environment (** {6 Enriching a safe environment } *) -- cgit v1.2.3