More expressive API for tclWITHHOLES.

7 files changed, 57 insertions, 63 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 183611659..6d3dc461e 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -71,14 +71,14 @@ 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
+    Tacticals.New.tclWITHHOLES false (Tactics.left_with_bindings false bl) sigma
   ]
 END
 
 TACTIC EXTEND eleft_with
   [ "eleft" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES true (Tactics.left_with_bindings true) sigma bl
+    Tacticals.New.tclWITHHOLES true (Tactics.left_with_bindings true bl) sigma
   ]
 END
 
@@ -95,14 +95,14 @@ 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
+    Tacticals.New.tclWITHHOLES false (Tactics.right_with_bindings false bl) sigma
   ]
 END
 
 TACTIC EXTEND eright_with
   [ "eright" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES true (Tactics.right_with_bindings true) sigma bl
+    Tacticals.New.tclWITHHOLES true (Tactics.right_with_bindings true bl) sigma
   ]
 END
 
@@ -117,8 +117,8 @@ TACTIC EXTEND constructor
 | [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
     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
+    let tac = Tactics.constructor_tac false None i bl in
+    Tacticals.New.tclWITHHOLES false tac sigma
   ]
 END
 
@@ -131,8 +131,8 @@ TACTIC EXTEND econstructor
 | [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma; it = bl } = bl in
     let i = Tacinterp.interp_int_or_var ist i in
-    let tac c = Tactics.constructor_tac true None i c in
-    Tacticals.New.tclWITHHOLES true tac sigma bl
+    let tac = Tactics.constructor_tac true None i bl in
+    Tacticals.New.tclWITHHOLES true tac sigma
   ]
 END
 
@@ -141,8 +141,8 @@ END
 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
+    let specialize = Proofview.V82.tactic (Tactics.specialize c) in
+    Tacticals.New.tclWITHHOLES false specialize sigma
   ]
 END
 
@@ -163,14 +163,14 @@ 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]
+    Tacticals.New.tclWITHHOLES false (Tactics.split_with_bindings false [bl]) sigma
   ]
 END
 
 TACTIC EXTEND esplit_with
   [ "esplit" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true) sigma [bl]
+    Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true [bl]) sigma
   ]
 END
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ae92f4c06..838f8865d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -494,7 +494,7 @@ let general_multi_rewrite with_evars l cl tac =
       let env = Proofview.Goal.env gl in
       let sigma,c = f env sigma in
       tclWITHHOLES with_evars
-        (general_rewrite_clause l2r with_evars ?tac c) sigma cl
+        (general_rewrite_clause l2r with_evars ?tac c cl) sigma
     end
   in
   let rec doN l2r c = function
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 063b425ba..1ffc0519f 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -34,15 +34,13 @@ END
 
 let replace_in_clause_maybe_by (sigma1,c1) c2 cl  tac =
   Tacticals.New.tclWITHHOLES false
-    (replace_in_clause_maybe_by c1 c2 cl)
+    (replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac))
     sigma1
-    (Option.map Tacinterp.eval_tactic tac)
 
 let replace_term dir_opt (sigma,c) cl =
   Tacticals.New.tclWITHHOLES false
-    (replace_term dir_opt c)
+    (replace_term dir_opt c cl)
     sigma
-    cl
 
 TACTIC EXTEND replace
    ["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
@@ -73,8 +71,8 @@ let induction_arg_of_quantified_hyp = function
    ElimOnIdent and not as "constr" *)
 
 let elimOnConstrWithHoles tac with_evars c =
-  Tacticals.New.tclWITHHOLES with_evars (tac with_evars) 
-    c.sigma (Some (None,ElimOnConstr c.it))
+  Tacticals.New.tclWITHHOLES with_evars
+    (tac with_evars (Some (None,ElimOnConstr c.it))) c.sigma
 
 TACTIC EXTEND simplify_eq_main
 | [ "simplify_eq" constr_with_bindings(c) ] ->
@@ -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 -> Tacticals.New.tclWITHHOLES false (tac (Some c.it)) c.sigma
 
 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
+  Tacticals.New.tclWITHHOLES false
+    (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) sigma
 
 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 70bf81497..3b497faab 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1784,11 +1784,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
         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 
-        (fun l' -> name_atomic ~env
+        (name_atomic ~env
           (TacIntroPattern l)
           (* spiwack: print uninterpreted, not sure if it is the
              expected behaviour. *)
-          (Tactics.intros_patterns l')) sigma l'
+          (Tactics.intros_patterns l')) sigma
       end
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.enter begin fun gl ->
@@ -1822,11 +1822,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	    (k,(loc,f))) cb 
 	in
         let sigma,tac = match cl with
-          | None -> sigma, fun l -> Tactics.apply_with_delayed_bindings_gen a ev l
+          | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
           | Some cl ->
               let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in
-              sigma, fun l -> Tactics.apply_delayed_in a ev clear id l cl in
-        Tacticals.New.tclWITHHOLES ev tac sigma l
+              sigma, Tactics.apply_delayed_in a ev clear id l cl in
+        Tacticals.New.tclWITHHOLES ev tac sigma
       end
       end
   | TacElim (ev,(keep,cb),cbo) ->
@@ -1835,22 +1835,22 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma = Proofview.Goal.sigma gl in 
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
         let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
-        let named_tac cbo =
+        let named_tac =
           let tac = Tactics.elim ev keep cb cbo in
           name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac
         in
-        Tacticals.New.tclWITHHOLES ev named_tac sigma cbo
+        Tacticals.New.tclWITHHOLES ev named_tac sigma
       end
   | TacCase (ev,(keep,cb)) ->
       Proofview.Goal.enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
-        let named_tac cb =
+        let named_tac =
           let tac = Tactics.general_case_analysis ev keep cb in
           name_atomic ~env (TacCase(ev,(keep,cb))) tac
         in
-        Tacticals.New.tclWITHHOLES ev named_tac sigma cb
+        Tacticals.New.tclWITHHOLES ev named_tac sigma
       end
   | TacFix (idopt,n) ->
       Proofview.Goal.enter begin fun gl ->
@@ -1914,9 +1914,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
         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
-        (fun c -> name_atomic ~env
+        (name_atomic ~env
           (TacAssert(b,t,ipat,c))
-          (Tactics.forward b tac ipat' c)) sigma c
+          (Tactics.forward b tac ipat' c)) sigma
       end
   | TacGeneralize cl ->
       Proofview.Goal.enter begin fun gl ->
@@ -1924,9 +1924,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
         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
-        (fun cl -> name_atomic ~env
+        (name_atomic ~env
           (TacGeneralize cl)
-          (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma cl
+          (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma
       end
   | TacGeneralizeDep c ->
       (new_interp_constr ist c) (fun c ->
@@ -1953,9 +1953,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
           in
           let na = interp_fresh_name ist env sigma na in
           Tacticals.New.tclWITHHOLES false
-          (fun na -> name_atomic ~env
+          (name_atomic ~env
             (TacLetTac(na,c_interp,clp,b,eqpat))
-            (let_tac b na c_interp clp eqpat)) sigma na
+            (let_tac b na c_interp clp eqpat)) sigma
         else
         (* We try to keep the pattern structure as much as possible *)
           let let_pat_tac b na c cl eqpat =
@@ -1968,7 +1968,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
             (TacLetTac(na,c,clp,b,eqpat))
 	    (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
                (let_pat_tac b (interp_fresh_name ist env sigma na)
-                  ((sigma,sigma'),c) clp) sigma' eqpat)
+                  ((sigma,sigma'),c) clp eqpat) sigma')
       end
 
   (* Automation tactics *)
@@ -2078,11 +2078,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
-        let named_tac bll =
+        let named_tac =
           let tac = Tactics.split_with_bindings ev bll in
           name_atomic ~env (TacSplit (ev, bll)) tac
         in
-        Tacticals.New.tclWITHHOLES ev named_tac sigma bll
+        Tacticals.New.tclWITHHOLES ev named_tac sigma
       end
   (* Conversion *)
   | TacReduce (r,cl) ->
@@ -2183,9 +2183,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
         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
         Tacticals.New.tclWITHHOLES false
-        (fun dqhyps -> name_atomic ~env
+        (name_atomic ~env
           (TacInversion(DepInversion(k,c_interp,ids),dqhyps))
-          (Inv.dinv k c_interp ids_interp dqhyps)) sigma dqhyps
+          (Inv.dinv k c_interp ids_interp dqhyps)) sigma
       end
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       Proofview.Goal.enter begin fun gl ->
@@ -2195,9 +2195,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
         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
         Tacticals.New.tclWITHHOLES false
-        (fun dqhyps -> name_atomic ~env
+        (name_atomic ~env
           (TacInversion (NonDepInversion (k,hyps,ids),dqhyps))
-          (Inv.inv_clause k ids_interp hyps dqhyps)) sigma dqhyps
+          (Inv.inv_clause k ids_interp hyps dqhyps)) sigma
       end
   | TacInversion (InversionUsing (c,idl),hyp) ->
       Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 61bef41d7..9b16fe3f7 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -493,26 +493,23 @@ module New = struct
       let (loc,_) = evi.Evd.evar_source in
       Pretype_errors.error_unsolvable_implicit loc env sigma evk None
 
-  let tclWITHHOLES accept_unresolved_holes tac sigma x =
+  let tclWITHHOLES accept_unresolved_holes tac sigma =
     tclEVARMAP >>= fun sigma_initial ->
-      if sigma == sigma_initial then tac x
+      if sigma == sigma_initial then tac
       else
-        let check_evars env new_sigma sigma initial_sigma =
-          try
-            check_evars env new_sigma sigma initial_sigma;
-            tclUNIT ()
-          with e when Errors.noncritical e ->
-            tclZERO e
-        in
-        let check_evars_if =
+        let check_evars_if x =
           if not accept_unresolved_holes then
             tclEVARMAP >>= fun sigma_final ->
               tclENV >>= fun env ->
-                check_evars env sigma_final sigma sigma_initial
+                try
+                  let () = check_evars env sigma_final sigma sigma_initial in
+                  tclUNIT x
+                with e when Errors.noncritical e ->
+                  tclZERO e
           else
-            tclUNIT ()
+            tclUNIT x
         in
-        Proofview.Unsafe.tclEVARS sigma <*> tac x <*> check_evars_if
+        Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
 
   let tclTIMEOUT n t =
     Proofview.tclOR
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 03ea89ad5..4e860892d 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -218,7 +218,7 @@ module New : sig
   val tclCOMPLETE : 'a tactic -> 'a tactic
   val tclSOLVE : unit tactic list -> unit tactic
   val tclPROGRESS : unit tactic -> unit tactic
-  val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic
+  val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
 
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e7fde1b83..a96ae2688 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1501,7 +1501,7 @@ let apply_with_delayed_bindings_gen b e l =
       let env = Proofview.Goal.env gl in
       let sigma, cb = f env sigma in
 	Tacticals.New.tclWITHHOLES e
-          (general_apply b b e k) sigma (loc,cb)
+          (general_apply b b e k (loc,cb)) sigma
     end
   in
   let rec aux = function
@@ -1604,8 +1604,8 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
     let sigma, c = f env sigma in
     Tacticals.New.tclWITHHOLES with_evars 
       (apply_in_once sidecond_first with_delta with_destruct with_evars
-         naming id (clear_flag,(loc,c)))
-      sigma tac
+         naming id (clear_flag,(loc,c)) tac)
+      sigma
   end
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
@@ -2138,9 +2138,8 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
           (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))
+                (None,(sigma,(c,NoBindings))) tac_ipat) (tac thin None []))
           sigma
-	  (tac thin None [])
       end
 
 and prepare_intros_loc loc dft = function