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.

7 files changed, 34 insertions, 67 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 470dc9d9cc..9d64efdeda 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1270,17 +1270,17 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
     | End_patt (_,_) , _ :: _  ->
 	anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left")
 
-let understand_my_constr c gls =
-  let env = pf_env gls in
+let understand_my_constr env sigma c concl =
+  let env = env in
   let rawc = Detyping.detype false [] env Evd.empty c in
   let rec frob = function
     | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None)
     | rc ->  map_glob_constr frob rc
   in
-  Pretyping.understand_tcc env (sig_sig gls) ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc)
+  Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc)
 
 let my_refine c gls =
-  let oc = understand_my_constr c gls in
+  let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
   Proofview.V82.of_tactic (Tactics.New.refine oc) gls
 
 (* end focus/claim *)
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
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index e034d06740..e49857be37 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -75,8 +75,6 @@ let type_ctx_instance evars env ctx inst subst =
     | [] -> subst
   in aux (subst, []) inst (List.rev ctx)
 
-let refine_ref = ref (fun _ -> assert(false))
-
 let id_of_class cl =
   match cl.cl_impl with
     | ConstRef kn -> let _,_,l = repr_con kn in Label.to_id l
@@ -295,12 +293,25 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	    else
 	      (Flags.silently 
 	       (fun () ->
-		Lemmas.start_proof id kind (Evd.from_env ~ctx:(Evd.evar_universe_context evm) Environ.empty_env) termtype
+                  (* spiwack: it is hard to reorder the actions to do
+                     the pretyping after the proof has opened. As a
+                     consequence, we use the low-level primitives to code
+                     the refinement manually.*)
+		let gls = Evd.future_goals evm in
+                let evm = Evd.reset_future_goals evm in
+                Lemmas.start_proof id kind evm termtype
 		(Lemmas.mk_hook
                   (fun _ -> instance_hook k pri global imps ?hook));
                  (* spiwack: I don't know what to do with the status here. *)
-		if not (Option.is_empty term) then 
-		  ignore (Pfedit.by (!refine_ref (evm, Option.get term)))
+		if not (Option.is_empty term) then
+                  let init_refine =
+                    Tacticals.New.tclTHENLIST [
+                      Proofview.Refine.refine (fun evm -> evm, Option.get term);
+                      Proofview.tclNEWGOALS gls;
+                      Tactics.New.reduce_after_refine;
+                    ]
+                  in
+		  ignore (Pfedit.by init_refine)
 		else if Flags.is_auto_intros () then
 		  ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro));
 		(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ();
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index f0932c8260..cddf629d9b 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -64,7 +64,3 @@ val id_of_class : typeclass -> Id.t
 (** returns [false] if, for lack of section, it declares an assumption
     (unless in a module type). *)
 val context : Decl_kinds.polymorphic -> local_binder list -> bool
-
-(** Forward ref for refine *)
-
-val refine_ref : (open_constr -> unit Proofview.tactic) ref