From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- library/states.mli | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) (limited to 'library/states.mli') diff --git a/library/states.mli b/library/states.mli index 12c71c99..1e0361ea 100644 --- a/library/states.mli +++ b/library/states.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Summary.frozen -> state 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 - -- cgit v1.2.3