Moving the remaining Refiner functions to Tacmach.

3 files changed, 4 insertions, 27 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 8e413c7a88..cd44b2ae71 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -9,17 +9,6 @@
 (************************************************************************)
 
 open Util
-open Evd
-
-type tactic = Proofview.V82.tac
-
-let sig_it x = x.it
-let project x = x.sigma
-
-(* Getting env *)
-
-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))
 
 (* 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 18ac5f4a76..e13e358d8f 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -10,18 +10,6 @@
 
 (** Legacy proof engine. Do not use in newly written code. *)
 
-open Evd
-open EConstr
-
-(** The refiner (handles primitive rules and high-level tactics). *)
-type tactic = Proofview.V82.tac
-
-val sig_it  : 'a sigma -> 'a
-val project : 'a sigma -> evar_map
-
-val pf_env  : Goal.goal sigma -> Environ.env
-val pf_hyps : Goal.goal sigma -> named_context
-
 (** A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.t Lazy.t
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 0bac0b0424..ecdbfa5118 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -29,10 +29,10 @@ let re_sig it  gc = { it = it; sigma = gc; }
 
 type tactic = Proofview.V82.tac
 
-let sig_it   = Refiner.sig_it
-let project  = Refiner.project
-let pf_env   = Refiner.pf_env
-let pf_hyps  = Refiner.pf_hyps
+let sig_it x = x.it
+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 test_conversion env sigma pb c1 c2 =
   Reductionops.check_conv ~pb env sigma c1 c2