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)

9 files changed, 91 insertions, 90 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index dbd89019e2..e6a8411534 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 70aaa0c0fc..3151a7ec75 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 7c134da7ac..a77b1d60a9 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 11107385da..25451fd924 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 1981fb837b..7f0db547d3 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 5682c2aa47..4fcc65bda9 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 1fa16a3015..ff35c98124 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 271cade276..48c853029e 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 e22816c136..1835b6cc99 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"];