Adding a primitive to the tactic monad to modify the exceptional content.

1 files changed, 8 insertions, 0 deletions

diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 79bf48acd..c88de133d 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -215,6 +215,14 @@ struct
   let modify f =
     { iolist = fun s nil cons -> cons () (f s) nil }
 
+  (** Exception manipulation *)
+
+  let interleave src dst m =
+    { iolist = fun s nil cons ->
+      m.iolist s (fun e1 -> nil (src e1))
+        (fun x s next -> cons x s (fun e2 -> next (dst e2)))
+    }
+
   (** List observation *)
 
   let once m =