diff options
author | 2013-08-12 13:36:34 +0000 | |
---|---|---|
committer | 2013-08-12 13:36:34 +0000 | |
commit | 7766935322266cb2e01d32e5e2827a6f92bc5078 (patch) | |
tree | f89a40963c67d0bf5bfd5702fae1a6f670b4a533 /toplevel | |
parent | f41f7162a216547b073d4a7f239b14d9379337eb (diff) |
Fixing potentially misused Errors.push.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16699 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/stm.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 52a5bd496..d72b1fd2f 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -454,7 +454,6 @@ end = struct (* {{{ *) let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable) let exn_on id ?valid e = - let e = Errors.push e in let loc = Option.default Loc.ghost (Loc.get_loc e) in let msg = string_of_ppcmds (print e) in Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg)); @@ -1129,6 +1128,7 @@ let process_transaction verbosely (loc, expr) = prerr_endline "executed }}}"; VCS.print () with e -> + let e = Errors.push e in match Stateid.get_state_id e with | None -> VCS.restore vcs; @@ -1136,7 +1136,6 @@ let process_transaction verbosely (loc, expr) = anomaly (str ("execute: "^ string_of_ppcmds (Errors.print_no_report e) ^ "}}}")) | Some (_, id) -> - let e = Errors.push e in prerr_endline ("Failed at state " ^ Stateid.string_of_state_id id); VCS.restore vcs; VCS.print (); |