Merge PR #17768: Move generalize-like tactics to their own module.

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

dev/ci/user-overlays/17768-ppedrot-split-generalize-tactics.sh

@@ -0,0 +1,7 @@
+overlay coqhammer https://github.com/ppedrot/coqhammer split-generalize-tactics 17768
+
+overlay equations https://github.com/ppedrot/Coq-Equations split-generalize-tactics 17768
+
+overlay itauto https://gitlab.inria.fr/pedrot/itauto split-generalize-tactics 17768
+
+overlay stalmarck https://github.com/ppedrot/stalmarck split-generalize-tactics 17768

plugins/firstorder/instances.ml

@@ -138,7 +138,7 @@ let left_instance_tac ~flags (inst,id) continue seq=
                 (pf_constr_of_global id >>= fun idc ->
                 Proofview.Goal.enter begin fun gl ->
                   let id0 = List.nth (pf_ids_of_hyps gl) 0 in
-                  generalize [mkApp(idc, [|mkVar id0|])]
+                  Generalize.generalize [mkApp(idc, [|mkVar id0|])]
                 end);
                 introf;
                 tclSOLVE [wrap ~flags 1 false continue
@@ -161,10 +161,10 @@ let left_instance_tac ~flags (inst,id) continue seq=
                     with e when CErrors.noncritical e ->
                       user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in
                   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evmap)
-                    (generalize [gt])
+                    (Generalize.generalize [gt])
                 end)
             else
-              pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|snd @@ Item.repr c|])]
+              pf_constr_of_global id >>= fun idc -> Generalize.generalize [mkApp(idc,[|snd @@ Item.repr c|])]
           in
             tclTHENLIST
               [special_generalize;

plugins/firstorder/rules.ml

@@ -80,7 +80,7 @@ let ll_atom_tac ~flags a backtrack id continue seq =
           gr >>= fun gr ->
           pf_constr_of_global gr >>= fun left ->
           pf_constr_of_global id >>= fun id ->
-            generalize [(mkApp(id, [|left|]))]);
+            Generalize.generalize [(mkApp(id, [|left|]))]);
          clear_global id;
          intro])
     (wrap ~flags 1 false continue seq) backtrack
@@ -153,7 +153,7 @@ let ll_ind_tac ~flags (ind,u as indu) largs backtrack id continue seq =
        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 -> Generalize.generalize (newhyps idc));
                clear_global id;
                tclDO lp intro])
            (wrap ~flags lp false continue seq) backtrack
@@ -174,7 +174,7 @@ let ll_arrow_tac ~flags a b c backtrack id continue seq=
           tclTHENS (cut cc)
             [(pf_constr_of_global id >>= fun c -> exact_no_check c);
              tclTHENLIST
-               [(pf_constr_of_global id >>= fun idc -> generalize [d idc]);
+               [(pf_constr_of_global id >>= fun idc -> Generalize.generalize [d idc]);
                 clear_global id;
                 introf;
                 introf;
@@ -215,7 +215,7 @@ let ll_forall_tac ~flags prod backtrack id continue seq=
               let open EConstr in
               let id0 = List.nth (pf_ids_of_hyps gls) 0 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
-              tclTHEN (generalize [term]) (clear [id0])
+              tclTHEN (Generalize.generalize [term]) (clear [id0])
            end);
            clear_global id;
            intro;

plugins/funind/functional_principles_proofs.ml

@@ -616,7 +616,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
                       make_refl_eq (Lazy.force refl_equal) type_of_term t
                     in
                     tclTHENLIST
-                      [ generalize (term_eq :: List.map mkVar dyn_infos.rec_hyps)
+                      [ Generalize.generalize (term_eq :: List.map mkVar dyn_infos.rec_hyps)
                       ; thin dyn_infos.rec_hyps
                       ; pattern_option [(Locus.AllOccurrencesBut [1], t)] None
                       ; observe_tac "toto"
@@ -807,14 +807,14 @@ let generalize_non_dep hyp =
       (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
       Tacticals.tclTHEN
         ((* observe_tac "h_generalize" *)
-         generalize (List.map mkVar to_revert))
+         Generalize.generalize (List.map mkVar to_revert))
         ((* observe_tac "thin" *) clear to_revert))
 
 let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id
 let var_of_decl = id_of_decl %> mkVar
 
 let revert idl =
-  Tacticals.tclTHEN (generalize (List.map mkVar idl)) (clear idl)
+  Tacticals.tclTHEN (Generalize.generalize (List.map mkVar idl)) (clear idl)
 
 let generate_equation_lemma env evd fnames f fun_num nb_params nb_args rec_args_num
     =
@@ -1473,7 +1473,7 @@ let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes
       in
       let open Tacticals in
       let revert l =
-        tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l)
+        tclTHEN (Generalize.generalize (List.map mkVar l)) (clear l)
       in
       let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in
       let prove_rec_arg_acc =
@@ -1520,7 +1520,7 @@ let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes
                 (Id.Set.of_list hyps)
             in
             tclTHENLIST
-              [ generalize [lemma]
+              [ Generalize.generalize [lemma]
               ; Simple.intro hid
               ; Elim.h_decompose_and (mkVar hid)
               ; Proofview.Goal.enter (fun g ->

plugins/funind/gen_principle.ml

@@ -877,7 +877,7 @@ let generalize_dependent_of x hyp =
             when (not (Id.equal id hyp))
                  && Termops.occur_var (Proofview.Goal.env g)
                       (Proofview.Goal.sigma g) x t ->
-            tclTHEN (Tactics.generalize [EConstr.mkVar id]) (thin [id])
+            tclTHEN (Generalize.generalize [EConstr.mkVar id]) (thin [id])
           | _ -> Proofview.tclUNIT ())
         (Proofview.Goal.hyps g))
 
@@ -1140,7 +1140,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i :
                     (Genredexpr.Cbv
                        {Redops.all_flags with Genredexpr.rDelta = false})
                     Locusops.onConcl
-                ; generalize (List.map mkVar ids)
+                ; Generalize.generalize (List.map mkVar ids)
                 ; thin ids ]
             else
               unfold_in_concl
@@ -1181,7 +1181,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i :
           tclTHENLIST
             [ tclMAP Simple.intro (args_names @ [res; hres])
             ; observe_tac "h_generalize"
-                (generalize
+                (Generalize.generalize
                    [ mkApp
                        ( applist (graph_principle, params)
                        , Array.map (fun c -> applist (c, params)) lemmas ) ])

plugins/funind/invfun.ml

@@ -54,7 +54,7 @@ let revert_graph kn post_tac hid =
           | Some f_complete ->
             let f_args, res = Array.chop (Array.length args - 1) args in
             tclTHENLIST
-              [ generalize
+              [ Generalize.generalize
                   [ applist
                       ( mkConst f_complete
                       , Array.to_list f_args @ [res.(0); mkVar hid] ) ]
@@ -100,7 +100,7 @@ let functional_inversion kn hid fconst f_correct =
         in
         tclTHENLIST
           [ pre_tac hid
-          ; generalize
+          ; Generalize.generalize
               [applist (f_correct, Array.to_list f_args @ [res; mkVar hid])]
           ; clear [hid]
           ; Simple.intro hid

plugins/funind/recdef.ml

@@ -743,7 +743,7 @@ let mkDestructEq not_on_hyp env sigma expr =
     pf_typel new_hyps (fun _ ->
         observe_tclTHENLIST
           (fun _ _ -> str "mkDestructEq")
-          [ generalize new_hyps
+          [ Generalize.generalize new_hyps
           ; Proofview.Goal.enter (fun g2 ->
                 let changefun patvars env sigma =
                   pattern_occs
@@ -1249,7 +1249,7 @@ let termination_proof_header is_mes input_type ids args_id relation rec_arg_num
                    (fun _ _ -> str "generalize")
                    (onNLastHypsId (nargs + 1)
                       (tclMAP (fun id ->
-                           tclTHEN (Tactics.generalize [mkVar id]) (clear [id]))))
+                           tclTHEN (Generalize.generalize [mkVar id]) (clear [id]))))
                ; observe_tac (fun _ _ -> str "fix") (fix hrec (nargs + 1))
                ; h_intros args_id
                ; Simple.intro wf_rec_arg
@@ -1451,7 +1451,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
           let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gl) in
           observe_tclTHENLIST
             (fun _ _ -> mt ())
-            [ generalize [lemma]
+            [ Generalize.generalize [lemma]
             ; Simple.intro hid
             ; Proofview.Goal.enter (fun gl ->
                   let ids = pf_ids_of_hyps gl in

plugins/ltac/coretactics.mlg

@@ -234,7 +234,7 @@ END
 (** Revert *)
 
 TACTIC EXTEND revert
-| [ "revert" ne_hyp_list(hl) ] -> { Tactics.revert hl }
+| [ "revert" ne_hyp_list(hl) ] -> { Generalize.revert hl }
 END
 
 (** Simple induction / destruct *)
@@ -300,7 +300,7 @@ END
 (* Generalize dependent *)
 
 TACTIC EXTEND generalize_dependent
-| [ "generalize" "dependent" constr(c) ] -> { Tactics.generalize_dep c }
+| [ "generalize" "dependent" constr(c) ] -> { Generalize.generalize_dep c }
 END
 
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)

plugins/ltac/extratactics.mlg

@@ -460,16 +460,16 @@ END
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
   defined by Conor McBride *)
 TACTIC EXTEND generalize_eqs
-| ["generalize_eqs" hyp(id) ] -> { abstract_generalize ~generalize_vars:false id }
+| ["generalize_eqs" hyp(id) ] -> { Generalize.abstract_generalize ~generalize_vars:false id }
 END
 TACTIC EXTEND dep_generalize_eqs
-| ["dependent" "generalize_eqs" hyp(id) ] -> { abstract_generalize ~generalize_vars:false ~force_dep:true id }
+| ["dependent" "generalize_eqs" hyp(id) ] -> { Generalize.abstract_generalize ~generalize_vars:false ~force_dep:true id }
 END
 TACTIC EXTEND generalize_eqs_vars
-| ["generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~generalize_vars:true id }
+| ["generalize_eqs_vars" hyp(id) ] -> { Generalize.abstract_generalize ~generalize_vars:true id }
 END
 TACTIC EXTEND dep_generalize_eqs_vars
-| ["dependent" "generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~force_dep:true ~generalize_vars:true id }
+| ["dependent" "generalize_eqs_vars" hyp(id) ] -> { Generalize.abstract_generalize ~force_dep:true ~generalize_vars:true id }
 END
 
 (** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T]

plugins/ltac/internals.ml

@@ -140,7 +140,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
     let type_of_a = Tacmach.pf_get_type_of gl a in
     Tacticals.pf_constr_of_global (delayed_force refl_equal) >>= fun req ->
     Tacticals.tclTHENLIST
-         [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))];
+         [Generalize.generalize [(mkApp(req, [| type_of_a; a|]))];
           Proofview.Goal.enter begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in

plugins/ltac/leminv.ml

@@ -288,7 +288,7 @@ let lemInvIn id c ids =
       else
         (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
     in
-    ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
+    ((tclTHEN (tclTHEN (Generalize.bring_hyps hyps) (lemInv id c))
         (intros_replace_ids)))
   end
 

plugins/ltac/tacinterp.ml

@@ -1777,7 +1777,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Tacticals.tclWITHHOLES false
         (name_atomic ~env
           (TacGeneralize cl)
-          (Tactics.generalize_gen cl)) sigma
+          (Generalize.generalize_gen cl)) sigma
       end
   | TacLetTac (ev,na,c,clp,b,eqpat) ->
       Proofview.Goal.enter begin fun gl ->

plugins/ltac2/tac2stdlib.ml

@@ -498,7 +498,7 @@ let () = define_prim1 "tac_rename" (list (pair ident ident)) begin fun ids ->
 end
 
 let () = define_prim1 "tac_revert" (list ident) begin fun ids ->
-  Tactics.revert ids
+  Generalize.revert ids
 end
 
 let () = define_prim0 "tac_admit" Proofview.give_up

plugins/ltac2/tac2tactics.ml

@@ -135,7 +135,7 @@ let elim ev c copt =
 let generalize pl =
   let mk_occ occs = mk_occurrences (fun i -> i) occs in
   let pl = List.map (fun (c, occs, na) -> (mk_occ occs, c), na) pl in
-  Tactics.new_generalize_gen pl
+  Generalize.new_generalize_gen pl
 
 let general_case_analysis ev c =
   let c = mk_with_bindings c in

plugins/micromega/coq_micromega.ml

@@ -2127,7 +2127,7 @@ let micromega_genr prover tac =
                arith_goal)
             [ kill_arith
             ; Tacticals.tclTHENLIST
-                [ Tactics.generalize (List.map EConstr.mkVar ids)
+                [ Generalize.generalize (List.map EConstr.mkVar ids)
                 ; Tactics.exact_check
                     (EConstr.applist (EConstr.mkVar goal_name, arith_args)) ] ]
       with

plugins/nsatz/nsatz.ml

@@ -11,7 +11,6 @@
 open CErrors
 open Util
 open Constr
-open Tactics
 
 open Utile
 
@@ -535,7 +534,7 @@ let return_term t =
   let a =
     mkApp (UnivGen.constr_of_monomorphic_global (Global.env ()) @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in
   let a = EConstr.of_constr a in
-  generalize [a]
+  Generalize.generalize [a]
 
 let nsatz_compute t =
   let lpol =

plugins/ssr/ssrview.ml

@@ -336,7 +336,7 @@ Goal.enter_one ~__LOC__ begin fun g ->
 end
 
 let pose_proof subject_name p =
-  Tactics.generalize [p] <*>
+  Generalize.generalize [p] <*>
   begin match subject_name with
   | id :: _ -> Ssrcommon.tclRENAME_HD_PROD (Name.Name id)
   | _ -> tclUNIT() end

tactics/equality.ml

@@ -1825,7 +1825,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
-      [revert (List.map snd dephyps);
+      [Generalize.revert (List.map snd dephyps);
        general_rewrite ~where:None ~l2r:dir AtLeastOneOccurrence ~freeze:true ~dep:dep_proof_ok ~with_evars:false (mkVar hyp, NoBindings);
        (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)]
       else