Removing a use of Goal.refine.

3 files changed, 13 insertions, 46 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index ae6ec558b9..031e1d34ce 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -243,27 +243,6 @@ module Refinable = struct
        many things to go wrong. *)
     handle := fusion delta_list !handle
 
-  (* [constr_of_raw h tycon flags] is a pretyping function.
-      The [tycon] argument allows to put a type constraint on the returned term.
-      The [flags] argument is passed to the pretyper.
-      The principal argument is a [glob_constr] which is then pretyped in the
-      context of a term, the remaining evars are registered to the handle.
-      It is the main component of the toplevel refine tactic.*)
-  (* spiwack: it is not entirely satisfactory to have this function here. Plus it is
-      a bit hackish. However it does not seem possible to move it out until
-      pretyping is defined as some proof procedure. *)
-  let constr_of_raw handle tycon flags lvar rawc = (); fun env rdefs gl info ->
-    (* We need to keep trace of what [rdefs] was originally*)
-    let init_defs = !rdefs in
-    (* call to [understand_tcc_evars] returns a constr with undefined evars
-       these evars will be our new goals *)
-    let (sigma, open_constr) =
-      Pretyping.understand_ltac flags !rdefs env lvar tycon rawc
-    in
-    let () = rdefs := sigma in
-    let () = update_handle handle init_defs !rdefs in
-    open_constr
-
   let constr_of_open_constr handle check_type (evars, c) = (); fun env rdefs gl info ->
     let () = update_handle handle !rdefs evars in
     rdefs := Evd.fold (fun ev evi evd -> if not (Evd.mem !rdefs ev) then Evd.add evd ev evi else evd) evars !rdefs;
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 696c91dc58..9888533828 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -87,16 +87,6 @@ module Refinable : sig
   val resolve_typeclasses : ?filter:Typeclasses.evar_filter -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
 
 
-  (* [constr_of_raw h tycon flags] is a pretyping function.
-      The [tycon] argument allows to put a type constraint on the returned term.
-      The [flags] argument is passed to the pretyper.
-      The principal argument is a [glob_constr] which is then pretyped in the
-      context of a term, the remaining evars are registered to the handle.
-      It is the main component of the toplevel refine tactic.*)
-  val constr_of_raw : handle -> Pretyping.typing_constraint ->
-    Pretyping.inference_flags -> Pretyping.ltac_var_map ->
-    Glob_term.glob_constr -> Term.constr sensitive
-
   (* [constr_of_open_constr h check_type] transforms an open constr into a 
      goal-sensitive constr, adding the undefined variables to the set of subgoals.
      If [check_type] is true, the term is coerced to the conclusion of the goal.
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 6478607444..c681078fa4 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -364,21 +364,19 @@ let refine_red_flags =
 let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences }
 
 let refine_tac {Glob_term.closure=closure;term=term} =
-    let c = Goal.Refinable.make begin fun h ->
-      Goal.bind Goal.concl (fun concl ->
-        let flags = Pretyping.all_no_fail_flags in
-        let tycon = Pretyping.OfType concl in
-        let lvar = { Pretyping.empty_lvar with
-          Pretyping.ltac_constrs = closure.Glob_term.typed;
-          Pretyping.ltac_uconstrs = closure.Glob_term.untyped;
-        } in
-        Goal.Refinable.constr_of_raw h tycon flags lvar term
-      )
-    end in
-    Proofview.Goal.lift c begin fun c ->
-      Proofview.tclSENSITIVE (Goal.refine c) <*>
-      Proofview.V82.tactic (reduce refine_red_flags refine_locs)
-    end
+  Proofview.Goal.enter begin fun gl ->
+    let concl = Proofview.Goal.concl gl in
+    let env = Proofview.Goal.env gl in
+    let flags = Pretyping.all_no_fail_flags in
+    let tycon = Pretyping.OfType concl in
+    let lvar = { Pretyping.empty_lvar with
+      Pretyping.ltac_constrs = closure.Glob_term.typed;
+      Pretyping.ltac_uconstrs = closure.Glob_term.untyped;
+    } in
+    let update evd = Pretyping.understand_ltac flags evd env lvar tycon term in
+    Proofview.Refine.refine_casted (fun h -> Proofview.Refine.update h update) <*>
+    Proofview.V82.tactic (reduce refine_red_flags refine_locs)
+  end
 
 TACTIC EXTEND refine
   [ "refine" uconstr(c) ] -> [  refine_tac c ]