summaryrefslogtreecommitdiff
path: root/tactics/tacticals.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacticals.ml')
-rw-r--r--tactics/tacticals.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 11625cbd..b82f1fca 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -53,7 +53,6 @@ let tclREPEAT_MAIN = Refiner.tclREPEAT_MAIN
let tclFIRST = Refiner.tclFIRST
let tclSOLVE = Refiner.tclSOLVE
let tclTRY = Refiner.tclTRY
-let tclINFO = Refiner.tclINFO
let tclCOMPLETE = Refiner.tclCOMPLETE
let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
let tclFAIL = Refiner.tclFAIL