aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/proofview.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/proofview.mli')
-rw-r--r--engine/proofview.mli1
1 files changed, 1 insertions, 0 deletions
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} *)