aboutsummaryrefslogtreecommitdiff
path: root/proofs/tacmach.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tacmach.mli')
-rw-r--r--proofs/tacmach.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 717c5212f3..ee80beba8b 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -126,8 +126,10 @@ val tclTHENLIST : tactic list -> tactic
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
val tclTHENL : tactic -> tactic -> tactic
val tclTHENS : tactic -> tactic list -> tactic
+val tclTHENST : tactic -> tactic list -> tactic -> tactic
val tclTHENSI : tactic -> tactic list -> tactic
val tclREPEAT : tactic -> tactic
+val tclREPEAT_MAIN : tactic -> tactic
val tclFIRST : tactic list -> tactic
val tclSOLVE : tactic list -> tactic
val tclTRY : tactic -> tactic