diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-05 11:22:26 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-05 12:53:46 +0100 |
| commit | 2c0f1eb6f9a6e16b2b4d3a99542df7f49c81f6ea (patch) | |
| tree | 4b6fb7d347faf46d5a7c51637fefd79b85396bd3 /stm | |
| parent | 5bb1120292b7d0497d04c36631bf49239aa6ddf4 (diff) | |
Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)
Here nonsensical means a Qed/Defined without a Lemma.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 7b2468548..05c59720b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1863,7 +1863,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 -let merge_proof_branch ?id qast keep brname = +let merge_proof_branch ?valid ?id qast keep brname = let brinfo = VCS.get_branch brname in let qed fproof = { qast; keep; brname; brinfo; fproof } in match brinfo with @@ -1886,7 +1886,7 @@ let merge_proof_branch ?id qast keep brname = VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> - iraise (State.exn_on Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) + iraise (State.exn_on ?valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) @@ -2044,7 +2044,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = VCS.commit id (Cmd {cast = x; cids = []; cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> - let rc = merge_proof_branch ~id:newtip x keep head in + let valid = if tty then Some(VCS.get_branch_pos head) else None in + let rc = merge_proof_branch ?valid ~id:newtip x keep head in VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); rc |