From 17f2b11a9a6bb39379239122e77ec12d0b96ff63 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 12 May 2015 14:19:13 +0200
Subject: nice error for Restart outside a proof (Close: #4235)

---
 stm/stm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 9771564752..97903e721b 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
-- 
cgit v1.2.3