with_heavy_rollback deplace dans States

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

4 files changed, 22 insertions, 20 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 470c85674..07d4049ce 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -186,16 +186,3 @@ let init () =
   add_frozen_state ();
   path_prefix := []
 
-
-(* Rollback. *)
-
-let with_heavy_rollback f x =
-  let sum = freeze_summaries ()
-  and flib = freeze() in
-  try 
-    f x
-  with reraise -> begin
-    unfreeze_summaries sum;
-    unfreeze flib;
-    raise reraise
-  end
diff --git a/library/lib.mli b/library/lib.mli
index 33f6e9056..d8b3def29 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -48,13 +48,6 @@ val export_module : unit -> library_segment
 val reset_to : section_path -> unit
 
 
-(*s 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. *)
-
-val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
-
-
 (*s We can get and set the state of the operations (used in [States]). *)
 
 type frozen
diff --git a/library/states.ml b/library/states.ml
index 2e198e36f..d8fed1437 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -20,3 +20,16 @@ let (extern_state,intern_state) =
   let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
   (fun s -> raw_extern s (get_state())),
   (fun s -> set_state (raw_intern s))
+
+(* Rollback. *)
+
+let with_heavy_rollback f x =
+  let sum = freeze_summaries ()
+  and flib = freeze() in
+  try 
+    f x
+  with reraise -> begin
+    unfreeze_summaries sum;
+    unfreeze flib;
+    raise reraise
+  end
diff --git a/library/states.mli b/library/states.mli
index 06a877802..d648a68ce 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -1,8 +1,17 @@
 
 (* $Id$ *)
 
+(*s States of the system. *)
+
 type state
 
 val intern_state : string -> unit
 val extern_state : string -> unit
 
+(*s 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. *)
+
+val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
+
+