3 files changed, 5 insertions, 18 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 6e398b61e..ba319fdc0 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -369,11 +369,3 @@ let check_evars env sigma extsigma origsigma =
 let gl_check_evars env sigma extsigma gl =
   let origsigma = gl.sigma in
   check_evars env sigma extsigma origsigma
-
-let tclWITHHOLES accept_unresolved_holes tac sigma c gl =
-  if sigma == project gl then tac c gl
-  else
-    let res = tclTHEN (tclEVARS sigma) (tac c) gl in
-    if not accept_unresolved_holes then
-      gl_check_evars (pf_env gl) (res).sigma sigma gl;
-    res
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 171b008d1..58f9b9617 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -138,9 +138,3 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 (* Check that holes in arguments have been resolved *)
 (* spiwack: used in [tclWITHHOLES] both newer and older copy. *)
 val check_evars : Environ.env -> evar_map -> evar_map -> evar_map -> unit
-
-(** [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which
-   may have unresolved holes; if [solve_holes] these holes must be
-   resolved after application of the tactic; [sigma] must be an
-   extension of the sigma of the goal *)
-val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 35f36f008..c5a6bec95 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1637,11 +1637,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
               (Option.map patt ipat) c)
       end
   | TacGeneralize cl ->
-      Proofview.V82.tactic begin fun gl ->
-        let sigma = project gl in
-        let env = pf_env gl in
+      let tac arg = Proofview.V82.tactic (Tactics.Simple.generalize_gen arg) in
+      Proofview.Goal.raw_enter begin fun gl ->
+        let sigma = Proofview.Goal.sigma gl in
+        let env = Proofview.Goal.env gl in
         let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
-        tclWITHHOLES false (Tactics.Simple.generalize_gen) sigma cl gl
+        Tacticals.New.tclWITHHOLES false tac sigma cl
       end
   | TacGeneralizeDep c ->
       (new_interp_constr ist c)