Put the "generalize" tactic in the monad.

15 files changed, 73 insertions, 76 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 1f3eb1335..e03cc675e 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -728,7 +728,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
        Tacticals.New.tclTHENLIST
-         [Proofview.V82.tactic (Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
+         [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
           Proofview.Goal.nf_enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 5aff262aa..7ec1b2ca0 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1755,7 +1755,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Tacticals.New.tclWITHHOLES false
         (name_atomic ~env
           (TacGeneralize cl)
-          (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma
+          (Tactics.generalize_gen cl)) sigma
       end }
   | TacLetTac (na,c,clp,b,eqpat) ->
       Proofview.V82.nf_evar_goals <*>
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index a6b338164..de06af005 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1289,7 +1289,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 		       (fun id ->
 			  hrec_for (out_name fix_name) per_info gls1 id)
 		       recs in
-		     generalize hrecs gls1
+		     Proofview.V82.of_tactic (generalize hrecs) gls1
 	       end;
 	       match bro with
 		   None ->
@@ -1365,7 +1365,7 @@ let end_tac et2 gls =
 		(default_justification (List.map mkVar clauses))
 	  | ET_Induction,EK_nodep ->
 	      tclTHENLIST
-		[generalize (pi.per_args@[pi.per_casee]);
+		[Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]));
 		 Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args))));
 		 default_justification (List.map mkVar clauses)]
 	  | ET_Case_analysis,EK_dep tree ->
@@ -1377,7 +1377,7 @@ let end_tac et2 gls =
 		   (initial_instance_stack clauses) [pi.per_casee] 0 tree
 	  | ET_Induction,EK_dep tree ->
 	      let nargs = (List.length pi.per_args) in
-		tclTHEN (generalize (pi.per_args@[pi.per_casee]))
+		tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])))
 		  begin
 		    fun gls0 ->
 		      let fix_id =
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 0e2a40245..5eff2f277 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -135,9 +135,9 @@ let left_instance_tac (inst,id) continue seq=
 	    [tclTHENLIST
 	       [Proofview.V82.of_tactic introf;
                 pf_constr_of_global id (fun idc ->
-		(fun gls->generalize
+		(fun gls-> Proofview.V82.of_tactic (generalize
 		   [mkApp(idc,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls));
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
 		Proofview.V82.of_tactic introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
@@ -158,10 +158,10 @@ let left_instance_tac (inst,id) continue seq=
 		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when Errors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
-		    tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
+		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
 	    else
 	      pf_constr_of_global id (fun idc ->
-		generalize [mkApp(idc,[|t|])])
+		Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
 	  in
 	    tclTHENLIST
 	      [special_generalize;
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index d05e9484a..92b6e828e 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -67,7 +67,7 @@ let ll_atom_tac a backtrack id continue seq=
       tclTHENLIST
 	[pf_constr_of_global (find_left a seq) (fun left ->
 	  pf_constr_of_global id (fun id -> 
-	    generalize [mkApp(id, [|left|])]));
+	    Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])])));
 	 clear_global id;
 	 Proofview.V82.of_tactic intro]
     with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -135,7 +135,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
        let newhyps idc =List.init lp (myterm idc) in
 	 tclIFTHENELSE
 	   (tclTHENLIST
-	      [pf_constr_of_global id (fun idc -> generalize (newhyps idc));
+	      [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
 	       clear_global id;
 	       tclDO lp (Proofview.V82.of_tactic intro)])
 	   (wrap lp false continue seq) backtrack gl
@@ -153,7 +153,7 @@ let ll_arrow_tac a b c backtrack id continue seq=
 	  tclTHENS (Proofview.V82.of_tactic (cut cc))
             [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
 	     tclTHENLIST
-	       [pf_constr_of_global id (fun idc -> generalize [d idc]);
+	       [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
 		clear_global id;
 		Proofview.V82.of_tactic introf;
 		Proofview.V82.of_tactic introf;
@@ -192,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq=
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
-		tclTHEN (generalize [term]) (Proofview.V82.of_tactic (clear [id0])) gls));
+		tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
 	   clear_global id;
 	   Proofview.V82.of_tactic intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0b7a1e646..879145c2f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -704,7 +704,7 @@ let build_proof
 		  in
 		  tclTHENSEQ
 		    [
-		      generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+		      Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)));
 		      thin dyn_infos.rec_hyps;
 		      Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
 		      (fun g -> observe_tac "toto" (
@@ -934,7 +934,7 @@ let generalize_non_dep hyp g =
   in
 (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
   tclTHEN
-    ((* observe_tac "h_generalize" *) (generalize  (List.map mkVar to_revert) ))
+    ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize  (List.map mkVar to_revert) )))
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
@@ -942,7 +942,7 @@ let id_of_decl decl = Nameops.out_name (get_name decl)
 let var_of_decl decl = mkVar (id_of_decl decl)
 let revert idl =
   tclTHEN
-    (generalize (List.map mkVar idl))
+    (Proofview.V82.of_tactic (generalize (List.map mkVar idl)))
     (thin idl)
 
 let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num =
@@ -1564,7 +1564,7 @@ let prove_principle_for_gen
     Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
   in
   let revert l =
-    tclTHEN (Tactics.generalize (List.map mkVar l)) (Proofview.V82.of_tactic (clear l))
+    tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
   in
   let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
   let prove_rec_arg_acc g =
@@ -1610,7 +1610,7 @@ let prove_principle_for_gen
       in
       tclTHENSEQ
 	[
-	  generalize [lemma];
+	  Proofview.V82.of_tactic (generalize [lemma]);
 	  Proofview.V82.of_tactic (Simple.intro hid);
 	  Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
 	  (fun g ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index fde1b7e70..72529fbbe 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -465,7 +465,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | LocalAssum (id,t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id])
+	   (Termops.occur_var (pf_env g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -715,7 +715,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	       })
 	    Locusops.onConcl)
 	  ;
-	  generalize (List.map mkVar ids);
+	  Proofview.V82.of_tactic (generalize (List.map mkVar ids));
 	  thin ids
 	]
       else
@@ -754,7 +754,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     tclTHENSEQ
       [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
-	(generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
+	(Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
 	Proofview.V82.of_tactic (Simple.intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
 	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
@@ -937,7 +937,7 @@ let revert_graph kn post_tac hid g =
 		  let f_args,res = Array.chop (Array.length args - 1) args in
 		  tclTHENSEQ
 		    [
-		      generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
+		      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
 		      thin [hid];
 		      Proofview.V82.of_tactic (Simple.intro hid);
 		      post_tac hid
@@ -981,7 +981,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	  in
 	  tclTHENSEQ[
 	    pre_tac hid;
-	    generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
+	    Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
 	    thin [hid];
 	    Proofview.V82.of_tactic (Simple.intro hid);
 	    Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c1c3801b4..10f08d3d1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -689,7 +689,7 @@ let mkDestructEq :
            to_revert_constr in
     pf_typel new_hyps (fun _ ->
     observe_tclTHENLIST (str "mkDestructEq")
-     [generalize new_hyps;
+     [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
         let changefun patvars = { run = fun sigma ->
           let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
@@ -1116,7 +1116,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       [observe_tac (str "generalize")
 		  (onNLastHypsId (nargs+1)
 		     (tclMAP (fun id ->
-			tclTHEN (Tactics.generalize [mkVar id]) (Proofview.V82.of_tactic (clear [id])))
+			tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
 		     ))
 	       ;
 		observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1)));
@@ -1306,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
 	   observe_tclTHENLIST (str "")
 	     [
-	       generalize [lemma];
+	       Proofview.V82.of_tactic (generalize [lemma]);
 	       Proofview.V82.of_tactic (Simple.intro hid);
 	       (fun g ->
 		  let ids = pf_ids_of_hyps g in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 5c0a8226a..0fcfbfc71 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1464,7 +1464,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
       ]
       (Tacmach.pf_concl gl))
    ;
-   Tactics.new_generalize env ;
+   Tactics.generalize env ;
    Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
   ] 
   end }
@@ -1726,7 +1726,7 @@ let micromega_gen
      | Some (ids,ff',res') -> 
       (Tacticals.New.tclTHENLIST
 	[
-	 Tactics.new_generalize (List.map Term.mkVar ids) ;
+	 Tactics.generalize (List.map Term.mkVar ids) ;
 	 micromega_order_change  spec res' 
 	  (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
 	])
@@ -1774,7 +1774,7 @@ let micromega_order_changer cert env ff  =
          ("__wit", cert, cert_typ)
         ]
         (Tacmach.pf_concl gl)));
-      Tactics.new_generalize env ;
+      Tactics.generalize env ;
       Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
      ]
   end }
@@ -1812,7 +1812,7 @@ let micromega_genr prover =
 	     (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in
            (Tacticals.New.tclTHENLIST
               [
-                Tactics.new_generalize (List.map Term.mkVar ids) ;
+                Tactics.generalize (List.map Term.mkVar ids) ;
                 micromega_order_changer res' env (abstract_wrt_formula ff' ff)
               ])
   with
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 0da630530..5f906a8da 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -13,5 +13,5 @@ DECLARE PLUGIN "nsatz_plugin"
 DECLARE PLUGIN "nsatz_plugin"
 
 TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute"  constr(lt) ] -> [ Proofview.V82.tactic (Nsatz.nsatz_compute lt) ]
+| [ "nsatz_compute"  constr(lt) ] -> [ Nsatz.nsatz_compute lt ]
 END
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index fc5054080..ab33a5d2c 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1067,12 +1067,12 @@ let replay_history tactic_normalisation =
 	  let p_initial = [P_APP 1;P_TYPE] in
 	  let tac= shuffle_mult_right p_initial e1.body k e2.body in
 	  Tacticals.New.tclTHENLIST [
-	    Proofview.V82.tactic (generalize_tac
+	    generalize_tac
 	      [mkApp (Lazy.force coq_OMEGA17, [|
 		val_of eq1;
 		val_of eq2;
 		mk_integer k;
-		mkVar id1; mkVar id2 |])]);
+		mkVar id1; mkVar id2 |])];
 	    Proofview.V82.tactic (mk_then tac);
 	    (intros_using [aux]);
 	    Proofview.V82.tactic (resolve_id aux);
@@ -1104,7 +1104,7 @@ let replay_history tactic_normalisation =
 		      mkVar (hyp_of_tag e1.id);
 		      mkVar (hyp_of_tag e2.id) |])
 	  in
-	  Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (generalize_tac [theorem]) (mk_then tac))) (solve_le)
+	  Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (generalize_tac [theorem])) (mk_then tac))) (solve_le)
       | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
 	  let id = hyp_of_tag e1.id in
 	  let eq1 = val_of(decompile e1)
@@ -1119,7 +1119,7 @@ let replay_history tactic_normalisation =
 	    [ Tacticals.New.tclTHENS
 	        (Tacticals.New.tclTHENLIST [
 		  (intros_using [aux]);
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA1,
 		      [| eq1; rhs; mkVar aux; mkVar id |])]);
 		  (clear [aux;id]);
@@ -1129,9 +1129,9 @@ let replay_history tactic_normalisation =
 		    (cut (mk_gt kk izero))
 		    [ Tacticals.New.tclTHENLIST [
 		        (intros_using [aux1; aux2]);
-		        (Proofview.V82.tactic (generalize_tac
+		        (generalize_tac
 			  [mkApp (Lazy.force coq_Zmult_le_approx,
-			    [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]));
+			    [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]);
 		        (clear [aux1;aux2;id]);
 		        (intros_using [id]);
 		        (loop l) ];
@@ -1157,7 +1157,7 @@ let replay_history tactic_normalisation =
 	    [ Tacticals.New.tclTHENS (cut (mk_gt kk dd))
 		[Tacticals.New.tclTHENLIST [
 		  (intros_using [aux2;aux1]);
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA4,
                       [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
 		  (clear [aux1;aux2]);
@@ -1187,7 +1187,7 @@ let replay_history tactic_normalisation =
 	      (cut state_eq)
 	      [Tacticals.New.tclTHENLIST [
 		(intros_using [aux1]);
-		Proofview.V82.tactic (generalize_tac
+		(generalize_tac
 		  [mkApp (Lazy.force coq_OMEGA18,
                     [| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
 		(clear [aux1;id]);
@@ -1202,7 +1202,7 @@ let replay_history tactic_normalisation =
 		 (cut (mk_gt kk izero))
 		 [Tacticals.New.tclTHENLIST [
 		   (intros_using [aux2;aux1]);
-		   Proofview.V82.tactic (generalize_tac
+		   (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA3,
 		       [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
 		   (clear [aux1;aux2;id]);
@@ -1229,7 +1229,7 @@ let replay_history tactic_normalisation =
 	    (cut (mk_eq eq1 (mk_inv eq2)))
 	    [Tacticals.New.tclTHENLIST [
 	      (intros_using [aux]);
-	      Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
+	      (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
 	        [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
 	      (clear [id1;id2;aux]);
 	      (intros_using [id]);
@@ -1265,7 +1265,7 @@ let replay_history tactic_normalisation =
 	      (elim_id aux);
 	      (clear [aux]);
 	      (intros_using [vid; aux]);
-	      Proofview.V82.tactic (generalize_tac
+	      (generalize_tac
 		[mkApp (Lazy.force coq_OMEGA9,
 		  [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
 	      Proofview.V82.tactic (mk_then tac);
@@ -1304,7 +1304,7 @@ let replay_history tactic_normalisation =
               if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
             let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
             Tacticals.New.tclTHENLIST [
-	      Proofview.V82.tactic (generalize_tac
+	      (generalize_tac
                 [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
 	      Proofview.V82.tactic (mk_then tac);
 	      (intros_using [id]);
@@ -1320,7 +1320,7 @@ let replay_history tactic_normalisation =
 		 (cut (mk_gt kk2 izero))
 		 [Tacticals.New.tclTHENLIST [
 		   (intros_using [aux2;aux1]);
-		   Proofview.V82.tactic (generalize_tac
+		   (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA7, [|
 		       eq1;eq2;kk1;kk2;
 		       mkVar aux1;mkVar aux2;
@@ -1338,12 +1338,12 @@ let replay_history tactic_normalisation =
                 simpl_in_concl;
 		reflexivity ] ]
       | CONSTANT_NOT_NUL(e,k) :: l ->
-	  Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
+	  Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
       | CONSTANT_NUL(e) :: l ->
 	  Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity
       | CONSTANT_NEG(e,k) :: l ->
 	  Tacticals.New.tclTHENLIST [
-	    Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]);
+	    (generalize_tac [mkVar (hyp_of_tag e)]);
             unfold sp_Zle;
 	    simpl_in_concl;
 	    unfold sp_not;
@@ -1366,7 +1366,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
   let (tac,t') = normalize p_initial t in
   let shift_left =
     tclTHEN
-      (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
+      (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]))
       (tclTRY (Proofview.V82.of_tactic (clear [id])))
   in
   if not (List.is_empty tac) then
@@ -1546,7 +1546,7 @@ let nat_inject =
 	  begin try match destructurate_prop t with
               Kapp(Le,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1555,7 +1555,7 @@ let nat_inject =
                 ]
             | Kapp(Lt,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1564,7 +1564,7 @@ let nat_inject =
                 ]
             | Kapp(Ge,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1573,7 +1573,7 @@ let nat_inject =
                 ]
             | Kapp(Gt,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
                     [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1582,7 +1582,7 @@ let nat_inject =
                 ]
             | Kapp(Neq,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1592,7 +1592,7 @@ let nat_inject =
             | Kapp(Eq,[typ;t1;t2]) ->
 		if is_conv typ (Lazy.force coq_nat) then
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		      [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
 		    (explore [P_APP 2; P_TYPE] t1);
 		    (explore [P_APP 3; P_TYPE] t2);
@@ -1723,7 +1723,7 @@ let destructure_hyps =
               then
 		let d1 = decidability t1 in
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp,
+		  (generalize_tac [mkApp (Lazy.force coq_imp_simp,
                                                                [| t1; t2; d1; mkVar i|])]);
 		  (onClearedName i (fun i ->
 		    (loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit))))
@@ -1734,7 +1734,7 @@ let destructure_hyps =
               begin match destructurate_prop t with
 		Kapp(Or,[t1;t2]) ->
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
                                             [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
 		    (onClearedName i (fun i ->
                       (loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit))))
@@ -1742,7 +1742,7 @@ let destructure_hyps =
 	      | Kapp(And,[t1;t2]) ->
 		  let d1 = decidability t1 in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_and,
 				                    [| t1; t2; d1; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1752,7 +1752,7 @@ let destructure_hyps =
 		  let d1 = decidability t1 in
 		  let d2 = decidability t2 in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_iff,
 				                    [| t1; t2; d1; d2; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1764,7 +1764,7 @@ let destructure_hyps =
 		       For t1, being decidable implies being Prop. *)
 		  let d1 = decidability t1 in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_imp,
 				                    [| t1; t2; d1; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1773,7 +1773,7 @@ let destructure_hyps =
 	      | Kapp(Not,[t]) ->
 		  let d = decidability t in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 			                    [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
 		    (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit))))
                   ]
@@ -1781,7 +1781,7 @@ let destructure_hyps =
 		  (try
 		     let thm = not_binop op in
                      Tacticals.New.tclTHENLIST [
-		       Proofview.V82.tactic (generalize_tac
+		       (generalize_tac
 			                       [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
 		       (onClearedName i (fun _ -> loop lit))
                      ]
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 177c870b3..dca46cbcf 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1280,8 +1280,8 @@ let resolution env full_reified_goal systems_list =
     CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
   let decompose_tactic = decompose_tree env context solution_tree in
 
-  Tactics.generalize
-    (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
+  Proofview.V82.of_tactic (Tactics.generalize
+    (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >>
   Proofview.V82.of_tactic (Tactics.change_concl reified) >>
   Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
   show_goal >>
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 01ebaa7b7..b1d3290aa 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -64,7 +64,7 @@ let choose_noteq eqonleft =
 
 let mkBranches c1 c2 =
   tclTHENLIST
-    [Proofview.V82.tactic (generalize [c2]);
+    [generalize [c2];
      Simple.elim c1;
      intros;
      onLastHyp Simple.case;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c3d6a65eb..d4589154f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2766,14 +2766,15 @@ let generalize_dep ?(with_let=false) c gl =
     gl
 
 (**  *)
-let generalize_gen_let lconstr gl =
+let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let newcl, evd =
-    List.fold_right_i (generalize_goal gl) 0 lconstr
-      (Tacmach.pf_concl gl,Tacmach.project gl)
+    List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr
+      (Tacmach.New.pf_concl gl,Tacmach.New.project gl)
   in
-  Proofview.V82.of_tactic (Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd)
-    (apply_type newcl (List.map_filter (fun ((_,c,b),_) ->
-      if Option.is_empty b then Some c else None) lconstr))) gl
+  let map ((_, c, b),_) = if Option.is_empty b then Some c else None in
+  let tac = apply_type newcl (List.map_filter map lconstr) in
+  Sigma.Unsafe.of_pair (tac, evd)
+end }
 
 let new_generalize_gen_let lconstr =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -2809,11 +2810,8 @@ let generalize_gen lconstr =
 let new_generalize_gen lconstr =
   new_generalize_gen_let (List.map (fun ((occs,c),na) ->
     (occs,c,None),na) lconstr)
-    
-let generalize l =
-  generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l)
 
-let new_generalize l =
+let generalize l =
   new_generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l)
 
 (* Faudra-t-il une version avec plusieurs args de generalize_dep ?
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f730dd6c4..9d02d3f6d 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -383,10 +383,9 @@ val letin_pat_tac : (bool * intro_pattern_naming) option ->
 
 (** {6 Generalize tactics. } *)
 
-val generalize      : constr list -> tactic
-val generalize_gen  : (constr Locus.with_occurrences * Name.t) list -> tactic
+val generalize      : constr list -> unit Proofview.tactic
+val generalize_gen  : (constr Locus.with_occurrences * Name.t) list -> unit Proofview.tactic
 
-val new_generalize  : constr list -> unit Proofview.tactic
 val new_generalize_gen  : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic
 
 val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -> tactic