Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.

1 files changed, 6 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 67893e3b78..ae4b2e3363 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -555,6 +555,12 @@ let tclEVARMAP =
 
 let tclENV = Proof.current
 
+let tclEFFECTS eff =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun initial ->
+  Proof.set (emit_side_effects eff initial)
+
 exception Timeout
 let _ = Errors.register_handler begin function
   | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")