aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/refiner.mli')
-rw-r--r--proofs/refiner.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index de6502dc3..e179589df 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -119,7 +119,6 @@ val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> Pp.std_ppcmds -> tactic
val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclSHOWHYPS : tactic -> tactic