Commit 2026-03-26 01:07 425c4949

fix(Tactic/Recall): allow different universe variable names (#37145) Fixes https://github.com/leanprover-community/mathlib4/issues/37144 This PR fixes recall failing when the recalled declaration uses a different universe variable name (or Type*) compared to the original declaration. The type-only branch of recall compared info.type directly against the elaborated type without first instantiating the original declaration's level parameters with fresh level metavariables. The value branch already did this correctly. 🤖 Prepared with Claude Code