diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-05-12 14:19:13 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-05-12 14:19:13 +0200 |
commit | 17f2b11a9a6bb39379239122e77ec12d0b96ff63 (patch) | |
tree | b705275f5f8381b7360f4e71c62e6201e5bede53 | |
parent | 0803c2dd715e6493c3e4f865bcf9ca2a16318c55 (diff) |
nice error for Restart outside a proof (Close: #4235)
-rw-r--r-- | stm/stm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 977156475..97903e721 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -846,7 +846,8 @@ end = struct (* {{{ *) | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup") | Some vcs, _ -> vcs in let cb, _ = - Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in + try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) + with Failure _ -> raise Proof_global.NoCurrentProof in let n = fold_until (fun n (_,vcs,_,_,_) -> if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) 0 id in |