Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.

Most of the code from Goal.Refine and related was moved to the one
file that was using it, wiz. tactics.ml. Some additional care should
be taken to clean up even more the remaining code.

1 files changed, 39 insertions, 2 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f14810482..d06d78165 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4203,6 +4203,38 @@ module Simple = struct
 
 end
 
+
+(* [with_type c typ] constrains term [c] to have type [typ].  *)
+let with_type t typ env sigma =
+  (* spiwack: this function assumes that no evars can be created during
+      this sort of coercion.
+      If it is not the case it could produce bugs. We would need to add a handle
+      and add the new evars to it. *)
+  let my_type = Retyping.get_type_of env sigma t in
+  let j = Environ.make_judge t my_type in
+  let (sigma, j') =
+    Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j typ
+  in
+  (sigma, j'.Environ.uj_val)
+
+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
+  with_type c concl env sigma
+
+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 = List.map Goal.build (Evar.Set.elements !handle) in
+  (subgoals, pf, sigma)
+
 (** Tacticals defined directly in term of Proofview *)
 module New = struct
   open Proofview.Notations
@@ -4214,8 +4246,13 @@ module New = struct
 
   let refine c =
     Proofview.Goal.nf_enter begin fun gl ->
-    let pf = Goal.refine_open_constr c in
-    Proofview.tclSENSITIVE pf <*>
+    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 }