From 5b432bf03f623b144871181446c68479482abe32 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 14:44:30 +0200
Subject: Deprecate Refiner [evar_map ref] exported functions.

Uses internal to Refiner remain.
---
 proofs/tacmach.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'proofs/tacmach.ml')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 1889054f8..c1d69dfc5 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -33,9 +33,11 @@ let re_sig it  gc = { it = it; sigma = gc; }
 type 'a sigma   = 'a Evd.sigma;;
 type tactic     = Proof_type.tactic;;
 
+[@@@ocaml.warning "-3"]
 let unpackage = Refiner.unpackage
 let repackage = Refiner.repackage
 let apply_sig_tac = Refiner.apply_sig_tac
+[@@@ocaml.warning "+3"]
 
 let sig_it   = Refiner.sig_it
 let project  = Refiner.project
-- 
cgit v1.2.3