Revert "Removing spurious tclWITHHOLES."

This reverts commit 36c7fba1180eaa2ceea7cc486ebd2f0d649042f0.

I had mixed up the boolean flag, resulting in the loss of evar-free
versions of tactics.

4 files changed, 35 insertions, 34 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 5c039e72c..183611659 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -71,7 +71,7 @@ END
 TACTIC EXTEND left_with
   [ "left" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Proofview.Unsafe.tclEVARS sigma <*> Tactics.left_with_bindings false bl
+    Tacticals.New.tclWITHHOLES false (Tactics.left_with_bindings false) sigma bl
   ]
 END
 
@@ -95,7 +95,7 @@ END
 TACTIC EXTEND right_with
   [ "right" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Proofview.Unsafe.tclEVARS sigma <*> Tactics.right_with_bindings false bl
+    Tacticals.New.tclWITHHOLES false (Tactics.right_with_bindings false) sigma bl
   ]
 END
 
@@ -118,7 +118,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
-    Proofview.Unsafe.tclEVARS sigma <*> tac bl
+    Tacticals.New.tclWITHHOLES false tac sigma bl
   ]
 END
 
@@ -142,7 +142,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
-    Proofview.Unsafe.tclEVARS sigma <*> specialize c
+    Tacticals.New.tclWITHHOLES false specialize sigma c
   ]
 END
 
@@ -163,7 +163,7 @@ END
 TACTIC EXTEND split_with
   [ "split" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Proofview.Unsafe.tclEVARS sigma <*> Tactics.split_with_bindings false [bl]
+    Tacticals.New.tclWITHHOLES false (Tactics.split_with_bindings false) sigma [bl]
   ]
 END
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f3482c310..063b425ba 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -21,7 +21,6 @@ open Util
 open Evd
 open Equality
 open Misctypes
-open Proofview.Notations
 
 DECLARE PLUGIN "extratactics"
 
@@ -33,14 +32,17 @@ TACTIC EXTEND admit
   [ "admit" ] -> [ admit_as_an_axiom ]
 END
 
-let replace_in_clause_maybe_by (sigma,c1) c2 cl  tac =
-  Proofview.Unsafe.tclEVARS sigma <*>
+let replace_in_clause_maybe_by (sigma1,c1) c2 cl  tac =
+  Tacticals.New.tclWITHHOLES false
     (replace_in_clause_maybe_by c1 c2 cl)
+    sigma1
     (Option.map Tacinterp.eval_tactic tac)
 
 let replace_term dir_opt (sigma,c) cl =
-  Proofview.Unsafe.tclEVARS sigma <*>
-    (replace_term dir_opt c) cl
+  Tacticals.New.tclWITHHOLES false
+    (replace_term dir_opt c)
+    sigma
+    cl
 
 TACTIC EXTEND replace
    ["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
@@ -202,7 +204,7 @@ END
 
 let onSomeWithHoles tac = function
   | None -> tac None
-  | Some c -> Proofview.Unsafe.tclEVARS c.sigma <*> tac (Some c.it)
+  | Some c -> Tacticals.New.tclWITHHOLES false tac c.sigma (Some c.it)
 
 TACTIC EXTEND contradiction
  [ "contradiction" constr_with_bindings_opt(c) ] ->
@@ -246,8 +248,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
-  Proofview.Unsafe.tclEVARS sigma <*>
-    general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true
+  Tacticals.New. tclWITHHOLES false
+    (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings)) sigma 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 b1ff0e401..70bf81497 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -497,8 +497,6 @@ let interp_fresh_id ist env sigma l =
       Id.of_string s in
   Tactics.fresh_id_in_env avoid id env
 
-
-
 (* Extract the uconstr list from lfun *)
 let extract_ltac_constr_context ist env =
   let open Glob_term in
@@ -1785,12 +1783,12 @@ 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
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
+        Tacticals.New.tclWITHHOLES false 
+        (fun l' -> name_atomic ~env
           (TacIntroPattern l)
           (* spiwack: print uninterpreted, not sure if it is the
              expected behaviour. *)
-          (Tactics.intros_patterns l')
+          (Tactics.intros_patterns l')) sigma l'
       end
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.enter begin fun gl ->
@@ -1915,20 +1913,20 @@ 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
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
+        Tacticals.New.tclWITHHOLES false
+        (fun c -> name_atomic ~env
           (TacAssert(b,t,ipat,c))
-          (Tactics.forward b tac ipat' c)
+          (Tactics.forward b tac ipat' c)) sigma c
       end
   | TacGeneralize cl ->
       Proofview.Goal.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
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
+        Tacticals.New.tclWITHHOLES false
+        (fun cl -> name_atomic ~env
           (TacGeneralize cl)
-          (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))
+          (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma cl
       end
   | TacGeneralizeDep c ->
       (new_interp_constr ist c) (fun c ->
@@ -1953,11 +1951,11 @@ 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
-	  Proofview.Unsafe.tclEVARS sigma <*>
           let na = interp_fresh_name ist env sigma na in
-          name_atomic ~env
+          Tacticals.New.tclWITHHOLES false
+          (fun na -> name_atomic ~env
             (TacLetTac(na,c_interp,clp,b,eqpat))
-            (let_tac b na c_interp clp eqpat)
+            (let_tac b na c_interp clp eqpat)) sigma na
         else
         (* We try to keep the pattern structure as much as possible *)
           let let_pat_tac b na c cl eqpat =
@@ -2184,10 +2182,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let sigma,ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
+        Tacticals.New.tclWITHHOLES false
+        (fun dqhyps -> name_atomic ~env
           (TacInversion(DepInversion(k,c_interp,ids),dqhyps))
-          (Inv.dinv k c_interp ids_interp dqhyps)
+          (Inv.dinv k c_interp ids_interp dqhyps)) sigma dqhyps
       end
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       Proofview.Goal.enter begin fun gl ->
@@ -2196,10 +2194,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let hyps = interp_hyp_list ist env sigma idl in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let sigma, ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
+        Tacticals.New.tclWITHHOLES false
+        (fun dqhyps -> name_atomic ~env
           (TacInversion (NonDepInversion (k,hyps,ids),dqhyps))
-          (Inv.inv_clause k ids_interp hyps dqhyps)
+          (Inv.inv_clause k ids_interp hyps dqhyps)) sigma dqhyps
       end
   | TacInversion (InversionUsing (c,idl),hyp) ->
       Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6f4c94e3f..e7fde1b83 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2134,11 +2134,12 @@ 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
-        Proofview.Unsafe.tclEVARS sigma <*>
+        Tacticals.New.tclWITHHOLES false
           (Tacticals.New.tclTHENFIRST
              (* Skip the side conditions of the apply *)
              (apply_in_once false true true true naming id
                 (None,(sigma,(c,NoBindings))) tac_ipat))
+          sigma
 	  (tac thin None [])
       end