diff options
Diffstat (limited to 'library/states.mli')
| -rw-r--r-- | library/states.mli | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/library/states.mli b/library/states.mli index 782e41ca7..fb11756e5 100644 --- a/library/states.mli +++ b/library/states.mli @@ -1,14 +1,15 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*s States of the system. In that module, we provide functions to get +(** {6 Sect } *) +(** 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. *) @@ -20,13 +21,15 @@ type state val freeze : unit -> state val unfreeze : state -> unit -(*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the +(** {6 Sect } *) +(** 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 [with_state_protection f x] applies [f] to [x] and restores the +(** {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 *) val with_state_protection : ('a -> 'b) -> 'a -> 'b |