From 821937aee71bf9439158e27e06f7b4f74289b209 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 16:57:31 +0200
Subject: STM: proof block detection made optional + simple test

---
 lib/flags.ml  | 2 ++
 lib/flags.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index c1ec9738ca..ecf3c3f168 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -68,6 +68,8 @@ let priority_of_string = function
   | "low" -> Low
   | "high" -> High
   | _ -> raise (Invalid_argument "priority_of_string")
+let async_proofs_tac_error_resilience = ref true
+let async_proofs_cmd_error_resilience = ref true
 
 let async_proofs_is_worker () =
   !async_proofs_worker_id <> "master"
diff --git a/lib/flags.mli b/lib/flags.mli
index 24780f0dcc..b26ef027c6 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,6 +34,8 @@ type priority = Low | High
 val async_proofs_worker_priority : priority ref
 val string_of_priority : priority -> string
 val priority_of_string : string -> priority
+val async_proofs_tac_error_resilience : bool ref
+val async_proofs_cmd_error_resilience : bool ref
 
 val debug : bool ref
 val in_debugger : bool ref
-- 
cgit v1.2.3