diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-18 08:15:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-18 08:15:29 +0000 |
| commit | f418ecb6a2915a8b8b9fd5598ced5376cbcb75bc (patch) | |
| tree | b723d3010efabc8483d4652527f7634324618073 /library/states.mli | |
| parent | 43ee19f32c3ac89c7312b46f13ebdc50b6896b3b (diff) | |
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
Diffstat (limited to 'library/states.mli')
| -rw-r--r-- | library/states.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 *) |