Induction issue?

Stream: lean4

[François G. Dorais]

This stopped working since the March 29 nightly, where the induction can't find the Decidable P instance anymore.

def casesTFOn {motive : Prop → Sort _} (P) [inst : Decidable P] : (T : motive True) → (F : motive False) → motive P :=
  λ ht hf => match inst with
  | isTrue H => eqTrue H ▸ ht
  | isFalse H => eqFalse H ▸ hf

example (P) [Decidable P] : ¬¬P → P := by
  induction P using casesTFOn
/-
error: unsolved goals
case inst
P : Prop
⊢ Decidable P
-/
  admit
  admit

Looking around, commit 41539a77 is a likely cause of this change in behavior. Is this an intensional change or a bug?

[Leonardo de Moura]

I will take a look, thanks for identifying the commit that introduced the problem.