coqtop -compile: avoid with_heavy_rollback when non-interactive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16444 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 5 deletions

diff --git a/library/states.mli b/library/states.mli
index 7e6535d92..26dec09e5 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -22,14 +22,20 @@ val unfreeze : state -> unit
 
 (** {6 Rollback } *)
 
-(** [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. *)
+(** [with_heavy_rollback f h x] applies [f] to [x]. If this application
+    ends on an exception, the wrapper [h] is applied to it, then
+    the state of the whole system is restored as it was before applying [f],
+    and finally the exception produced by [h] is raised. *)
+
 val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
 
+(** [without_rollback] is just like [with_heavy_rollback], except that
+    no state is restored in case of exception. *)
+
+val without_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
+
 (** [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
 
-