`induction` ignores registered induction schemes

[JasonGross]

Description of the problem

How can I get induction to use the dependent induction scheme rather than the minimality scheme registered in corelib?

Small Rocq / Coq file to reproduce the bug

Scheme eq_ind := Induction for Corelib.Init.Logic.eq Sort Prop.
Scheme eq_rect := Induction for Corelib.Init.Logic.eq Sort Type.
Goal forall x1 x3 x9 x5 (x : @Corelib.Init.Logic.eq x1 x3 x9)
(_ : (fun (a : x1) (_ : @Corelib.Init.Logic.eq x1 x3 a) => x5 a)
       x9 x),
(fun (a : x1) (_ : @Corelib.Init.Logic.eq x1 x3 a) => x5 a) x9 x.
Proof.
    intros x1 x3 x9 x5 x.
    Fail induction x. (* Error: Abstracting over the term "x9" leads to a term
    fun x0 : x1 =>
    (fun (a : x1) (_ : x3 = a) => x5 a) x0 x ->
    (fun (a : x1) (_ : x3 = a) => x5 a) x0 x
    which is ill-typed.
    Reason is: Illegal application:
    The term "fun (a : x1) (_ : x3 = a) => x5 a" of type
     "forall a : x1, x3 = a -> Type"
    cannot be applied to the terms
     "x0" : "x1"
     "x" : "x3 = x9"
    The 2nd term has type "x3 = x9" which should be a subtype of
    "x3 = x0". *)
    induction x using eq_rect.

Version of Rocq / Coq where this bug occurs

9.1.0

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

[SkySkimmer]

For backwards compatibility induction tries the non dependent scheme first for inductives in Prop.
IDK how to solve this without breaking random developments.

[ppedrot]

One more table that tracks when we opt out of this behaviour?

[SkySkimmer]

Maybe induction could tell that it needs a dependent scheme and not even try to look for a nondependent scheme here?