From 73ddce3136549532c81405fa82871dcd3a51b28f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 26 Mar 2014 20:37:40 +0100
Subject: Adding a tclEFFECTS primitive allowing to push STM side-effects in
 tactics.

---
 proofs/proofview.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'proofs/proofview.mli')

diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 7be8f6003..409bbb76a 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -234,6 +234,9 @@ val tclEVARMAP : Evd.evar_map tactic
    environment is returned by {!Proofview.Goal.env}. *)
 val tclENV : Environ.env tactic
 
+(* [tclEFFECTS eff] add the effects [eff] to the current state. *)
+val tclEFFECTS : Declareops.side_effects -> unit tactic
+
 (* Shelves all the goals under focus. The goals are placed on the
    shelf for later use (or being solved by side-effects). *)
 val shelve : unit tactic
-- 
cgit v1.2.3