Skip to content

chore: use new elaborators more#142

Merged
grunweg merged 3 commits into
masterfrom
bump-betterelabs
Jul 1, 2026
Merged

chore: use new elaborators more#142
grunweg merged 3 commits into
masterfrom
bump-betterelabs

Conversation

@grunweg

@grunweg grunweg commented Jun 1, 2026

Copy link
Copy Markdown
Collaborator

Incorporates #124, and goes a bit further.

Main finding: we want to add support for OneJetBundle to findModel. Making this extensible would be really nice!

@grunweg grunweg mentioned this pull request Jun 29, 2026
grunweg added a commit that referenced this pull request Jul 1, 2026
Bump to current mathlib: uneventful.
This will allow using the improved custom elaborators in #142 and #144.
@grunweg grunweg force-pushed the bump-betterelabs branch from 587b82d to 07940fe Compare July 1, 2026 12:35
@grunweg

grunweg commented Jul 1, 2026

Copy link
Copy Markdown
Collaborator Author

Same procedure as last PR.

@grunweg grunweg merged commit ded8fda into master Jul 1, 2026
1 check failed
@grunweg grunweg deleted the bump-betterelabs branch July 1, 2026 13:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant