From eb3e8efaaafd0de673184db85b9b647cfa24dd92 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 27 Feb 2015 17:18:16 +0100
Subject: STM: Considering Stack_overflow as a normal tactic error (Close
 #3576)

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

diff --git a/stm/stm.ml b/stm/stm.ml
index 5edf480446..b38407c045 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1067,7 +1067,7 @@ end = struct (* {{{ *)
       ignore(Future.join checked_proof);
       RespBuiltProof(proof,time)
     with
-    | e when Errors.noncritical e ->
+    | e when Errors.noncritical e || e = Stack_overflow ->
         let (e, info) = Errors.push e in
         (* This can happen if the proof is broken.  The error has also been
          * signalled as a feedback, hence we can silently recover *)
-- 
cgit v1.2.3