generalize_eqs_vars fix incorrect selection of variables to generalize

dev/ci/user-overlays/22001-SkySkimmer-gene-eqs-vars.sh

@@ -0,0 +1,4 @@
+overlay kami https://github.com/SkySkimmer/kami gene-eqs-vars 22001
+# Make PRs against https://github.com/mit-plv/kami base branch rv32i
+
+overlay itree https://github.com/SkySkimmer/InteractionTrees gene-eqs-vars 22001

doc/changelog/04-tactics/22001-gene-eqs-vars-Changed.rst

@@ -0,0 +1,6 @@
+- **Changed:**
+  :tacn:`generalize_eqs_vars` (used in :tacn:`dependent induction`)
+  does less useless generalizations
+  (`#22001 <https://github.com/rocq-prover/rocq/pull/22001>`_,
+  fixes `#22000 <https://github.com/rocq-prover/rocq/issues/22000>`_,
+  by Gaëtan Gilbert).

tactics/generalize.ml

@@ -364,12 +364,17 @@ let hyps_of_vars env sigma sign nogen hyps =
     let (_,lh) =
       Context.Named.fold_inside
         (fun (hs,hl) d ->
+           (* hs: vars to generalize (set)
+              hl: vars to generalize that we have seen (list)
+
+              we should generalize d if it is not nogen and
+              either is in hs, or depends on some var in hs *)
           let x = NamedDecl.get_id d in
           if Id.Set.mem x nogen then (hs,hl)
           else if Id.Set.mem x hs then (hs,x::hl)
           else
             let xvars = global_vars_set_of_decl env sigma d in
-              if not (Id.Set.is_empty (Id.Set.diff xvars hs)) then
+              if not (Id.Set.is_empty (Id.Set.inter xvars hs)) then
                 (Id.Set.add x hs, x :: hl)
               else (hs, hl))
         ~init:(hyps,[])
@@ -488,7 +493,6 @@ let abstract_args gl generalize_vars dep id defined f args =
 let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
   let open Context.Named.Declaration in
   Proofview.Goal.enter begin fun gl ->
-  Rocqlib.(check_required_library jmeq_module_name);
   let sigma = Proofview.Goal.sigma gl in
   let (f, args, def, id, oldid) =
     let oldid = Tacmach.pf_get_new_id id gl in

test-suite/bugs/bug_22000.v

@@ -0,0 +1,12 @@
+Section S.
+  Variable rename : nat -> nat.
+  Variable rename_inj : rename 0 = 0.
+
+  Goal forall x y, x = S y -> False.
+  Proof.
+    intros x y H.
+    generalize_eqs_vars H.
+    Check rename_inj.
+    Fail Check y.
+  Abort.
+End S.