From e5b355107d985d7efe2976b9eee9b6c182e25f24 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 12:36:43 +0200
Subject: Remove Refiner.refiner.

---
 proofs/refiner.ml  | 2 --
 proofs/refiner.mli | 2 --
 2 files changed, 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3c6a5d1694..8e413c7a88 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -21,8 +21,6 @@ let project x = x.sigma
 let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
 let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
 
-let refiner = Logic.refiner
-
 (* A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.t Lazy.t
 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 0ea630fdbc..18ac5f4a76 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -22,8 +22,6 @@ val project : 'a sigma -> evar_map
 val pf_env  : Goal.goal sigma -> Environ.env
 val pf_hyps : Goal.goal sigma -> named_context
 
-val refiner : check:bool -> Constr.t -> unit Proofview.tactic
-
 (** A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.t Lazy.t
 
-- 
cgit v1.2.3