Skip to content

nightly-2025-01-01

Pre-release
Pre-release
Compare
Choose a tag to compare
@leodemoura leodemoura released this 01 Jan 08:36
· 1 commit to main since this release
6d44715

Changes since nightly-2024-12-31:

Full commit log

  • 6d44715 fix: make sure parent structure projections have 'go to definition' information (#6487)
  • 3427630 feat: configuration options for the grind tactic (#6490)
  • 5ba4761 fix: E-matching module for grind (#6488)
  • 8899c7e feat: instantiate ematch theorems in grind (#6485)
  • 640b356 chore: add missing diff-exposing in type/value mismatch errors (#6484)
  • 8f5ce3a feat: upstream ToExpr deriving handler from Mathlib (#6473)