Imported Upstream version 8.5~beta1+dfsg

1 files changed, 11 insertions, 8 deletions

diff --git a/library/states.mli b/library/states.mli
index 9474d831..66de1490 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -17,19 +17,22 @@ val intern_state : string -> unit
 val extern_state : string -> unit
 
 type state
-val freeze : unit -> state
+val freeze : marshallable:Summary.marshallable -> state
 val unfreeze : state -> unit
 
-(** {6 Rollback } *)
+val summary_of_state : state -> Summary.frozen
 
-(** [with_heavy_rollback f x] applies [f] to [x] and restores the
-  state of the whole system as it was before the evaluation if an exception
-  is raised. *)
-val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
+(** {6 Rollback } *)
 
 (** [with_state_protection f x] applies [f] to [x] and restores the
-  state of the whole system as it was before the evaluation of f *)
+  state of the whole system as it was before applying [f] *)
 
 val with_state_protection : ('a -> 'b) -> 'a -> 'b
 
+(** [with_state_protection_on_exception f x] applies [f] to [x] and restores the
+  state of the whole system as it was before applying [f] only if an
+  exception is raised.  Unlike [with_state_protection] it also takes into
+  account the proof state *)
+
+val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b