From 43343c1f79d9f373104ae5174baf41e2257e2b8d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 May 2016 11:02:58 +0200
Subject: Removing the old refine tactic from the Tactics module.

It is indeed confusing, as it has little to do with the proper refine defined
in the New submodule. Legacy code relying on it should call the Logic or
Tacmach modules instead.
---
 plugins/decl_mode/decl_proof_instr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index de06af0053..be6ce59bd3 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -485,7 +485,7 @@ let thus_tac c ctyp submetas gls =
     Proofview.V82.of_tactic (exact_check proof) gls
   else
     let refiner = concl_refiner list proof gls in
-      Tactics.refine refiner gls
+      Tacmach.refine refiner gls
 
 (* general forward step *)
 
-- 
cgit v1.2.3