Removing spurious tclWITHHOLES.

Indeed [tclWITHHOLES false tac sigma x] is equivalent to [tclEVARS sigma <*> tac x]
and we should try to reduce the use of this tactical, because it is mostly
a legacy tactic.

4 files changed, 25 insertions, 29 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 179d3622f..cbac5c73a 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -12,6 +12,8 @@ open Util
 open Locus
 open Misctypes
 
+open Proofview.Notations
+
 DECLARE PLUGIN "coretactics"
 
 TACTIC EXTEND reflexivity
@@ -67,7 +69,7 @@ END
 TACTIC EXTEND left_with
   [ "left" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES false (Tactics.left_with_bindings false) sigma bl
+    Proofview.V82.tclEVARS sigma <*> Tactics.left_with_bindings false bl
   ]
 END
 
@@ -91,7 +93,7 @@ END
 TACTIC EXTEND right_with
   [ "right" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES false (Tactics.right_with_bindings false) sigma bl
+    Proofview.V82.tclEVARS sigma <*> Tactics.right_with_bindings false bl
   ]
 END
 
@@ -114,7 +116,7 @@ TACTIC EXTEND constructor
     let { Evd.sigma = sigma; it = bl } = bl in
     let i = Tacinterp.interp_int_or_var ist i in
     let tac c = Tactics.constructor_tac false None i c in
-    Tacticals.New.tclWITHHOLES false tac sigma bl
+    Proofview.V82.tclEVARS sigma <*> tac bl
   ]
 END
 
@@ -138,7 +140,7 @@ TACTIC EXTEND specialize
   [ "specialize" constr_with_bindings(c) ] -> [
     let { Evd.sigma = sigma; it = c } = c in
     let specialize c = Proofview.V82.tactic (Tactics.specialize c) in
-    Tacticals.New.tclWITHHOLES false specialize sigma c
+    Proofview.V82.tclEVARS sigma <*> specialize c
   ]
 END
 
@@ -159,7 +161,7 @@ END
 TACTIC EXTEND split_with
   [ "split" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES false (Tactics.split_with_bindings false) sigma [bl]
+    Proofview.V82.tclEVARS sigma <*> Tactics.split_with_bindings false [bl]
   ]
 END
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ec120f9c6..efe9dde78 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -21,6 +21,7 @@ open Util
 open Evd
 open Equality
 open Misctypes
+open Proofview.Notations
 
 DECLARE PLUGIN "extratactics"
 
@@ -32,17 +33,14 @@ TACTIC EXTEND admit
   [ "admit" ] -> [ admit_as_an_axiom ]
 END
 
-let replace_in_clause_maybe_by (sigma1,c1) c2 cl  tac =
-  Tacticals.New.tclWITHHOLES false
+let replace_in_clause_maybe_by (sigma,c1) c2 cl  tac =
+  Proofview.V82.tclEVARS sigma <*>
     (replace_in_clause_maybe_by c1 c2 cl)
-    sigma1
     (Option.map Tacinterp.eval_tactic tac)
 
 let replace_term dir_opt (sigma,c) cl =
-  Tacticals.New.tclWITHHOLES false
-    (replace_term dir_opt c)
-    sigma
-    cl
+  Proofview.V82.tclEVARS sigma <*>
+    (replace_term dir_opt c) cl
 
 TACTIC EXTEND replace
    ["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
@@ -204,7 +202,7 @@ END
 
 let onSomeWithHoles tac = function
   | None -> tac None
-  | Some c -> Tacticals.New.tclWITHHOLES false tac c.sigma (Some c.it)
+  | Some c -> Proofview.V82.tclEVARS c.sigma <*> tac (Some c.it)
 
 TACTIC EXTEND contradiction
  [ "contradiction" constr_with_bindings_opt(c) ] ->
@@ -248,8 +246,8 @@ END
 
 let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) =
   let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
-  Tacticals.New. tclWITHHOLES false
-    (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings)) sigma true
+  Proofview.V82.tclEVARS sigma <*>
+    general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true
 
 TACTIC EXTEND rewrite_star
 | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index df3115265..afd08026e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1716,7 +1716,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
-        Tacticals.New.tclWITHHOLES false Tactics.intros_patterns sigma l'
+        Proofview.V82.tclEVARS sigma <*> Tactics.intros_patterns l'
       end
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.raw_enter begin fun gl ->
@@ -1808,7 +1808,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
         let tac = Option.map (interp_tactic ist) t in
-        Tacticals.New.tclWITHHOLES false (Tactics.forward b tac ipat) sigma c
+        Proofview.V82.tclEVARS sigma <*> Tactics.forward b tac ipat c
       end
   | TacGeneralize cl ->
       let tac arg = Proofview.V82.tactic (Tactics.Simple.generalize_gen arg) in
@@ -1816,7 +1816,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         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
-        Tacticals.New.tclWITHHOLES false tac sigma cl
+        Proofview.V82.tclEVARS sigma <*> tac cl
       end
   | TacGeneralizeDep c ->
       (new_interp_constr ist c)
@@ -1838,9 +1838,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
             let with_eq = if b then None else Some (true,id) in
             Tactics.letin_tac with_eq na c None cl
           in
-	  Tacticals.New.tclWITHHOLES false
-            (let_tac b (interp_fresh_name ist env na) c_interp clp)
-            sigma eqpat
+	  Proofview.V82.tclEVARS sigma <*>
+            let_tac b (interp_fresh_name ist env na) c_interp clp eqpat
         else
         (* We try to keep the pattern structure as much as possible *)
           let let_pat_tac b na c cl eqpat =
@@ -1848,9 +1847,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
             let with_eq = if b then None else Some (true,id) in
             Tactics.letin_pat_tac with_eq na c cl
           in
-	  Tacticals.New.tclWITHHOLES false
-            (let_pat_tac b (interp_fresh_name ist env na)
-            (interp_pure_open_constr ist env sigma c) clp) sigma eqpat
+          let_pat_tac b (interp_fresh_name ist env na)
+            (interp_pure_open_constr ist env sigma c) clp eqpat
       end
 
   (* Automation tactics *)
@@ -2024,7 +2022,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in
         let sigma,ids = interp_or_and_intro_pattern_option ist env sigma ids in
-        Tacticals.New.tclWITHHOLES false (Inv.dinv k c_interp ids) sigma dqhyps
+        Proofview.V82.tclEVARS sigma <*> Inv.dinv k c_interp ids dqhyps
       end
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       Proofview.Goal.raw_enter begin fun gl ->
@@ -2033,8 +2031,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let hyps = interp_hyp_list ist env idl in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in
         let sigma, ids = interp_or_and_intro_pattern_option ist env sigma ids in
-        Tacticals.New.tclWITHHOLES false (Inv.inv_clause k ids hyps)
-          sigma dqhyps
+        Proofview.V82.tclEVARS sigma <*> Inv.inv_clause k ids hyps dqhyps
       end
   | TacInversion (InversionUsing (c,idl),hyp) ->
       Proofview.Goal.raw_enter begin fun gl ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7e6e960a6..5123aed9c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1807,12 +1807,11 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let sigma,c = f env sigma in
-        Tacticals.New.tclWITHHOLES false
+        Proofview.V82.tclEVARS sigma <*>
           (Tacticals.New.tclTHENFIRST
              (* Skip the side conditions of the apply *)
              (apply_in_once false true true true (Some (clear,naming)) id
                 (None,(sigma,(c,NoBindings))) tac_ipat))
-          sigma
 	  (tac thin None [])
       end