From 178672504f1c92b162c2575b14034cc7b698b6a4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Feb 2019 18:29:40 +0100
Subject: [vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.

We try to do a bit of cleanup for the `with_fail` function, this still
is delicate code.
---
 stm/stm.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index c11f8d86e6..cc0de0e9df 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2064,6 +2064,12 @@ end = struct (* {{{ *)
 
   module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) ()
 
+  let stm_fail ~st fail f =
+    if fail then
+      Vernacentries.with_fail ~st f
+    else
+      f ()
+
   let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
     { indentation; verbose; loc; expr = e; strlen } : unit
   =
@@ -2075,7 +2081,7 @@ end = struct (* {{{ *)
         | e -> e, time, batch, fail in
       find ~time:false ~batch:false ~fail:false e in
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
-    Vernacstate.Proof_global.with_fail ~st (fun () ->
+    stm_fail ~st fail (fun () ->
     (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Vernacstate.Proof_global.with_current_proof (fun _ p ->
-- 
cgit v1.2.3