aboutsummaryrefslogtreecommitdiffhomepage
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, 1 insertions, 0 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 09964a331..52a12a23d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -36,6 +36,7 @@ open Tacexpr
(*************************************************)
let tclIDTAC = tclIDTAC
+let tclIDTAC_MESSAGE = tclIDTAC_MESSAGE
let tclORELSE = tclORELSE
let tclTHEN = tclTHEN
let tclTHENLIST = tclTHENLIST