diff options
Diffstat (limited to 'library/states.mli')
| -rw-r--r-- | library/states.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/library/states.mli b/library/states.mli index f0dab29f2..9b5872bde 100644 --- a/library/states.mli +++ b/library/states.mli @@ -6,8 +6,9 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {6 Sect } *) -(** States of the system. In that module, we provide functions to get +(** {6 States of the system} *) + +(** In that module, we provide functions to get and set the state of the whole system. Internally, it is done by freezing the states of both [Lib] and [Summary]. We provide functions to write and restore state to and from a given file. *) @@ -19,14 +20,13 @@ type state val freeze : unit -> state val unfreeze : state -> unit -(** {6 Sect } *) -(** Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the +(** {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. *) - val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b -(** {6 Sect } *) (** [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 *) |