diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 15 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
2 files changed, 4 insertions, 13 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 4a1e64eb4a..169d608d2d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -869,7 +869,6 @@ end = struct (* {{{ *) cur_id := id | { state = Error ie } -> - cur_id := id; Exninfo.iraise ie | _ -> @@ -2832,17 +2831,9 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs = - match Stateid.get info with - | None -> - VCS.restore vcs; - VCS.print (); - anomaly(str"error with no safe_id attached:" ++ spc() ++ - CErrors.iprint_no_report (e, info) ++ str".") - | Some (safe_id, id) -> - stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); - VCS.restore vcs; - VCS.print (); - Exninfo.iraise (e, info) + VCS.restore vcs; + VCS.print (); + Exninfo.iraise (e, info) let snapshot_vio ~doc ldir long_f_dot_vo = let doc = finish ~doc in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f40b3e901b..454a4b66e7 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -214,6 +214,6 @@ let classify_vernac e = | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow - | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + | (VtStartProof _ | VtUnknown), _ -> VtQuery, VtLater) in static_control_classifier e |