diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 26 |
1 files changed, 12 insertions, 14 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 32c6c7d959..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 | _ -> @@ -2017,7 +2016,7 @@ end = struct (* {{{ *) find ~time:false ~batch:false ~fail:false e in let st = Vernacstate.freeze_interp_state ~marshallable:false in Vernacentries.with_fail st fail (fun () -> - (if time then System.with_time ~batch else (fun x -> x)) (fun () -> + (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> let Proof.{goals} = Proof.data p in @@ -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 @@ -2993,7 +2984,14 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Unknown: we execute it, check for open goals and propagate sideeff *) | VtUnknown, VtNow -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in - let id = VCS.new_node ~id:newtip () in + if not (get_allow_nested_proofs ()) && in_proof then + "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on." + |> Pp.str + |> (fun s -> (UserError (None, s), Exninfo.null)) + |> State.exn_on ~valid:Stateid.dummy Stateid.dummy + |> Exninfo.iraise + else + let id = VCS.new_node ~id:newtip () in let head_id = VCS.get_branch_pos head in let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) let step () = |