From a4996beb20f0d2102245c6bfa4cd1ae4c08f2478 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 4 May 2026 16:38:05 +0200 Subject: [PATCH 1/2] Remove non needed check_required_library in Generalize.abstract_args Dependent equality is not always used by this function so this restriction is too strong. Even if it was needed we should check the register not the library. --- tactics/generalize.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/tactics/generalize.ml b/tactics/generalize.ml index cf11b59e1875..f6d3207a98db 100644 --- a/tactics/generalize.ml +++ b/tactics/generalize.ml @@ -488,7 +488,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 From 5c1391640aec568062cc069c3cf2a12c7cee3b6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 4 May 2026 16:41:24 +0200 Subject: [PATCH 2/2] generalize_eqs_vars fix incorrect selection of variables to generalize Fix #22000 --- .../user-overlays/22001-SkySkimmer-gene-eqs-vars.sh | 4 ++++ .../04-tactics/22001-gene-eqs-vars-Changed.rst | 6 ++++++ tactics/generalize.ml | 7 ++++++- test-suite/bugs/bug_22000.v | 12 ++++++++++++ 4 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 dev/ci/user-overlays/22001-SkySkimmer-gene-eqs-vars.sh create mode 100644 doc/changelog/04-tactics/22001-gene-eqs-vars-Changed.rst create mode 100644 test-suite/bugs/bug_22000.v diff --git a/dev/ci/user-overlays/22001-SkySkimmer-gene-eqs-vars.sh b/dev/ci/user-overlays/22001-SkySkimmer-gene-eqs-vars.sh new file mode 100644 index 000000000000..9571c2f59f88 --- /dev/null +++ b/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 diff --git a/doc/changelog/04-tactics/22001-gene-eqs-vars-Changed.rst b/doc/changelog/04-tactics/22001-gene-eqs-vars-Changed.rst new file mode 100644 index 000000000000..a0ff941c6401 --- /dev/null +++ b/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 `_, + fixes `#22000 `_, + by Gaëtan Gilbert). diff --git a/tactics/generalize.ml b/tactics/generalize.ml index f6d3207a98db..e87a00534ac8 100644 --- a/tactics/generalize.ml +++ b/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,[]) diff --git a/test-suite/bugs/bug_22000.v b/test-suite/bugs/bug_22000.v new file mode 100644 index 000000000000..ba6c346b65a7 --- /dev/null +++ b/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.