Fix de Bruijn index bug in inductive_of_mutfix.find_ind

[JasonGross]

Summary

• Fix a de Bruijn index off-by-one in inductive_of_mutfix.find_ind that caused rocq check (and the kernel guard checker) to fail on fixpoints whose structural argument type contains a de Bruijn reference (e.g., a section Let-bound type alias).
• The bug was introduced by a46bbfb (9.3) ("Reorder and cleanup in inductive_of_mutfix.find_ind"), which moved push_rel before the find_inductive call. Since ty is valid in the pre-push context, de Bruijn indices in ty were resolved to wrong bindings in the post-push environment.
• Added a regression test (test-suite/coqchk/bug_22125.v).

Fixes #22125.

Test plan

• Minimal reproduction: Section S. Let T := list nat. Fixpoint my_length (l : T) ... End S. now passes rocqchk
• All existing coqchk tests pass
• Guard checker success/failure tests pass

🤖 Generated with Claude Code

[SkySkimmer]

maybe also add a coqc test with

Definition my_length (T:=list nat) := fix my_length (l : T) : nat :=
  match l with
  | nil => O
  | cons _ l' => S (my_length l')
  end.

?

[ppedrot]

Indeed.

[ppedrot]

@coqbot run full ci

[yannl35133]

Why are the tests in two different files, in success? A single file in bugs should be checked by rocq check.

[JasonGross]

Why are the tests in two different files, in success? A single file in bugs should be checked by rocq check.

I added it in response to @SkySkimmer 's comment, but indeed I don't understand what the second file adds over the existing one (neither in content nor in mechanism of being tested). What is the thing that you believe is missing from the coqchk test @SkySkimmer ?

[JasonGross]

Files merged. Note that full ci passed before I rebased, but I guess we might as well @coqbot run full ci

[yannl35133]

The second test could fail in rocq c directly, instead of requiring rocq check to appear; it's going to be easier to debug if it gets broken again. I imagine there's nothing deeper.