aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tacticals.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 07f9def2c8..374706c8f9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -29,6 +29,8 @@ module NamedDecl = Context.Named.Declaration
type tactic = Proofview.V82.tac
+[@@@ocaml.warning "-3"]
+
let tclIDTAC = Refiner.tclIDTAC
let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE
let tclORELSE0 = Refiner.tclORELSE0