Remove the deprecated open-constr based refine.

That is [Tactics.New.refine]. Replaced it with a wrapper around the primitive refine [Proofview.Refine.refine], but with extra reductions on the resulting goals.

There was two used of this refine: one in the declarative mode, and one in type classes. The porting of the latter is likely to have introduced bugs.

Factored code with Ltac's refine in Extratactics.

4 files changed, 14 insertions, 54 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f8bca11558..1e6caca57e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -759,10 +759,6 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl
       eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
    with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl
 
-let _ = Classes.refine_ref := begin fun c ->
-  Tactics.New.refine c
-end
-
 (** Take the head of the arity of a constr.
     Used in the partial application tactic. *)
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e0995096fc..71d766e123 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -349,18 +349,6 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
-
-let refine_red_flags =
-  Genredexpr.Lazy {
-    Genredexpr.rBeta=true;
-    rIota=true;
-    rZeta=false;
-    rDelta=false;
-    rConst=[];
-  }
-
-let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences }
-
 let refine_tac {Glob_term.closure=closure;term=term} =
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
@@ -373,8 +361,7 @@ let refine_tac {Glob_term.closure=closure;term=term} =
       Pretyping.ltac_idents = closure.Glob_term.idents;
     } in
     let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in
-    Proofview.Refine.refine ~unsafe:false update <*>
-    Proofview.V82.tactic (reduce refine_red_flags refine_locs)
+    Tactics.New.refine ~unsafe:false update
   end
 
 TACTIC EXTEND refine
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d304071195..ea40fe4b90 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4196,24 +4196,6 @@ module Simple = struct
 end
 
 
-let update_handle handle init_defs post_defs =
-  let filter ev _ = not (Evd.mem init_defs ev) in
-  let fold ev evi accu = if filter ev evi then Evar.Set.add ev accu else accu in
-  Evd.fold_undefined fold post_defs handle
-
-let constr_of_open_constr handle (evars, c) env sigma concl =
-  let () = handle := update_handle !handle sigma evars in
-  let fold ev evi evd = if not (Evd.mem sigma ev) then Evd.add evd ev evi else evd in
-  let sigma = Evd.fold fold evars sigma in
-  Proofview.Refine.with_type env sigma c concl
-
-let refine_open_constr c env sigma concl =
-  let handle = ref Evar.Set.empty in
-  let sigma, pf = constr_of_open_constr handle c env sigma concl in
-  let sigma = Evarconv.consider_remaining_unif_problems env sigma in
-  let subgoals = Evar.Set.elements !handle in
-  (subgoals, pf, sigma)
-
 (** Tacticals defined directly in term of Proofview *)
 module New = struct
   open Proofview.Notations
@@ -4223,19 +4205,12 @@ module New = struct
   open Genredexpr
   open Locus
 
-  let refine c =
-    Proofview.Goal.nf_enter begin fun gl ->
-    let env = Proofview.Goal.env gl in
-    let sigma = Proofview.Goal.sigma gl in
-    let concl = Proofview.Goal.concl gl in
-    let (gls, pf, sigma) = refine_open_constr c env sigma concl in
-    Proofview.V82.tclEVARS sigma <*>
-    Proofview.Refine.refine ~unsafe:true (fun h -> (h, pf)) <*>
-    Proofview.tclNEWGOALS gls <*>
-      Proofview.V82.tactic (reduce
-         (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]})
-         {onhyps=None; concl_occs=AllOccurrences }
-      )
-    end
+  let reduce_after_refine =
+    Proofview.V82.tactic (reduce
+      (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]})
+      {onhyps=None; concl_occs=AllOccurrences })
 
+  let refine ?unsafe c =
+    Proofview.Refine.refine ?unsafe c <*>
+    reduce_after_refine
 end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e724f675e1..a4fb6dd887 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -436,10 +436,12 @@ end
 
 module New : sig
 
-  val refine : Evd.open_constr -> unit Proofview.tactic
-  (** DEPRECATED. Legacy refine tactic. You should not be using this code, as
-      it may be unsound to manipulate evar maps without care. Use the
-      [Proofview.Refine] module instead. *)
+  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*constr) -> unit Proofview.tactic
+  (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c]
+      followed by beta-iota-reduction of the conclusion. *)
+
+  val reduce_after_refine : unit Proofview.tactic
+  (** The reducing tactic called after {!refine}. *)
 
   open Proofview
   val exact_proof : Constrexpr.constr_expr -> unit tactic