Reorganization of tactics:

- made "apply" tactics of type Proofview.tactic, as well as other inner
  functions about elim and assert
- used same hypothesis naming policy for intros and internal_cut (towards a
  reorganization of intro patterns)
- "apply ... in H as pat" now supports any kind of introduction
  pattern (doc not changed)

20 files changed, 484 insertions, 402 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index dbd89019e..e6a841153 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -248,7 +248,7 @@ module Btauto = struct
           let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
           Tacticals.New.tclTHENLIST [
             Proofview.V82.tactic (Tactics.change_concl changed_gl);
-            Proofview.V82.tactic (Tactics.apply (Lazy.force soundness));
+            Tactics.apply (Lazy.force soundness);
             Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
             try_unification env
           ]
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 70aaa0c0f..3151a7ec7 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -486,7 +486,7 @@ let f_equal =
         else
           Tacticals.New.tclTRY (Tacticals.New.tclTHEN
           ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut)
-          (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) (fun c -> Proofview.V82.tactic (apply c)))))
+          (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)))
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 7c134da7a..a77b1d60a 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -377,10 +377,10 @@ let tac_zero_inf_pos gl (n,d) =
    let tacn=ref (apply (get coq_Rlt_zero_1)) in
    let tacd=ref (apply (get coq_Rlt_zero_1)) in
    for _i = 1 to n - 1 do
-       tacn:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
+       tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
    for _i = 1 to d - 1 do
-       tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
-   (tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd])
+       tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
+   (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd])
 ;;
 
 (* preuve que 0<=n*1/d
@@ -391,10 +391,10 @@ let tac_zero_infeq_pos gl (n,d)=
                  else (apply (get coq_Rle_zero_1))) in
    let tacd=ref (apply (get coq_Rlt_zero_1)) in
    for  _i = 1 to n - 1 do
-       tacn:=(tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
+       tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
    for _i = 1 to d - 1 do
-       tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
-   (tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
+       tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
+   (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
 ;;
 
 (* preuve que 0<(-n)*(1/d) => False
@@ -402,14 +402,14 @@ let tac_zero_infeq_pos gl (n,d)=
 let tac_zero_inf_false gl (n,d) =
     if n=0 then (apply (get coq_Rnot_lt0))
     else
-     (tclTHEN (apply (get coq_Rle_not_lt))
+     (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt))
 	      (tac_zero_infeq_pos gl (-n,d)))
 ;;
 
 (* preuve que 0<=(-n)*(1/d) => False
 *)
 let tac_zero_infeq_false gl (n,d) =
-     (tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
+     (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
 	      (tac_zero_inf_pos gl (-n,d)))
 ;;
 
@@ -423,14 +423,14 @@ let my_cut c gl=
 let exact = exact_check;;
 
 let tac_use h =
-  let tac = Proofview.V82.of_tactic (exact h.hname) in
+  let tac = exact h.hname in
   match h.htype with
     "Rlt" -> tac
   |"Rle" -> tac
-  |"Rgt" -> (tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac)
-  |"Rge" -> (tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac)
-  |"eqTLR" -> (tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac)
-  |"eqTRL" -> (tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac)
+  |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac)
+  |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac)
+  |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac)
+  |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac)
   |_->assert false
 ;;
 
@@ -462,43 +462,44 @@ let mkAppL a =
 exception GoalDone
 
 (* Résolution d'inéquations linéaires dans R *)
-let rec fourier gl=
+let rec fourier () =
+  Proofview.Goal.enter begin fun gl ->
+    let concl = Proofview.Goal.concl gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
-    let goal = strip_outer_cast (pf_concl gl) in
+    let goal = strip_outer_cast concl in
     let fhyp=Id.of_string "new_hyp_for_fourier" in
     (* si le but est une inéquation, on introduit son contraire,
        et le but à prouver devient False *)
-    try (let tac =
-     match (kind_of_term goal) with
+    try 
+      match (kind_of_term goal) with
       App (f,args) ->
       (match (string_of_R_constr f) with
 	     "Rlt" ->
-	       (tclTHEN
-	         (tclTHEN (apply (get coq_Rfourier_not_ge_lt))
-			  (Proofview.V82.of_tactic (intro_using  fhyp)))
-		 fourier)
+	       (Tacticals.New.tclTHEN
+	         (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt))
+			  (intro_using  fhyp))
+		 (fourier ()))
 	    |"Rle" ->
-	     (tclTHEN
-	      (tclTHEN (apply (get coq_Rfourier_not_gt_le))
-		       (Proofview.V82.of_tactic (intro_using  fhyp)))
-			fourier)
+	     (Tacticals.New.tclTHEN
+	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le))
+		       (intro_using  fhyp))
+			(fourier ()))
 	    |"Rgt" ->
-	     (tclTHEN
-	      (tclTHEN (apply (get coq_Rfourier_not_le_gt))
-		       (Proofview.V82.of_tactic (intro_using  fhyp)))
-	      fourier)
+	     (Tacticals.New.tclTHEN
+	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt))
+		       (intro_using  fhyp))
+	      (fourier ()))
 	    |"Rge" ->
-	     (tclTHEN
-	      (tclTHEN (apply (get coq_Rfourier_not_lt_ge))
-		       (Proofview.V82.of_tactic (intro_using  fhyp)))
-	      fourier)
+	     (Tacticals.New.tclTHEN
+	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge))
+		       (intro_using  fhyp))
+	      (fourier ()))
 	    |_-> raise GoalDone)
         |_-> raise GoalDone
-      in tac gl)
      with GoalDone ->
     (* les hypothèses *)
     let hyps = List.map (fun (h,t)-> (mkVar h,t))
-                        (list_of_sign (pf_hyps gl)) in
+                        (list_of_sign (Proofview.Goal.hyps gl)) in
     let lineq =ref [] in
     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
 		        with NoIneq -> ())
@@ -506,7 +507,7 @@ let rec fourier gl=
     (* lineq = les inéquations découlant des hypothèses *)
     if !lineq=[] then Errors.error "No inequalities";
     let res=fourier_lineq (!lineq) in
-    let tac=ref tclIDTAC in
+    let tac=ref (Proofview.tclUNIT ()) in
     if res=[]
     then Errors.error "fourier failed"
     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
@@ -551,11 +552,11 @@ let rec fourier gl=
 	   let tc=rational_to_real cres in
        (* puis sa preuve *)
            let tac1=ref (if h1.hstrict
-                         then (tclTHENS (apply (get coq_Rfourier_lt))
+                         then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt))
                                  [tac_use h1;
                                   tac_zero_inf_pos  gl
                                       (rational_to_fraction c1)])
-                         else (tclTHENS (apply (get coq_Rfourier_le))
+                         else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le))
                                  [tac_use h1;
 				  tac_zero_inf_pos  gl
                                       (rational_to_fraction c1)])) in
@@ -563,20 +564,20 @@ let rec fourier gl=
            List.iter (fun (h,c)->
              (if (!s)
 	      then (if h.hstrict
-	            then tac1:=(tclTHENS (apply (get coq_Rfourier_lt_lt))
+	            then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt))
 			       [!tac1;tac_use h;
 			        tac_zero_inf_pos  gl
                                       (rational_to_fraction c)])
-	            else tac1:=(tclTHENS (apply (get coq_Rfourier_lt_le))
+	            else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le))
 			       [!tac1;tac_use h;
 			        tac_zero_inf_pos  gl
                                       (rational_to_fraction c)]))
 	      else (if h.hstrict
-	            then tac1:=(tclTHENS (apply (get coq_Rfourier_le_lt))
+	            then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt))
 			       [!tac1;tac_use h;
 			        tac_zero_inf_pos  gl
                                       (rational_to_fraction c)])
-	            else tac1:=(tclTHENS (apply (get coq_Rfourier_le_le))
+	            else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le))
 			       [!tac1;tac_use h;
 			        tac_zero_inf_pos  gl
                                       (rational_to_fraction c)])));
@@ -586,43 +587,43 @@ let rec fourier gl=
                       then tac_zero_inf_false gl (rational_to_fraction cres)
                       else tac_zero_infeq_false gl (rational_to_fraction cres)
            in
-           tac:=(tclTHENS (my_cut ineq)
-                     [tclTHEN (change_concl
+           tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq))
+                     [Tacticals.New.tclTHEN (Proofview.V82.tactic (change_concl
 			       (mkAppL [| get coq_not; ineq|]
-				       ))
-		      (tclTHEN (apply (if sres then get coq_Rnot_lt_lt
+				       )))
+		      (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
 					       else get coq_Rnot_le_le))
-			    (tclTHENS (Proofview.V82.of_tactic (Equality.replace
+			    (Tacticals.New.tclTHENS (Equality.replace
 				       (mkAppL [|get coq_Rminus;!t2;!t1|]
 					       )
-				       tc))
+				       tc)
 		 	       [tac2;
-                                (tclTHENS
-				  (Proofview.V82.of_tactic (Equality.replace
+                                (Tacticals.New.tclTHENS
+				  (Equality.replace
 				    (mkApp (get coq_Rinv,
 				      [|get coq_R1|]))
-				    (get coq_R1)))
+				    (get coq_R1))
 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
 
-      			        [tclORELSE
-                                   (* TODO : Ring.polynom []*) tclIDTAC
-                                   tclIDTAC;
-				 pf_constr_of_global (get coq_sym_eqT) (fun symeq ->
-					  (tclTHEN (apply symeq)
+      			        [Tacticals.New.tclORELSE
+                                   (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
+                                   (Proofview.tclUNIT ());
+				 Tacticals.New.pf_constr_of_global (get coq_sym_eqT) (fun symeq ->
+					  (Tacticals.New.tclTHEN (apply symeq)
 						(apply (get coq_Rinv_1))))]
 
 					 )
 				]));
                        !tac1]);
-	   tac:=(tclTHENS (Proofview.V82.of_tactic (cut (get coq_False)))
-				  [tclTHEN (Proofview.V82.of_tactic intro) (Proofview.V82.of_tactic (contradiction None));
+	   tac:=(Tacticals.New.tclTHENS (cut (get coq_False))
+				  [Tacticals.New.tclTHEN intro (contradiction None);
 				   !tac])
       |_-> assert false) |_-> assert false
 	  );
 (*    ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
-      (!tac gl)
+      !tac
 (*      ((tclABSTRACT None !tac) gl) *)
-
+  end
 ;;
 
 (*
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index 11107385d..25451fd92 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -13,5 +13,5 @@ open FourierR
 DECLARE PLUGIN "fourier_plugin"
 
 TACTIC EXTEND fourier
-  [ "fourierz" ] -> [ Proofview.V82.tactic fourier ]
+  [ "fourierz" ] -> [ fourier () ]
 END
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 1981fb837..7f0db547d 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1433,11 +1433,11 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 	 backtrack_eqs_until_hrec hrec eqs;
 	 (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
 	 (tclTHENS  (* We must have exactly ONE subgoal !*)
-	    (apply (mkVar hrec))
+	    (Proofview.V82.of_tactic (apply (mkVar hrec)))
 	    [ tclTHENSEQ
 		[
 		  keep (tcc_hyps@eqs);
-		  apply (Lazy.force acc_inv);
+		  (Proofview.V82.of_tactic (apply (Lazy.force acc_inv)));
 		  (fun g ->
 		     if is_mes
 		     then
@@ -1556,7 +1556,7 @@ let prove_principle_for_gen
 	       (
 		 (* observe_tac  *)
 (* 		   "apply wf_thm"  *)
-		 Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))
+		 Proofview.V82.of_tactic (Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|])))
 	       )
 	    )
 	 )
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 5682c2aa4..4fcc65bda 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -487,7 +487,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    (fun gl -> 
 	      let term = mkApp (mkVar principle_id,Array.of_list bindings) in
 	      let gl', _ty = pf_eapply Typing.e_type_of gl term in
-		apply term gl')
+		Proofview.V82.of_tactic (apply term) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
       ]
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1fa16a301..ff35c9812 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -255,7 +255,7 @@ let tclUSER tac is_mes l g =
       | None -> clear []
       | Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l)
   in
-  tclTHENSEQ
+  tclTHENLIST
     [
       clear_tac;
       if is_mes
@@ -271,7 +271,7 @@ let tclUSER tac is_mes l g =
 
 let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
   if is_mes
-  then tclCOMPLETE (Simple.apply (delayed_force well_founded_ltof))
+  then tclCOMPLETE (fun gl -> Proofview.V82.of_tactic (Simple.apply (delayed_force well_founded_ltof)) gl)
   else (* tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) *) (tclUSER concl_tac is_mes names_to_suppress)
 
 
@@ -377,12 +377,12 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
     ) [] rev_context in 
     let rev_ids = pf_get_new_ids (List.rev ids) g in 
     let new_b = substl (List.map mkVar rev_ids) b in 
-    tclTHENSEQ 
+    tclTHENLIST 
       [
 	h_intros (List.rev rev_ids);
 	Proofview.V82.of_tactic (intro_using teq_id);
 	onLastHypId (fun heq -> 
-	  tclTHENSEQ[
+	  tclTHENLIST[
 	    thin to_intros;
 	    h_intros to_intros;
 	    (fun g' -> 
@@ -507,14 +507,14 @@ let rec prove_lt hyple g =
       let y =
 	List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in
       tclTHENLIST[
-	apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]));
+	Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
 	observe_tac (str "prove_lt") (prove_lt hyple)
       ]
     with Not_found -> 
       (
 	(
 	  tclTHENLIST[
-	    apply (delayed_force lt_S_n);
+	    Proofview.V82.of_tactic (apply (delayed_force lt_S_n));
 	    (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption))
 	  ])
       )
@@ -764,7 +764,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 	  ];
 	  observe_tac (str "proving decreasing") (
 	    tclTHENS (* proof of args < formal args *)
-	      (apply (Lazy.force expr_info.acc_inv))
+	      (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv)))
 	      [ 
 		observe_tac (str "assumption") (Proofview.V82.of_tactic assumption);
 		tclTHENLIST
@@ -812,7 +812,7 @@ let rec prove_le g =
   in 
   tclFIRST[
     Proofview.V82.of_tactic assumption;
-    apply (delayed_force le_n);
+    Proofview.V82.of_tactic (apply (delayed_force le_n));
     begin
       try
 	let matching_fun = 
@@ -825,7 +825,7 @@ let rec prove_le g =
 	  List.hd (List.tl args)
 	in 
 	tclTHENLIST[
-	  apply(mkApp(le_trans (),[|x;y;z;mkVar h|]));
+	  Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|])));
 	  observe_tac (str "prove_le (rec)") (prove_le)
 	] 
       with Not_found -> tclFAIL 0 (mt())
@@ -855,7 +855,7 @@ let rec make_rewrite_list expr_info max = function
       )
       [make_rewrite_list expr_info max l;
        tclTHENLIST[ (* x < S max proof *)
-	 apply (delayed_force le_lt_n_Sm);
+	 Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm));
 	 observe_tac (str "prove_le(2)") prove_le
        ]
       ] )
@@ -892,7 +892,7 @@ let make_rewrite expr_info l hp max =
 	   (observe_tac (str "h_reflexivity") (Proofview.V82.of_tactic intros_reflexivity))]))
        ;
 	 tclTHENLIST[ (* x < S (S max) proof *)
-	 apply (delayed_force le_lt_SS);
+	 Proofview.V82.of_tactic (apply (delayed_force le_lt_SS));
 	 observe_tac (str "prove_le (3)") prove_le
 	 ]
        ])  
@@ -1082,12 +1082,12 @@ let termination_proof_header is_mes input_type ids args_id relation
 		 (* this gives the accessibility argument *)
 		 observe_tac
 		   (str "apply wf_thm")
-		   (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))
+		   (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])))
 		   )
 	       ]
 	     ;
 	     (* rest of the proof *)
-	     tclTHENSEQ
+	     tclTHENLIST
 	       [observe_tac (str "generalize")
 		  (onNLastHypsId (nargs+1)
 		     (tclMAP (fun id ->
@@ -1206,7 +1206,7 @@ let build_and_l l =
 	let c,tac,nb = f pl in
 	mk_and p1 c,
 	tclTHENS
-	  (apply (constr_of_global conj_constr))
+	  (Proofview.V82.of_tactic (apply (constr_of_global conj_constr)))
 	  [tclIDTAC;
 	   tac
 	  ],nb+1
@@ -1278,7 +1278,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
     build_proof Evd.empty_evar_universe_context
       (  fun gls ->
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
-	   tclTHENSEQ
+	   tclTHENLIST
 	     [
 	       Simple.generalize [lemma];
 	       Proofview.V82.of_tactic (Simple.intro hid);
@@ -1306,7 +1306,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
 		    tclCOMPLETE(
 		      tclFIRST[
 			tclTHEN
-			  (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
+			  (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
 			  e_assumption;
 		      Eauto.eauto_with_bases
 			(true,5)
@@ -1338,11 +1338,11 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
 	       (tclFIRST
 	 	  (List.map
 	 	     (fun c ->
-	 		tclTHENSEQ
-	 		  [Proofview.V82.of_tactic intros;
+	 		Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST
+	 		  [intros;
 	 		   Simple.apply (fst (interp_constr Evd.empty (Global.env()) c)) (*FIXME*);
-	 		   tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto)
-	 		  ]
+	 		   Tacticals.New.tclCOMPLETE Auto.default_auto
+	 		  ])
 	 	     )
 	 	     using_lemmas)
 	       ) tclIDTAC)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 271cade27..48c853029 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -37,7 +37,7 @@ let elim_id id =
   Proofview.Goal.enter begin fun gl ->
     simplest_elim (Tacmach.New.pf_global id gl)
   end
-let resolve_id id gl = apply (pf_global gl id) gl
+let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
 
 let timing timer_name f arg = f arg
 
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e22816c13..1835b6cc9 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1283,7 +1283,7 @@ let resolution env full_reified_goal systems_list =
   Tactics.generalize
     (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
   Tactics.change_concl reified >>
-  Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
+  Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
   show_goal >>
   Tactics.normalise_vm_in_concl >>
   (*i Alternatives to the previous line:
@@ -1292,7 +1292,7 @@ let resolution env full_reified_goal systems_list =
    - Skip the conversion check and rely directly on the QED:
       Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >>
   i*)
-  Tactics.apply (Lazy.force coq_I)
+  Proofview.V82.of_tactic (Tactics.apply (Lazy.force coq_I))
 
 let total_reflexive_omega_tactic gl =
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 59de85901..dc8f31859 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -573,6 +573,7 @@ let prim_refiner r sigma goal =
 	       raise (RefinerError IntroNeedsProduct))
 
     | Cut (b,replace,id,t) ->
+(*        if !check && not (Retyping.get_sort_of env sigma t) then*)
         let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
 	let sign,t,cl,sigma =
 	  if replace then
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index dbfde64e4..a4babd276 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -79,8 +79,8 @@ let apply_tac_list tac glls =
 
 let one_step l gl =
   [Proofview.V82.of_tactic Tactics.intro]
-  @ (List.map Tactics.Simple.eapply (List.map mkVar (pf_ids_of_hyps gl)))
-  @ (List.map Tactics.Simple.eapply l)
+  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
+  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
   @ (List.map assumption (pf_ids_of_hyps gl))
 
 let rec prolog l n gl =
@@ -122,7 +122,7 @@ let unify_e_resolve poly flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv' in
   let clenv' = clenv_unique_resolver ~flags clenv' gls in
     tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-      (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c)) gls
+      (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls
 
 let e_exact poly flags (c,clenv) =
   let clenv', subst = 
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 5aceeb9f4..1c249c999 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -117,7 +117,7 @@ let diseqCase eqonleft =
   (tclTHEN (choose_noteq eqonleft)
   (tclTHEN  (Proofview.V82.tactic red_in_concl)
   (tclTHEN  (intro_using absurd)
-  (tclTHEN  (Proofview.V82.tactic (Simple.apply (mkVar diseq)))
+  (tclTHEN  (Simple.apply (mkVar diseq))
   (tclTHEN  (Extratactics.injHyp absurd)
             (full_trivial [])))))))
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 91d774e6e..56a5920a1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -563,7 +563,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
 	    (clear [id]));
 	 tclFIRST
 	   [assumption;
-	    tclTHEN (Proofview.V82.tactic (apply sym)) assumption;
+	    tclTHEN (apply sym) assumption;
 	    try_prove_eq
 	   ]
 	]))
@@ -1513,9 +1513,8 @@ let cutSubstInHyp_LR eqn id =
   let sigma,body,expected_goal = pf_apply subst_tuple_term gl e1 e2 idtyp in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
   let refine = Proofview.V82.tactic (fun gl -> Tacmach.refine_no_check (mkVar id) gl) in
-  let subst = Proofview.V82.of_tactic (tclTHENFIRST (bareRevSubstInConcl (lbeq,u) body eq) refine) in
-    Proofview.V82.tclEVARS sigma <*>
-      Proofview.V82.tactic (fun gl -> cut_replacing id expected_goal subst gl)
+  let subst = tclTHENFIRST (bareRevSubstInConcl (lbeq,u) body eq) refine in
+    Proofview.V82.tclEVARS sigma <*> (cut_replacing id expected_goal subst)
   end
 
 let cutSubstInHyp_RL eqn id =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index af28f5145..e50786b31 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -477,7 +477,7 @@ let step left x tac =
   let l =
     List.map (fun lem ->
       Tacticals.New.tclTHENLAST
-      (Proofview.V82.tactic (apply_with_bindings (lem, ImplicitBindings [x])))
+        (apply_with_bindings (lem, ImplicitBindings [x]))
         tac)
       !(if left then transitivity_left_table else transitivity_right_table)
   in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 8592cd33d..a8a4b1dcc 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1426,7 +1426,7 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
 	let tac = 
 	  match clause, p with
 	  | Some id, Some p ->
-	      cut_replacing id newt (Tacmach.refine p)
+	      Proofview.V82.of_tactic (cut_replacing id newt (Proofview.V82.tactic (Tacmach.refine p)))
 	  | Some id, None -> 
 	      change_in_hyp None (fun env sigma -> sigma, newt) (id, InHypTypeOnly)
 	  | None, Some p ->
@@ -2025,7 +2025,7 @@ let setoid_reflexivity =
   setoid_proof "reflexive"
     (fun env evm car rel -> 
       tac_open (poly_proof PropGlobal.get_reflexive_proof TypeGlobal.get_reflexive_proof
-		  env evm car rel) apply)
+		  env evm car rel) (fun c -> Proofview.V82.of_tactic (apply c)))
     (reflexivity_red true)
 
 let setoid_symmetry =
@@ -2034,7 +2034,7 @@ let setoid_symmetry =
       tac_open
 	(poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof
 	   env evm car rel)
-	apply)
+	(fun c -> Proofview.V82.of_tactic (apply c)))
     (symmetry_red true)
     
 let setoid_transitivity c =
@@ -2043,8 +2043,8 @@ let setoid_transitivity c =
       tac_open (poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof
 	   env evm car rel)
 	(fun proof -> match c with
-	| None -> eapply proof
-	| Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])))
+	| None -> Proofview.V82.of_tactic (eapply proof)
+	| Some c -> Proofview.V82.of_tactic (apply_with_bindings (proof,ImplicitBindings [ c ]))))
     (transitivity_red true c)
     
 let setoid_symmetry_in id =
@@ -2063,7 +2063,7 @@ let setoid_symmetry_in id =
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
     tclTHENS (Proofview.V82.of_tactic (Tactics.cut new_hyp))
       [ intro_replacing id;
-	tclTHENLIST [ Proofview.V82.of_tactic intros; Proofview.V82.of_tactic setoid_symmetry; apply (mkVar id); Proofview.V82.of_tactic Tactics.assumption ] ]
+	Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]) ]
       gl)
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e1c53df4d..02e49584f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1691,7 +1691,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           List.fold_map (interp_open_constr_with_bindings_arg_loc ist env) sigma cb
         in
         let tac = match cl with
-          | None -> fun l -> Proofview.V82.tactic (Tactics.apply_with_bindings_gen a ev l)
+          | None -> fun l -> Tactics.apply_with_bindings_gen a ev l
           | Some cl ->
               (fun l ->
                 Proofview.Goal.raw_enter begin fun gl ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 59318fb22..c82db8531 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -182,25 +182,9 @@ let apply_clear_request clear_flag dft c =
   if clear then Proofview.V82.tactic (thin [destVar c])
   else Tacticals.New.tclIDTAC
 
-let internal_cut_gen b d t gl =
-  try internal_cut b d t gl
-  with Evarutil.ClearDependencyError (id,err) ->
-    error_clear_dependency (pf_env gl) id err
-
-let internal_cut = internal_cut_gen false
-let internal_cut_replace = internal_cut_gen true
-
-let internal_cut_rev_gen b id t gl =
-  try internal_cut_rev b id t gl
-  with Evarutil.ClearDependencyError (id,err) ->
-    error_clear_dependency (pf_env gl) id err
-
-let internal_cut_rev_replace = internal_cut_rev_gen true
-
 (* Moving hypotheses *)
 let move_hyp        = Tacmach.move_hyp
 
-
 (* Renaming hypotheses *)
 let rename_hyp      = Tacmach.rename_hyp
 
@@ -217,6 +201,71 @@ let fresh_id avoid id gl =
 let new_fresh_id avoid id gl =
   fresh_id_in_env avoid id (Proofview.Goal.env gl)
 
+let id_of_name_with_default id = function
+  | Anonymous -> id
+  | Name id   -> id
+
+let default_id_of_sort s =
+  if Sorts.is_small s then default_small_ident else default_type_ident
+
+let default_id env sigma = function
+  | (name,None,t) ->
+      let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in
+      id_of_name_with_default dft name
+  | (name,Some b,_) -> id_of_name_using_hdchar env b name
+
+(* Non primitive introduction tactics are treated by intro_then_gen
+   There is possibly renaming, with possibly names to avoid and
+   possibly a move to do after the introduction *)
+
+type name_flag =
+  | NamingAvoid of Id.t list
+  | NamingBasedOn of Id.t * Id.t list
+  | NamingMustBe of Loc.t * Id.t
+
+let find_name repl decl naming gl = match naming with
+  | NamingAvoid idl ->
+      (* this case must be compatible with [find_intro_names] below. *)
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      new_fresh_id idl (default_id env sigma decl) gl
+  | NamingBasedOn (id,idl) ->  new_fresh_id idl id gl
+  | NamingMustBe (loc,id) ->
+      (* When name is given, we allow to hide a global name *)
+      let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
+      let id' = next_ident_away id ids_of_hyps in
+      if not repl && not (Id.equal id' id) then
+        user_err_loc (loc,"",pr_id id ++ str" is already used.");
+      id
+
+(**************************************************************)
+(*            Cut rule                                        *)
+(**************************************************************)
+
+let internal_cut_gen b naming t =
+  Proofview.Goal.raw_enter begin fun gl ->
+  try 
+    let id = find_name b (Anonymous,None,t) naming gl in
+    Proofview.V82.tactic (internal_cut b id t)
+  with Evarutil.ClearDependencyError (id,err) ->
+    error_clear_dependency (Proofview.Goal.env gl) id err
+  end
+
+let internal_cut = internal_cut_gen false
+let internal_cut_replace = internal_cut_gen true
+
+let internal_cut_rev_gen b naming t =
+  Proofview.Goal.raw_enter begin fun gl ->
+  try
+    let id = find_name b (Anonymous,None,t) naming gl in
+    Proofview.V82.tactic (internal_cut_rev b id t)
+  with Evarutil.ClearDependencyError (id,err) ->
+    error_clear_dependency (Proofview.Goal.env gl) id err
+  end
+
+let internal_cut_rev = internal_cut_rev_gen false
+let internal_cut_rev_replace = internal_cut_rev_gen true
+
 (**************************************************************)
 (*          Fixpoints and CoFixpoints                         *)
 (**************************************************************)
@@ -462,42 +511,6 @@ let unfold_constr = function
 (*         Introduction tactics            *)
 (*******************************************)
 
-let id_of_name_with_default id = function
-  | Anonymous -> id
-  | Name id   -> id
-
-let default_id_of_sort s =
-  if Sorts.is_small s then default_small_ident else default_type_ident
-
-let default_id env sigma = function
-  | (name,None,t) ->
-      let dft = default_id_of_sort (Typing.sort_of env sigma t) in
-      id_of_name_with_default dft name
-  | (name,Some b,_) -> id_of_name_using_hdchar env b name
-
-(* Non primitive introduction tactics are treated by central_intro
-   There is possibly renaming, with possibly names to avoid and
-   possibly a move to do after the introduction *)
-
-type intro_name_flag =
-  | IntroAvoid of Id.t list
-  | IntroBasedOn of Id.t * Id.t list
-  | IntroMustBe of Id.t
-
-let find_name loc decl x gl = match x with
-  | IntroAvoid idl ->
-      (* this case must be compatible with [find_intro_names] below. *)
-      let env = Proofview.Goal.env gl in
-      let sigma = Proofview.Goal.sigma gl in
-      new_fresh_id idl (default_id env sigma decl) gl
-  | IntroBasedOn (id,idl) ->  new_fresh_id idl id gl
-  | IntroMustBe id ->
-      (* When name is given, we allow to hide a global name *)
-      let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
-      let id' = next_ident_away id ids_of_hyps in
-      if not (Id.equal id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used.");
-      id'
-
 (* Returns the names that would be created by intros, without doing
    intros.  This function is supposed to be compatible with an
    iteration of [find_name] above. As [default_id] checks the sort of
@@ -518,16 +531,16 @@ let build_intro_tac id dest tac = match dest with
   | MoveLast -> Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id)
   | dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id]
 
-let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
+let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   Proofview.Goal.raw_enter begin fun gl ->
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
     let concl = nf_evar (Proofview.Goal.sigma gl) concl in
     match kind_of_term concl with
     | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
-        let name = find_name loc (name,None,t) name_flag gl in
+        let name = find_name false (name,None,t) name_flag gl in
 	build_intro_tac name move_flag tac
     | LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
-        let name = find_name loc (name,Some b,t) name_flag gl in
+        let name = find_name false (name,Some b,t) name_flag gl in
 	build_intro_tac name move_flag tac
     | _ ->
 	begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct)
@@ -539,23 +552,23 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
         end <*>
 	  Proofview.tclORELSE
 	  (Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl)
-	     (intro_then_gen loc name_flag move_flag false dep_flag tac))
+	     (intro_then_gen name_flag move_flag false dep_flag tac))
           begin function
             | RefinerError IntroNeedsProduct ->
-                Proofview.tclZERO (Loc.add_loc (Errors.UserError("Intro",str "No product even after head-reduction.")) loc)
+                Proofview.tclZERO (Errors.UserError("Intro",str "No product even after head-reduction."))
             | e -> Proofview.tclZERO e
           end
   end
 
-let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> Proofview.tclUNIT ())
-let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) MoveLast true false
-let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) MoveLast false false
-let intro_then = intro_then_gen dloc (IntroAvoid []) MoveLast false false
-let intro = intro_gen dloc (IntroAvoid []) MoveLast false false
-let introf = intro_gen dloc (IntroAvoid []) MoveLast true false
-let intro_avoiding l = intro_gen dloc (IntroAvoid l) MoveLast false false
+let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ())
+let intro_mustbe_force id = intro_gen (NamingMustBe (dloc,id)) MoveLast true false
+let intro_using id = intro_gen (NamingBasedOn (id,[])) MoveLast false false
+let intro_then = intro_then_gen (NamingAvoid []) MoveLast false false
+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 dloc (IntroAvoid []) MoveLast true false
+let intro_then_force = intro_then_gen (NamingAvoid []) MoveLast true false
 
 (**** Multiple introduction tactics ****)
 
@@ -565,13 +578,13 @@ let rec intros_using = function
 
 let intros = Tacticals.New.tclREPEAT intro
 
-let intro_forthcoming_then_gen loc name_flag move_flag dep_flag n bound tac =
+let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
   let rec aux n ids =
     (* Note: we always use the bound when there is one for "*" and "**" *)
     if (match bound with None -> true | Some (_,p) -> n < p) then
     Proofview.tclORELSE
       begin
-      intro_then_gen loc name_flag move_flag false dep_flag
+      intro_then_gen name_flag move_flag false dep_flag
          (fun id -> aux (n+1) (id::ids))
       end
       begin function
@@ -625,8 +638,8 @@ let intros_replacing ids =
 (* User-level introduction tactics *)
 
 let intro_move idopt hto = match idopt with
-  | None -> intro_gen dloc (IntroAvoid []) hto true false
-  | Some id -> intro_gen dloc (IntroMustBe id) hto true false
+  | None -> intro_gen (NamingAvoid []) hto true false
+  | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false
 
 let pf_lookup_hypothesis_as_renamed env ccl = function
   | AnonHyp n -> Detyping.lookup_index_as_renamed env ccl n
@@ -691,7 +704,7 @@ let try_intros_until tac = function
 let rec intros_move = function
   | [] -> Proofview.tclUNIT ()
   | (hyp,destopt) :: rest ->
-      Tacticals.New.tclTHEN (intro_gen dloc (IntroMustBe hyp) destopt false false)
+      Tacticals.New.tclTHEN (intro_gen (NamingMustBe (dloc,hyp)) destopt false false)
 	(intros_move rest)
 
 (* Apply a tactic on a quantified hypothesis, an hypothesis in context
@@ -775,7 +788,9 @@ let cut_intro t = Tacticals.New.tclTHENFIRST (cut t) intro
    another hypothesis.
 *)
 
-let assert_replacing id t tac = tclTHENFIRST (internal_cut_replace id t) tac
+let assert_replacing id t tac =
+  Tacticals.New.tclTHENFIRST
+    (internal_cut_replace (NamingMustBe (dloc,id)) t) tac
 
 (* [cut_replacing id T tac] adds the subgoals of the proof of [T]
    after the current goal
@@ -788,7 +803,9 @@ let assert_replacing id t tac = tclTHENFIRST (internal_cut_replace id t) tac
    another hypothesis.
 *)
 
-let cut_replacing id t tac = tclTHENLAST (internal_cut_rev_replace id t) tac
+let cut_replacing id t tac =
+  Tacticals.New.tclTHENLAST
+    (internal_cut_rev_replace (NamingMustBe (dloc,id)) t) tac
 
 let error_uninstantiated_metas t clenv =
   let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
@@ -808,10 +825,9 @@ let check_unresolved_evars_of_metas sigma clenv =
   | _ -> ())
   (meta_list clenv.evd)
 
-let clear_of_flag flag =
-  match flag with
-  | None -> true (* default for apply in *)
-  | Some b -> b
+let make_naming id t = function
+  | None -> (true,NamingMustBe (dloc,id)) (* default for apply in *)
+  | Some naming -> naming
 
 (* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some
    goal [G], [clenv_refine_in] returns [n+1] subgoals, the [n] last
@@ -819,8 +835,7 @@ let clear_of_flag flag =
    [Ti] and the first one (resp last one) being [G] whose hypothesis
    [id] is replaced by P using the proof given by [tac] *)
 
-let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) clear_flag id clenv0 gl =
-  let with_clear = clear_of_flag clear_flag in
+let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) naming id clenv0 =
   let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv0 in
   let clenv =
     if with_classes then
@@ -832,15 +847,16 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) clea
   if not with_evars && occur_meta new_hyp_typ then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
-  let id' = if with_clear then id else fresh_id [] id gl in
-  let exact_tac = refine_no_check new_hyp_prf in
-  tclTHEN
-    (tclEVARS clenv.evd)
+  let exact_tac = Proofview.V82.tactic (refine_no_check new_hyp_prf) in
+  let with_clear,naming = make_naming id new_hyp_prf naming in
+  Tacticals.New.tclTHEN
+    (Proofview.V82.tclEVARS clenv.evd)
     (if sidecond_first then
-       tclTHENFIRST (internal_cut_gen with_clear id' new_hyp_typ) exact_tac
+       Tacticals.New.tclTHENFIRST
+         (internal_cut_gen with_clear naming new_hyp_typ) exact_tac
      else
-       tclTHENLAST (internal_cut_rev_gen with_clear id' new_hyp_typ) exact_tac)
-    gl
+       Tacticals.New.tclTHENLAST
+         (internal_cut_rev_gen with_clear naming new_hyp_typ) exact_tac)
 
 (********************************************)
 (*       Elimination tactics                *)
@@ -894,19 +910,24 @@ let enforce_prop_bound_names rename tac =
         | LetIn (na,c,t,t') ->
             mkLetIn (na,c,t,aux (push_rel (na,Some c,t) env) sigma (i-1) t')
         | _ -> print_int i; Pp.msg (print_constr t); assert false in
-      let rename_branch i gl =
-        let env = pf_env gl in
-        let sigma = project gl in
-        let t = pf_concl gl in
-        change_concl (aux env sigma i t) gl in
-      (if isrec then tclTHENFIRSTn else tclTHENLASTn)
+      let rename_branch i =
+        Proofview.Goal.enter begin fun gl ->
+          let env = Proofview.Goal.env gl in
+          let sigma = Proofview.Goal.sigma gl in
+          let t = Proofview.Goal.concl gl in
+          Proofview.V82.tactic (fun gl -> change_concl (aux env sigma i t) gl)
+        end in
+      (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
         tac
         (Array.map rename_branch nn)
   | _ ->
       tac
 
-let elimination_clause_scheme with_evars ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause gl =
-  let elimclause = make_clenv_binding (pf_env gl) (project gl) (elim, elimty) bindings in
+let elimination_clause_scheme with_evars ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause =
+  Proofview.Goal.raw_enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv =
     (match kind_of_term (nth_arg i elimclause.templval.rebus) with
        | Meta mv -> mv
@@ -914,7 +935,8 @@ let elimination_clause_scheme with_evars ?(flags=elim_flags ()) rename i (elim,
              (str "The type of elimination clause is not well-formed."))
   in
   let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
-  enforce_prop_bound_names rename (Proofview.V82.of_tactic (Clenvtac.res_pf elimclause' ~with_evars:with_evars ~flags)) gl
+  enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars:with_evars ~flags)
+  end
 
 (*
  * Elimination tactic with bindings and using an arbitrary
@@ -930,48 +952,58 @@ type eliminator = {
   elimbody : constr with_bindings
 }
 
-let general_elim_clause_gen elimtac indclause elim gl =
+let general_elim_clause_gen elimtac indclause elim =
+  Proofview.Goal.raw_enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
   let (elimc,lbindelimc) = elim.elimbody in
-  let elimt = pf_type_of gl elimc in
+  let elimt = Retyping.get_type_of env sigma elimc in
   let i =
     match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
-  elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause gl
+  elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause
+  end
 
-let general_elim with_evars clear_flag (c, lbindc) elim gl =
-  let ct = pf_type_of gl c in
-  let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
+let general_elim with_evars clear_flag (c, lbindc) elim =
+  Proofview.Goal.raw_enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let ct = Retyping.get_type_of env sigma c in
+  let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
   let elimtac = elimination_clause_scheme with_evars in
-  let indclause  = pf_apply make_clenv_binding gl (c, t) lbindc in
-  tclTHEN
+  let indclause  = make_clenv_binding env sigma (c, t) lbindc in
+  Tacticals.New.tclTHEN
     (general_elim_clause_gen elimtac indclause elim)
-    (Proofview.V82.of_tactic
-       (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
-    gl
+    (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
+  end
 
 (* Case analysis tactics *)
 
-let general_case_analysis_in_context with_evars clear_flag (c,lbindc) gl =
-  let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let sort = elimination_sort_of_goal gl in
+let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let concl = Proofview.Goal.concl gl in
+  let t = Retyping.get_type_of env sigma c in
+  let (mind,_) = reduce_to_quantified_ind env sigma t in
+  let sort = Tacticals.New.elimination_sort_of_goal gl in
   let sigma, elim =
-    if occur_term c (pf_concl gl) then
-      pf_apply build_case_analysis_scheme gl mind true sort
+    if occur_term c concl then
+      build_case_analysis_scheme env sigma mind true sort
     else
-      pf_apply build_case_analysis_scheme_default gl mind sort in
-  tclTHEN (tclEVARS sigma)
+      build_case_analysis_scheme_default env sigma mind sort in
+  Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma)
   (general_elim with_evars clear_flag (c,lbindc)
    {elimindex = None; elimbody = (elim,NoBindings);
-    elimrename = Some (false, constructors_nrealdecls (fst mind))}) gl
+    elimrename = Some (false, constructors_nrealdecls (fst mind))})
+  end
 
 let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
   match kind_of_term c with
     | Var id when lbindc == NoBindings ->
 	Tacticals.New.tclTHEN (try_intros_until_id_check id)
-	  (Proofview.V82.tactic
-             (general_case_analysis_in_context with_evars clear_flag cx))
+	  (general_case_analysis_in_context with_evars clear_flag cx)
     | _ ->
-	Proofview.V82.tactic
-          (general_case_analysis_in_context with_evars clear_flag cx)
+        general_case_analysis_in_context with_evars clear_flag cx
 
 let simplest_case c = general_case_analysis false None (c,NoBindings)
 
@@ -999,7 +1031,7 @@ let default_elim with_evars clear_flag (c,_ as cx) =
     (Proofview.Goal.raw_enter begin fun gl ->
       let evd, elim = find_eliminator c gl in
 	Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd)
-	  (Proofview.V82.tactic (general_elim with_evars clear_flag cx elim))
+	  (general_elim with_evars clear_flag cx elim)
     end)
     begin function
       | IsRecord ->
@@ -1011,9 +1043,8 @@ let default_elim with_evars clear_flag (c,_ as cx) =
 
 let elim_in_context with_evars clear_flag c = function
   | Some elim ->
-      Proofview.V82.tactic
-        (general_elim with_evars clear_flag c {elimindex = Some (-1); elimbody = elim;
-                                    elimrename = None})
+      general_elim with_evars clear_flag c
+        {elimindex = Some (-1); elimbody = elim; elimrename = None}
   | None -> default_elim with_evars clear_flag c
 
 let elim with_evars clear_flag (c,lbindc as cx) elim =
@@ -1044,8 +1075,11 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
     (* Set the hypothesis name in the message *)
     raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
 
-let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause gl =
-  let elimclause = make_clenv_binding (pf_env gl) (project gl) (elim, elimty) bindings in
+let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause =
+  Proofview.Goal.raw_enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
   let hypmv =
     try match List.remove Int.equal indmv (clenv_independent elimclause) with
@@ -1055,21 +1089,22 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (
           (str "The type of elimination clause is not well-formed.") in
   let elimclause'  = clenv_fchain ~flags indmv elimclause indclause in
   let hyp = mkVar id in
-  let hyp_typ = pf_type_of gl hyp in
-  let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
+  let hyp_typ = Retyping.get_type_of env sigma hyp in
+  let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
   let new_hyp_typ  = clenv_type elimclause'' in
   if eq_constr hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in"
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
-  clenv_refine_in with_evars None id elimclause'' gl
+  clenv_refine_in with_evars None id elimclause''
+  end
 
 let general_elim_clause with_evars flags id c e =
   let elim = match id with
   | None -> elimination_clause_scheme with_evars ~flags
   | Some id -> elimination_in_clause_scheme with_evars ~flags id
   in
-  Proofview.V82.tactic (fun gl -> general_elim_clause_gen elim c e gl)
+  general_elim_clause_gen elim c e
 
 (* Apply a tactic below the products of the conclusion of a lemma *)
 
@@ -1114,100 +1149,143 @@ let make_projection env sigma params cstr sign elim i n c u =
       | None -> None
   in elim
 
-let descend_in_conjunctions tac exit c gl =
+let descend_in_conjunctions tac exit c =
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
   try
-    let ((ind,u),t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+    let t = Retyping.get_type_of env sigma c in
+    let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
     let sign,ccl = decompose_prod_assum t in
     match match_with_tuple ccl with
     | Some (_,_,isrec) ->
 	let n = (constructors_nrealargs ind).(0) in
-	let sort = elimination_sort_of_goal gl in
-	let id = fresh_id [] (Id.of_string "H") gl in
-	let IndType (indf,_) = pf_apply find_rectype gl ccl in
+	let sort = Tacticals.New.elimination_sort_of_goal gl in
+	let IndType (indf,_) = find_rectype env sigma ccl in
 	let (_,inst), params = dest_ind_family indf in
-	let cstr = (get_constructors (pf_env gl) indf).(0) in
+	let cstr = (get_constructors env indf).(0) in
 	let elim =
 	  try DefinedRecord (Recordops.lookup_projections ind)
 	  with Not_found ->
-	    let elim = pf_apply build_case_analysis_scheme gl (ind,u) false sort in
+	    let elim = build_case_analysis_scheme env sigma (ind,u) false sort in
 	    NotADefinedRecordUseScheme (snd elim) in
-	tclFIRST
-	  (List.init n (fun i gl ->
-	    match pf_apply make_projection gl params cstr sign elim i n c u with
-	    | None -> tclFAIL 0 (mt()) gl
+	Tacticals.New.tclFIRST
+	  (List.init n (fun i ->
+            Proofview.Goal.raw_enter begin fun gl ->
+            let env = Proofview.Goal.env gl in
+            let sigma = Proofview.Goal.sigma gl in
+	    match make_projection env sigma params cstr sign elim i n c u with
+	    | None -> Tacticals.New.tclFAIL 0 (mt())
 	    | Some (p,pt) ->
-	    tclTHENS
-	      (internal_cut id pt)
-	      [refine p; (* Might be ill-typed due to forbidden elimination. *)
-	       tclTHEN (tac (not isrec) (mkVar id)) (thin [id])] gl))
-	  gl
+	    Tacticals.New.tclTHENS
+	      (internal_cut (NamingAvoid []) pt)
+	      [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *)
+	       Tacticals.New.onLastHypId (fun id ->
+                 Tacticals.New.tclTHEN
+                   (tac (not isrec) (mkVar id))
+                   (Proofview.V82.tactic (thin [id])))]
+            end))
     | None ->
 	raise Exit
   with RefinerError _|UserError _|Exit -> exit ()
+  end
 
 (****************************************************)
 (*            Resolution tactics                    *)
 (****************************************************)
 
-let solve_remaining_apply_goals gl = 
+let solve_remaining_apply_goals =
+  Proofview.Goal.enter begin fun gl ->
   if !apply_solve_class_goals then
     try 
-      let env = pf_env gl and sigma = project gl and concl = pf_concl gl in
-	if Typeclasses.is_class_type sigma concl then
-          let evd', c' = Typeclasses.resolve_one_typeclass env sigma concl in
-	    (tclTHEN (tclEVARS evd') (refine_no_check c')) gl
-	else tclIDTAC gl
-    with Not_found -> tclIDTAC gl
-  else tclIDTAC gl
-    
-let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) gl0 =
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      let concl = Proofview.Goal.concl gl in
+      if Typeclasses.is_class_type sigma concl then
+        let evd', c' = Typeclasses.resolve_one_typeclass env sigma concl in
+	Tacticals.New.tclTHEN
+          (Proofview.V82.tclEVARS evd')
+          (Proofview.V82.tactic (refine_no_check c'))
+	else Proofview.tclUNIT ()
+    with Not_found -> Proofview.tclUNIT ()
+  else Proofview.tclUNIT ()
+  end
+  
+let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) =
+  Proofview.Goal.enter begin fun gl ->
+  let concl = Proofview.Goal.concl gl in
   let flags =
     if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   (* The actual type of the theorem. It will be matched against the
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
-  let concl_nprod = nb_prod (pf_concl gl0) in
-  let rec try_main_apply with_destruct c gl =
-    let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in
+  let concl_nprod = nb_prod concl in
+  let rec try_main_apply with_destruct c =
+    Proofview.Goal.raw_enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+
+    let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in
     let try_apply thm_ty nprod =
-      let n = nb_prod thm_ty - nprod in
-	if n<0 then error "Applied theorem has not enough premisses.";
-	let clause = pf_apply make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
-	  Proofview.V82.of_tactic (Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags) gl
+      try
+        let n = nb_prod thm_ty - nprod in
+        if n<0 then error "Applied theorem has not enough premisses.";
+        let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
+        Clenvtac.res_pf clause ~with_evars ~flags
+      with UserError _ as exn ->
+        Proofview.tclZERO exn
     in
-      try try_apply thm_ty0 concl_nprod
-      with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
+    Proofview.tclORELSE
+      (try_apply thm_ty0 concl_nprod)
+      (function PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
 	let rec try_red_apply thm_ty =
-	  try
+          try 
             (* Try to head-reduce the conclusion of the theorem *)
-            let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in
-              try try_apply red_thm concl_nprod
-              with PretypeError _|RefinerError _|UserError _|Failure _ ->
+            let red_thm = try_red_product env sigma thm_ty in
+            Proofview.tclORELSE
+              (try_apply red_thm concl_nprod)
+              (function PretypeError _|RefinerError _|UserError _|Failure _ ->
 		try_red_apply red_thm
-	  with Redelimination ->
+              | exn -> raise exn)
+          with Redelimination ->
             (* Last chance: if the head is a variable, apply may try
 	       second order unification *)
-	    try if not (Int.equal concl_nprod 0) then try_apply thm_ty 0 else raise Exit
-	    with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
+            let tac =
 	      if with_destruct then
                 descend_in_conjunctions
-                  try_main_apply (fun _ -> Loc.raise loc exn) c gl
+                  try_main_apply
+                  (fun _ -> Proofview.tclZERO (Loc.add_loc exn0 loc)) c
 	      else
-		Loc.raise loc exn
+		Proofview.tclZERO (Loc.add_loc exn0 loc) in
+            if not (Int.equal concl_nprod 0) then
+              try
+                Proofview.tclORELSE
+                  (try_apply thm_ty 0)
+                  (function PretypeError _|RefinerError _|UserError _|Failure _->
+                    tac
+                  | exn -> raise exn)
+              with UserError _ | Exit ->
+                tac
+            else
+              tac
 	in try_red_apply thm_ty0
+      | exn -> raise exn)
+    end
   in
-    tclTHENLIST [
+    Tacticals.New.tclTHENLIST [
       try_main_apply with_destruct c;
       solve_remaining_apply_goals;
-      Proofview.V82.of_tactic
-        (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
-    ] gl0
+      apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
+    ]
+  end
 
 let rec apply_with_bindings_gen b e = function
-  | [] -> tclIDTAC
+  | [] -> Proofview.tclUNIT ()
   | [k,cb] -> general_apply b b e k cb
   | (k,cb)::cbl ->
-      tclTHENLAST (general_apply b b e k cb) (apply_with_bindings_gen b e cbl)
+      Tacticals.New.tclTHENLAST
+        (general_apply b b e k cb)
+        (apply_with_bindings_gen b e cbl)
 
 let apply_with_bindings cb = apply_with_bindings_gen false false [None,(dloc,cb)]
 
@@ -1249,8 +1327,8 @@ let progress_with_clause flags innerclause clause =
   try List.find_map f ordered_metas
   with Not_found -> error "Unable to unify."
 
-let apply_in_once_main flags innerclause (d,lbind) gl =
-  let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
+let apply_in_once_main flags innerclause env sigma (d,lbind) =
+  let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with e when Errors.noncritical e ->
@@ -1258,26 +1336,32 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
     try aux (clenv_push_prod clause)
     with NotExtensibleClause -> raise e
   in
-  aux (pf_apply make_clenv_binding gl (d,thm) lbind)
+  aux (make_clenv_binding env sigma (d,thm) lbind)
 
-let apply_in_once sidecond_first with_delta with_destruct with_evars hyp_clear_flag
-    id (clear_flag,(loc,(d,lbind))) gl0 =
+let apply_in_once sidecond_first with_delta with_destruct with_evars naming
+    id (clear_flag,(loc,(d,lbind))) =
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
   let flags = if with_delta then elim_flags () else elim_no_delta_flags () in
-  let t' = pf_get_hyp_typ gl0 id in
-  let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
-  let rec aux with_destruct c gl =
+  let t' = Tacmach.New.pf_get_hyp_typ id gl in
+  let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
+  let rec aux with_destruct c =
+    Proofview.Goal.raw_enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
     try
-      let clause = apply_in_once_main flags innerclause (c,lbind) gl in
-      tclTHEN
-        (clenv_refine_in ~sidecond_first with_evars hyp_clear_flag id clause)
-        (Proofview.V82.of_tactic
-           (apply_clear_request clear_flag false c))
-        gl
+      let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in
+      Tacticals.New.tclTHEN
+        (clenv_refine_in ~sidecond_first with_evars naming id clause)
+        (apply_clear_request clear_flag false c)
     with e when with_destruct ->
       let e = Errors.push e in
-      descend_in_conjunctions aux (fun _ -> raise e) c gl
+      descend_in_conjunctions aux (fun _ -> raise e) c
+    end
   in
-  aux with_destruct d gl0
+  aux with_destruct d
+  end
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
@@ -1436,7 +1520,7 @@ let specialize (c,lbind) g =
        | Var id when Id.List.mem id (pf_ids_of_hyps g) ->
 	   tclTHEN tac
 	     (tclTHENFIRST
-	       (fun g -> internal_cut_replace id (pf_type_of g term) g)
+	       (fun g -> Proofview.V82.of_tactic (internal_cut_replace (NamingMustBe (dloc,id)) (pf_type_of g term)) g)
 	       (exact_no_check term)) g
        | _ -> tclTHEN tac
 	   (tclTHENLAST
@@ -1487,7 +1571,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
 	(Proofview.Goal.env gl) (Proofview.Goal.sigma gl) (fst mind, i) in
       let cons = mkConstructU cons in
 	
-      let apply_tac = Proofview.V82.tactic (general_apply true false with_evars None (dloc,(cons,lbind))) in
+      let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in
 	(Tacticals.New.tclTHENLIST
            [Proofview.V82.tclEVARS sigma; Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
   end
@@ -1500,7 +1584,7 @@ let one_constructor i lbind = constructor_tac false None i lbind
  *)
 
 let rec tclANY tac = function
-| [] -> Proofview.tclZERO (Errors.UserError ("", str "No applicable tactic."))
+| [] -> Tacticals.New.tclZEROMSG (str "No applicable tactic.")
 | arg :: l ->
   Proofview.tclOR (tac arg) (fun _ -> tclANY tac l)
 
@@ -1618,7 +1702,7 @@ let rewrite_hyp l2r id =
         else
           Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
     | _ ->
-        Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation."))
+        Tacticals.New.tclZEROMSG (str"Cannot find a known equation.")
   end
 
 let rec explicit_intro_names = function
@@ -1664,31 +1748,31 @@ let rec intros_patterns b avoid ids thin destopt bound n tac = function
   | [] when fit_bound n bound -> tac ids thin
   | [] ->
       (* Behave as IntroAnonymous *)
-      intro_then_gen dloc (IntroAvoid avoid)
+      intro_then_gen (NamingAvoid avoid)
 	destopt true false
         (fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac [])
   | (loc,pat) :: l ->
   if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
   match pat with
   | IntroWildcard ->
-      intro_then_gen loc (IntroBasedOn(wild_id,avoid@explicit_intro_names l))
+      intro_then_gen (NamingBasedOn(wild_id,avoid@explicit_intro_names l))
 	MoveLast true false
         (fun id -> intros_patterns b avoid ids ((loc,id)::thin) destopt bound (n+1) tac l)
   | IntroIdentifier id ->
       check_thin_clash_then id thin avoid (fun thin ->
-        intro_then_gen loc (IntroMustBe id) destopt true false
+        intro_then_gen (NamingMustBe (loc,id)) destopt true false
           (fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac l))
   | IntroAnonymous ->
-      intro_then_gen loc (IntroAvoid (avoid@explicit_intro_names l))
+      intro_then_gen (NamingAvoid (avoid@explicit_intro_names l))
 	destopt true false
         (fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac l)
   | IntroFresh id ->
       (* todo: avoid thinned names to interfere with generation of fresh name *)
-      intro_then_gen loc (IntroBasedOn (id, avoid@explicit_intro_names l))
+      intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l))
 	destopt true false
         (fun id -> intros_patterns b avoid (id::ids) thin destopt bound (n+1) tac l)
   | IntroForthcoming onlydeps ->
-      intro_forthcoming_then_gen loc (IntroAvoid (avoid@explicit_intro_names l))
+      intro_forthcoming_then_gen (NamingAvoid (avoid@explicit_intro_names l))
 	  destopt onlydeps n bound
         (fun ids -> intros_patterns b avoid ids thin destopt bound (n+List.length ids) tac l)
   | IntroOrAndPattern ll ->
@@ -1700,7 +1784,7 @@ let rec intros_patterns b avoid ids thin destopt bound n tac = function
 	(intro_decomp_eq loc l' thin
 	   (fun thin bound' -> intros_patterns b avoid ids thin destopt bound' 0 (fun ids thin -> intros_patterns b avoid ids thin destopt bound (n+1) tac l)))
   | IntroRewrite l2r ->
-      intro_then_gen loc (IntroAvoid(avoid@explicit_intro_names l))
+      intro_then_gen (NamingAvoid(avoid@explicit_intro_names l))
 	MoveLast true false
         (fun id ->
 	  Tacticals.New.tclTHENLAST (* Skip the side conditions of the rewriting step *)
@@ -1733,63 +1817,64 @@ let intro_patterns = function
 (*   Other cut tactics    *)
 (**************************)
 
-let make_id s = new_fresh_id [] (default_id_of_sort s)
-
-let prepare_intros s ipat gl =
-  let make_id s = make_id s gl in
-  let fresh_id l id = new_fresh_id l id gl in
-  match ipat with
-  | None ->
-      make_id s , Proofview.tclUNIT ()
-  | Some (loc,ipat) -> match ipat with
-  | IntroIdentifier id ->
-      id, Proofview.tclUNIT ()
-  | IntroAnonymous ->
-      make_id s  , Proofview.tclUNIT ()
-  | IntroFresh id ->
-      fresh_id [] id , Proofview.tclUNIT ()
+let rec prepare_naming loc = function
+  | IntroIdentifier id -> NamingMustBe (loc,id)
+  | IntroAnonymous -> NamingAvoid []
+  | IntroFresh id -> NamingBasedOn (id,[])
   | IntroWildcard ->
-      let id = make_id s in
-      id , clear_wildcards [dloc,id]
+      error "Did you really mind erasing the newly generated hypothesis?"
+  | IntroRewrite _
+  | IntroOrAndPattern _
+  | IntroInjection _
+  | IntroForthcoming _ -> assert false
+
+let rec prepare_intros_loc loc dft = function
+  | IntroIdentifier _
+  | IntroAnonymous
+  | IntroFresh _
+  | IntroWildcard as ipat ->
+      prepare_naming loc ipat,
+      (fun _ -> Proofview.tclUNIT ())
   | IntroRewrite l2r ->
-      let id = make_id s in
-      id, Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
+      prepare_naming loc dft,
+      (fun id -> Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl)
   | IntroOrAndPattern ll ->
-      make_id s,
-      Tacticals.New.onLastHypId
-	(intro_or_and_pattern loc true ll []
-	  (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0 (fun _ l -> clear_wildcards l)))
+      prepare_naming loc dft,
+      (intro_or_and_pattern loc true ll []
+	 (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0
+           (fun _ l -> clear_wildcards l)))
   | IntroInjection l ->
-      make_id s,
-      Tacticals.New.onLastHypId
-	(intro_decomp_eq loc l []
-	  (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0 (fun _ l -> clear_wildcards l)))
+      prepare_naming loc dft,
+      (intro_decomp_eq loc l []
+	 (fun thin bound -> intros_patterns true [] [] thin MoveLast bound 0
+           (fun _ l -> clear_wildcards l)))
   | IntroForthcoming _ -> user_err_loc
-      (loc,"",str "Introduction pattern for one hypothesis expected")
+      (loc,"",str "Introduction pattern for one hypothesis expected.")
+
+let prepare_intros dft = function
+  | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
+  | Some (loc,ipat) -> prepare_intros_loc loc dft ipat
 
 let ipat_of_name = function
   | Anonymous -> None
   | Name id -> Some (dloc, IntroIdentifier id)
 
-let allow_replace c = function (* A rather arbitrary condition... *)
-  | Some (_, IntroIdentifier id) ->
-      let c = fst (decompose_app ((strip_lam_assum c))) in
-      if isVar c && Id.equal (destVar c) id then Some id else None
-  | _ ->
-      None
+ let head_ident c =
+   let c = fst (decompose_app ((strip_lam_assum c))) in
+   if isVar c then Some (destVar c) else None
+
+let do_replace id = function
+  | NamingMustBe (_,id') when Option.equal Id.equal id (Some id') -> true
+  | _ -> false
 
 let assert_as first ipat c =
-  Proofview.Goal.raw_enter begin fun gl ->
-  let hnf_type_of = Tacmach.New.pf_hnf_type_of gl in
-  match kind_of_term (hnf_type_of c) with
-  | Sort s ->
-      let (id,tac) = prepare_intros s ipat gl in
-      let repl = not (Option.is_empty (allow_replace c ipat)) in
-      Tacticals.New.tclTHENS
-	(Proofview.V82.tactic ((if first then internal_cut_gen else internal_cut_rev_gen) repl id c))
-	(if first then [Proofview.tclUNIT (); tac] else [tac; Proofview.tclUNIT ()])
-  | _  -> Proofview.tclZERO (Errors.UserError ("",str"Not a proposition or a type."))
-  end
+  let naming,tac = prepare_intros IntroAnonymous ipat in
+  let repl = do_replace (head_ident c) naming in
+  Tacticals.New.tclTHENS
+    ((if first then internal_cut_gen
+      else internal_cut_rev_gen) repl naming c)
+    (if first then [Proofview.tclUNIT (); Tacticals.New.onLastHypId tac]
+     else [Tacticals.New.onLastHypId tac; Proofview.tclUNIT ()])
 
 let assert_tac na = assert_as true (ipat_of_name na)
 let enough_tac na = assert_as false (ipat_of_name na)
@@ -1814,28 +1899,27 @@ let as_tac id ipat = match ipat with
   | None -> Proofview.tclUNIT ()
 
 let tclMAPLAST tacfun l =
-  let tacfun x = Proofview.V82.tactic (tacfun x) in
   List.fold_right (fun x -> Tacticals.New.tclTHENLAST (tacfun x)) l (Proofview.tclUNIT())
 
 let tclMAPFIRST tacfun l =
-  let tacfun x = Proofview.V82.tactic (tacfun x) in
   List.fold_right (fun x -> Tacticals.New.tclTHENFIRST (tacfun x)) l (Proofview.tclUNIT())
 
 let general_apply_in sidecond_first with_delta with_destruct with_evars
     with_clear id lemmas ipat =
+  let tac (naming,lemma) =
+    apply_in_once sidecond_first with_delta with_destruct with_evars
+      naming id lemma in
+  let naming,ipat_tac = prepare_intros (IntroIdentifier id) ipat in
+  let clear = do_replace (Some id) naming in
+  let lemmas_target =
+    let last,first = List.sep_last lemmas in
+    List.map (fun lem -> (None,lem)) first @ [(Some (clear,naming),last)]
+  in
   if sidecond_first then
     (* Skip the side conditions of the applied lemma *)
-    Tacticals.New.tclTHENLAST
-      (tclMAPLAST
-	(apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id)
-	lemmas)
-      (as_tac id ipat)
+    Tacticals.New.tclTHENLAST (tclMAPLAST tac lemmas_target) (ipat_tac id)
   else
-    Tacticals.New.tclTHENFIRST
-      (tclMAPFIRST
-	(apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id)
-	lemmas)
-      (as_tac id ipat)
+    Tacticals.New.tclTHENFIRST (tclMAPFIRST tac lemmas_target) (ipat_tac id)
 
 let apply_in simple with_evars clear_flag id lemmas ipat =
   general_apply_in false simple simple with_evars clear_flag id lemmas ipat
@@ -1888,7 +1972,7 @@ let letin_tac_gen with_eq abs ty =
 	  let sigma, _ = Typing.e_type_of env sigma term in
             sigma, term,
             Tacticals.New.tclTHEN
-	      (intro_gen loc (IntroMustBe heq) (decode_hyp lastlhyp) true false)
+	      (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
 	      (Proofview.V82.tactic (thin_body [heq;id]))
       | None ->
 	  (Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
@@ -1899,7 +1983,7 @@ let letin_tac_gen with_eq abs ty =
 	  Tacticals.New.tclTHENLIST
 	    [ Proofview.V82.tclEVARS sigma;
 	      Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
-              intro_gen dloc (IntroMustBe id) (decode_hyp lastlhyp) true false;
+              intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false;
               Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
               eq_tac ]))
   end
@@ -3333,7 +3417,8 @@ let induction_tac with_evars elim (varname,lbind) typ gl =
   let indclause = pf_apply make_clenv_binding gl (mkVar varname,typ) lbind  in
   let i = match i with None -> index_of_ind_arg elimt | Some i -> i in
   let elimc = mkCast (elimc, DEFAULTcast, elimt) in
-  elimination_clause_scheme with_evars rename i (elimc, elimt, lbindelimc) indclause gl
+  Proofview.V82.of_tactic
+    (elimination_clause_scheme with_evars rename i (elimc, elimt, lbindelimc) indclause) gl
 
 let induction_from_context clear_flag isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
   inhyps =
@@ -3376,7 +3461,7 @@ let induction_without_atomization isrec with_evars elim names lid =
   in
   let nlid = List.length lid in
   if not (Int.equal nlid awaited_nargs)
-  then Proofview.tclZERO (Errors.UserError ("", str"Not the right number of induction arguments."))
+  then Tacticals.New.tclZEROMSG (str"Not the right number of induction arguments.")
   else
     Proofview.tclTHEN (Proofview.V82.tclEVARS sigma)
       (induction_from_context_l with_evars elim_info lid names)
@@ -3691,11 +3776,9 @@ let symmetry_red allowred =
   match_with_equation concl >>= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->
-      Proofview.V82.tactic begin
-        tclTHEN
-          (convert_concl_no_check concl DEFAULTcast)
-          (pf_constr_of_global eq_data.sym apply)
-      end
+      Tacticals.New.tclTHEN
+        (Proofview.V82.tactic (convert_concl_no_check concl DEFAULTcast))
+        (Tacticals.New.pf_constr_of_global eq_data.sym apply)
   | None,eq,eq_kind -> prove_symmetry eq eq_kind
   end
 
@@ -3723,7 +3806,7 @@ let symmetry_in id =
           | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
         Tacticals.New.tclTHENS (cut (it_mkProd_or_LetIn symccl sign))
           [ Proofview.V82.tactic (intro_replacing id);
-            Tacticals.New.tclTHENLIST [ intros; symmetry; Proofview.V82.tactic (apply (mkVar id)); assumption ] ]
+            Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
     end
     begin function
       | NoEquationFound -> Hook.get forward_setoid_symmetry_in id
@@ -3785,16 +3868,14 @@ let transitivity_red allowred t =
   match_with_equation concl >>= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->
-      Proofview.V82.tactic begin
-        tclTHEN
-          (convert_concl_no_check concl DEFAULTcast)
-          (match t with
-	  | None -> pf_constr_of_global eq_data.trans eapply
-	  | Some t -> pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
-      end
-  | None,eq,eq_kind ->
+      Tacticals.New.tclTHEN
+        (Proofview.V82.tactic (convert_concl_no_check concl DEFAULTcast))
+        (match t with
+	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply
+	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
+   | None,eq,eq_kind ->
       match t with
-      | None -> Proofview.tclZERO (Errors.UserError ("",str"etransitivity not supported for this relation."))
+      | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
       | Some t -> prove_transitivity eq eq_kind t
   end
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f58e218be..f50e52a19 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -175,14 +175,14 @@ val revert        : Id.t list -> unit Proofview.tactic
 val apply_type : constr -> constr list -> tactic
 val bring_hyps : named_context -> unit Proofview.tactic
 
-val apply                 : constr -> tactic
-val eapply                : constr -> tactic
+val apply                 : constr -> unit Proofview.tactic
+val eapply                : constr -> unit Proofview.tactic
 
 val apply_with_bindings_gen :
-  advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> tactic
+  advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> unit Proofview.tactic
 
-val apply_with_bindings   : constr with_bindings -> tactic
-val eapply_with_bindings  : constr with_bindings -> tactic
+val apply_with_bindings   : constr with_bindings -> unit Proofview.tactic
+val eapply_with_bindings  : constr with_bindings -> unit Proofview.tactic
 
 val cut_and_apply         : constr -> unit Proofview.tactic
 
@@ -251,7 +251,7 @@ type eliminator = {
 }
 
 val general_elim  : evars_flag -> clear_flag ->
-  constr with_bindings -> eliminator -> tactic
+  constr with_bindings -> eliminator -> unit Proofview.tactic
 
 val general_elim_clause : evars_flag -> unify_flags -> identifier option ->
   clausenv -> eliminator -> unit Proofview.tactic
@@ -336,8 +336,8 @@ val intros_transitivity         : constr option -> unit Proofview.tactic
 
 val cut                         : constr -> unit Proofview.tactic
 val cut_intro                   : constr -> unit Proofview.tactic
-val assert_replacing            : Id.t -> types -> tactic -> tactic
-val cut_replacing               : Id.t -> types -> tactic -> tactic
+val assert_replacing            : Id.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
+val cut_replacing               : Id.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
 
 val assert_as : bool -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
 val forward   : bool -> unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
@@ -386,8 +386,8 @@ module Simple : sig
   val generalize      : constr list -> tactic
   val generalize_gen  : (constr Locus.with_occurrences * Name.t) list -> tactic
 
-  val apply  : constr -> tactic
-  val eapply : constr -> tactic
+  val apply  : constr -> unit Proofview.tactic
+  val eapply : constr -> unit Proofview.tactic
   val elim   : constr -> unit Proofview.tactic
   val case   : constr -> unit Proofview.tactic
   val apply_in : identifier -> constr -> unit Proofview.tactic
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index d972fb929..8d040c257 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -314,7 +314,7 @@ let coq_nnpp_path =
 
 let tauto_classical flags nnpp =
   Proofview.tclORELSE
-    (Tacticals.New.tclTHEN (Proofview.V82.tactic (apply nnpp)) (tauto_intuitionistic flags))
+    (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags))
     begin function
       | UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed."))
       | e -> Proofview.tclZERO e
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 15b370b06..c3dc8f89d 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -387,7 +387,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
            in
            Tacticals.New.tclTHENLIST [
              Proofview.tclEFFECTS eff;
-             Equality.replace p q ; Proofview.V82.tactic (apply app) ; Auto.default_auto]
+             Equality.replace p q ; apply app ; Auto.default_auto]
   end
 
 (* used in the bool -> leib side *)
@@ -456,7 +456,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
                 Tacticals.New.tclTHENLIST [
                   Proofview.tclEFFECTS eff;
                   Equality.replace_by t1 t2
-                    (Tacticals.New.tclTHEN (Proofview.V82.tactic (apply app)) (Auto.default_auto)) ;
+                    (Tacticals.New.tclTHEN (apply app) (Auto.default_auto)) ;
                   aux q1 q2 ]
               )
         )
@@ -727,7 +727,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
 		     intros; (Proofview.V82.tactic simpl_in_concl);
                      Auto.default_auto;
                      Tacticals.New.tclREPEAT (
-                      Tacticals.New.tclTHENLIST [Proofview.V82.tactic (apply (andb_true_intro()));
+                      Tacticals.New.tclTHENLIST [apply (andb_true_intro());
                                   simplest_split ;Auto.default_auto ]
                       );
                       Proofview.Goal.enter begin fun gls ->
@@ -892,7 +892,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
 	    (* left *)
 	    Tacticals.New.tclTHENLIST [
 	      simplest_left;
-              Proofview.V82.tactic (apply (mkApp(blI,Array.map(fun x->mkVar x) xargs)));
+              apply (mkApp(blI,Array.map(fun x->mkVar x) xargs));
               Auto.default_auto
             ]
             ;
@@ -908,7 +908,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
               assert_by (Name freshH3)
 		(mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
 		(Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs)));
+		  apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs));
                   Auto.default_auto
 		]);
 	      Equality.general_rewrite_bindings_in true