Merge branch 'v8.5'

19 files changed, 72 insertions, 120 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index ea3f0ac0da..0cc8a0b1b9 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Proof_type
 open Clenv
 open Pattern
 open Evd
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1c15fa40bf..e97a42e6e4 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -17,7 +17,6 @@ open Proof_type
 open Tacticals
 open Tacmach
 open Tactics
-open Patternops
 open Clenv
 open Typeclasses
 open Globnames
@@ -42,7 +41,7 @@ let get_typeclasses_dependency_order () = !typeclasses_dependency_order
 
 open Goptions
 
-let set_typeclasses_modulo_eta =
+let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
@@ -51,7 +50,7 @@ let set_typeclasses_modulo_eta =
       optread  = get_typeclasses_modulo_eta;
       optwrite = set_typeclasses_modulo_eta; }
 
-let set_typeclasses_dependency_order =
+let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9ee14b801c..9b69481da9 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -9,8 +9,6 @@
 open Errors
 open Term
 open Hipattern
-open Tacmach
-open Tacticals
 open Tactics
 open Coqlib
 open Reductionops
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 5c039e72c1..6d3dc461ec 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
-    Proofview.Unsafe.tclEVARS sigma <*> Tactics.left_with_bindings false 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
-    Proofview.Unsafe.tclEVARS sigma <*> Tactics.right_with_bindings false 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
-    Proofview.Unsafe.tclEVARS sigma <*> tac 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
-    Proofview.Unsafe.tclEVARS sigma <*> specialize 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
-    Proofview.Unsafe.tclEVARS sigma <*> Tactics.split_with_bindings false [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/eauto.mli b/tactics/eauto.mli
index 19e2f198bb..7073e8a2b8 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -8,7 +8,6 @@
 
 open Term
 open Proof_type
-open Auto
 open Evd
 open Hints
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index b7d5b1028d..3cb4fa9c4c 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -15,7 +15,6 @@ open Hipattern
 open Tacmach.New
 open Tacticals.New
 open Tactics
-open Misctypes
 open Proofview.Notations
 
 let introElimAssumsThen tac ba =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c130fa1514..838f8865d0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -487,9 +487,6 @@ let apply_special_clear_request clear_flag f =
       e when catchable_exception e -> tclIDTAC
   end
 
-type delayed_open_constr_with_bindings =
-    env -> evar_map -> evar_map * constr with_bindings
-
 let general_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
     Proofview.Goal.enter begin fun gl ->
@@ -497,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
@@ -1474,8 +1471,6 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* then it uses the predicate "\x.phi(proj1_sig x,proj2_sig x)", and so   *)
 (* on for further iterated sigma-tuples                                   *)
 
-exception NothingToRewrite
-
 let cutSubstInConcl l2r eqn =
   Proofview.Goal.nf_enter begin fun gl ->
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
@@ -1513,9 +1508,6 @@ let try_rewrite tac =
     | e when catchable_exception e ->
 	tclZEROMSG
           (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
-    | NothingToRewrite ->
-	tclZEROMSG
-          (strbrk "Nothing to rewrite.")
     | e -> Proofview.tclZERO ~info e
   end
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 90d8a224b5..3e13ee570c 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -11,7 +11,6 @@ open Names
 open Term
 open Evd
 open Environ
-open Tacmach
 open Tacexpr
 open Ind_tables
 open Locus
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 42d00e1e1a..2c4df06080 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Tacmach
 open Names
 open Tacexpr
 open Locus
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f3482c3100..1ffc0519fe 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,15 @@ TACTIC EXTEND admit
   [ "admit" ] -> [ admit_as_an_axiom ]
 END
 
-let replace_in_clause_maybe_by (sigma,c1) c2 cl  tac =
-  Proofview.Unsafe.tclEVARS sigma <*>
-    (replace_in_clause_maybe_by c1 c2 cl)
-    (Option.map Tacinterp.eval_tactic tac)
+let replace_in_clause_maybe_by (sigma1,c1) c2 cl  tac =
+  Tacticals.New.tclWITHHOLES false
+    (replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac))
+    sigma1
 
 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 cl)
+    sigma
 
 TACTIC EXTEND replace
    ["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
@@ -71,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) ] ->
@@ -202,7 +202,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 (Some c.it)) c.sigma
 
 TACTIC EXTEND contradiction
  [ "contradiction" constr_with_bindings_opt(c) ] ->
@@ -246,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
-  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) 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/hipattern.mli b/tactics/hipattern.mli
index c200871ef6..27d25056e1 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Evd
 open Coqlib
 
 (** High-order patterns *)
@@ -145,8 +144,6 @@ val is_matching_sigma : constr -> bool
 val match_eqdec : constr -> bool * constr * constr * constr * constr
 
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
-open Proof_type
-open Tacmach
 val dest_nf_eq : [ `NF ] Proofview.Goal.t -> constr -> (constr * constr * constr)
 
 (** Match a negation *)
diff --git a/tactics/inv.mli b/tactics/inv.mli
index b3478dda27..412f30c20d 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Term
 open Misctypes
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 47a4de444f..2f80d26fc4 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Term
 open Constrexpr
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 1bffa9f60c..53f3f5652c 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -73,7 +73,6 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
 (* Summary and Object declaration *)
 
 open Nametab
-open Libnames
 open Libobject
 
 let mactab =
@@ -86,7 +85,6 @@ let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab)
 
 (* Declaration of the TAC-DEFINITION object *)
 let add (kn,td) = mactab := KNmap.add kn td !mactab
-let replace (kn,td) = mactab := KNmap.add kn td !mactab
 
 let load_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b1ff0e4014..3b497faab5 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 
+        (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
       end
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.enter begin fun gl ->
@@ -1824,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) ->
@@ -1837,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 ->
@@ -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
+        (name_atomic ~env
           (TacAssert(b,t,ipat,c))
-          (Tactics.forward b tac ipat' c)
+          (Tactics.forward b tac ipat' c)) sigma
       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
+        (name_atomic ~env
           (TacGeneralize cl)
-          (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))
+          (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma
       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
+          (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
         else
         (* We try to keep the pattern structure as much as possible *)
           let let_pat_tac b na c cl eqpat =
@@ -1970,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 *)
@@ -2080,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) ->
@@ -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
+        (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
       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
+        (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
       end
   | TacInversion (InversionUsing (c,idl),hyp) ->
       Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 59cd065d12..42e61cb57e 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -100,20 +100,11 @@ let subst_evaluable subst =
   let subst_eval_ref = subst_evaluable_reference subst in
     subst_or_var (subst_and_short_name subst_eval_ref)
 
-let subst_unfold subst (l,e) =
-  (l,subst_evaluable subst e)
-
-let subst_flag subst red =
-  { red with rConst = List.map (subst_evaluable subst) red.rConst }
-
 let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
 
 let subst_glob_constr_or_pattern subst (c,p) =
   (subst_glob_constr subst c,subst_pattern subst p)
 
-let subst_pattern_with_occurrences subst (l,p) =
-  (l,subst_glob_constr_or_pattern subst p)
-
 let subst_redexp subst =
   Miscops.map_red_expr_gen
     (subst_glob_constr subst)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index cf2126f8dd..9b16fe3f7b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -16,7 +16,6 @@ open Context
 open Declarations
 open Tacmach
 open Clenv
-open Misctypes
 
 (************************************************************************)
 (* Tacticals re-exported from the Refiner module                        *)
@@ -494,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 6249bbc593..4e860892d0 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,14 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Pp
 open Names
 open Term
 open Context
 open Tacmach
 open Proof_type
-open Clenv
 open Tacexpr
 open Locus
 open Misctypes
@@ -220,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 07969c7d74..a96ae26888 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -765,8 +765,6 @@ let intro = intro_gen (NamingAvoid []) MoveLast false false
 let introf = intro_gen (NamingAvoid []) MoveLast true false
 let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
 
-let intro_then_force = intro_then_gen (NamingAvoid []) MoveLast true false
-
 let intro_move_avoid idopt avoid hto = match idopt with
   | None -> intro_gen (NamingAvoid avoid) hto true false
   | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false
@@ -1503,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
@@ -1606,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
@@ -2136,12 +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))
-	  (tac thin None [])
+                (None,(sigma,(c,NoBindings))) tac_ipat) (tac thin None []))
+          sigma
       end
 
 and prepare_intros_loc loc dft = function
@@ -2790,12 +2788,6 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
   atomize_one (List.length argl) [] []
   end
 
-let find_atomic_param_of_ind nparams indtyp =
-  let argl = snd (decompose_app indtyp) in
-  let params,args = List.chop nparams argl in
-  let test c = isVar c && not (List.exists (dependent c) params) in
-  List.map destVar (List.filter test args)
-
 (* [cook_sign] builds the lists [beforetoclear] (preceding the
    ind. var.) and [aftertoclear] (coming after the ind. var.)  of hyps
    that must be erased, the lists of hyps to be generalize [decldeps] on the