From aae3c3b42a9bad20ebde4a139e6de660fbb8e042 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 15 Aug 2014 14:03:11 +0200
Subject: Removing unused Refiner.tclWITHHOLES.

---
 tactics/tacinterp.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 35f36f0089..c5a6bec959 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)
-- 
cgit v1.2.3