From 1d16c80c53702c3118cc61729a0823d4a9cdaf78 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 May 2020 18:44:32 +0200
Subject: Deprecate the legacy tacticals from module Refiner.

---
 tactics/tacticals.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'tactics')

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
-- 
cgit v1.2.3