Put the "generalize" tactic in the monad.

3 files changed, 13 insertions, 13 deletions

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