Commit 2026-02-03 15:41 03ea12b8

fix(FieldSimp): declaration has free variables kernel errors (#32403) Fix a bug in field_simp that produces a (kernel) declaration has free variables error. The fix also makes field_simp dischargers more powerful by adding more hypotheses to their local context. The issue was that an internal simp call was misconfigured, so that simp assumed the discharger did not use any assumptions in the local context that were added by congruence lemmas. Because of this, simp was not clearing its cache often enough, and would use cached proofs that referenced non-existent hypotheses. The fix was to set the contextual flag to true.