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 /toplevel/vernac.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 'toplevel/vernac.mli')
-rw-r--r-- | toplevel/vernac.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 767c53063..d89e90d0c 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -22,7 +22,6 @@ exception End_of_input val just_parsing : bool ref val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit -val eval_ctrl : Vernacexpr.vernac_expr -> unit val raw_do_vernac : Pcoq.Gram.parsable -> unit (** Set XML hooks *) |