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.

---
 plugins/ltac/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/tacinterp.ml')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index dda7f0742c..a8bb97c774 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1087,7 +1087,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacShowHyps tac ->
          Proofview.V82.tactic begin
            tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
-         end
+         end [@ocaml.warning "-3"]
   | TacAbstract (t,ido) ->
       let call = LtacMLCall tac in
       let trace = push_trace(None,call) ist in
-- 
cgit v1.2.3