From f30822ba46d08d65597e0e3230ea6ad86c98453f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 7 Nov 2016 16:03:53 +0100
Subject: Proofview: tclINDEPENDENTL

---
 engine/proofview.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/proofview.mli')

diff --git a/engine/proofview.mli b/engine/proofview.mli
index 90be2f90a..294b03dca 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -292,6 +292,7 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact
     independent of backtracking in another. It is equivalent to
     [tclEXTEND [] tac []]. *)
 val tclINDEPENDENT : unit tactic -> unit tactic
+val tclINDEPENDENTL: 'a tactic -> 'a list tactic
 
 
 (** {7 Goal manipulation} *)
-- 
cgit v1.2.3