Moving the remaining Refiner functions to Tacmach.

9 files changed, 12 insertions, 37 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index bca1eb5754..f14edec639 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -186,7 +186,7 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoalgoal gl = pp(Goal.pr_goal gl)
 let ppgoal g = pp(Printer.pr_goal g)
-let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Refiner.project g))
+let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Tacmach.project g))
 let pphintdb db = pp(envpp Hints.pr_hint_db_env db)
 let ppproofview p =
   let gls,sigma = Proofview.proofview p in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e7c75e029e..878f7a834e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -201,7 +201,7 @@ let exec_tactic env evd n f args =
   (* Evaluate the whole result *)
   let gl = dummy_goal env evd in
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
-  let evd = Evd.minimize_universes (Refiner.project gls) in
+  let evd = Evd.minimize_universes gls.Evd.sigma in
   let nf c = constr_of evd c in
   Array.map nf !tactic_res, Evd.universe_context_set evd
 
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5c25db1a82..5f463f8de4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -748,7 +748,7 @@ let pf_abs_cterm gl n c0 = abs_cterm (pf_env gl) (project gl) n c0
 (* }}} *)
 
 let pf_merge_uc uc gl =
-  re_sig (sig_it gl) (Evd.merge_universe_context (Refiner.project gl) uc)
+  re_sig (sig_it gl) (Evd.merge_universe_context gl.Evd.sigma uc)
 let pf_merge_uc_of sigma gl =
   let ucst = Evd.evar_universe_context sigma in
   pf_merge_uc ucst gl
diff --git a/printing/printer.ml b/printing/printer.ml
index 2ad9e268c2..37b8b244a3 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -16,7 +16,6 @@ open Constr
 open Context
 open Environ
 open Evd
-open Refiner
 open Constrextern
 open Ppconstr
 open Declarations
@@ -421,7 +420,7 @@ let pr_transparent_state ts =
  *)
 let pr_goal ?(diffs=false) ?og_s g_s =
   let g = sig_it g_s in
-  let sigma = project g_s in
+  let sigma = Tacmach.project g_s in
   let env = Goal.V82.env sigma g in
   let concl = Goal.V82.concl sigma g in
   let goal =
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index c78cc96a83..43f70dfecc 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -335,7 +335,7 @@ let unwrap g_s =
   match g_s with
   | Some g_s ->
     let goal = Evd.sig_it g_s in
-    let sigma = Refiner.project g_s in
+    let sigma = Tacmach.project g_s in
     goal_info goal sigma
   | None -> ([], CString.Map.empty, Pp.mt ())
 
@@ -545,7 +545,7 @@ let match_goals ot nt =
 
 let get_proof_context (p : Proof.t) =
   let Proof.{goals; sigma} = Proof.data p in
-  sigma, Refiner.pf_env { Evd.it = List.(hd goals); sigma }
+  sigma, Tacmach.pf_env { Evd.it = List.(hd goals); sigma }
 
 let to_constr pf =
   let open CAst in
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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index eb7f2190a8..af23747d43 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -30,7 +30,6 @@ open Genredexpr
 open Tacmach.New
 open Logic
 open Clenv
-open Refiner
 open Tacticals
 open Hipattern
 open Coqlib
@@ -355,7 +354,7 @@ let fresh_id_in_env avoid id env =
   next_ident_away_in_goal id avoid
 
 let fresh_id avoid id gl =
-  fresh_id_in_env avoid id (pf_env gl)
+  fresh_id_in_env avoid id (Tacmach.pf_env gl)
 
 let new_fresh_id avoid id gl =
   fresh_id_in_env avoid id (Proofview.Goal.env gl)
@@ -1007,7 +1006,7 @@ let find_intro_names ctxt gl =
       let name = fresh_id avoid (default_id env gl.sigma decl) gl in
       let newenv = push_rel decl env in
       (newenv, name :: idl, Id.Set.add name avoid))
-    ctxt (pf_env gl, [], Id.Set.empty) in
+    ctxt (Tacmach.pf_env gl, [], Id.Set.empty) in
   List.rev res
 
 let build_intro_tac id dest tac = match dest with