From f418ecb6a2915a8b8b9fd5598ced5376cbcb75bc Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 18 Sep 2010 08:15:29 +0000 Subject: Fixing bugs #2347 (part 2) and #2388: error message printing was done too late, in a global environment which was no longer the correct one, leading to the failure of error printing (hence an anomaly) in case the command modified the state in several steps. Now, errors raised by vernac commands are processed in the same (intermediate) state they were raised from, just before rolling back to the original state. that modify the state in several Now, errors raised by vernac commands that modify the state in several steps (say S1, S2, ..., Sn) are processed in the state they were produced in (S1, S2, ... Sn-1), git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/states.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/states.mli') diff --git a/library/states.mli b/library/states.mli index 70d139d36..4f114d576 100644 --- a/library/states.mli +++ b/library/states.mli @@ -25,7 +25,7 @@ val unfreeze : state -> unit (** [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 +val with_heavy_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 *) -- cgit v1.2.3