Skip to content

chore: use new TangentSpace% elaborator#144

Merged
grunweg merged 1 commit into
masterfrom
more-elaborators
Jul 1, 2026
Merged

chore: use new TangentSpace% elaborator#144
grunweg merged 1 commit into
masterfrom
more-elaborators

Conversation

@grunweg

@grunweg grunweg commented Jun 17, 2026

Copy link
Copy Markdown
Collaborator

And a few more drive-by golfs. Mostly to show what's possible --- many changes I'm slightly positive about, but some are significant improvements. And if we want to eliminate superfluous models with corners, we want to make all these changes anyway.

@grunweg grunweg force-pushed the more-elaborators branch from 42689f8 to da4422a Compare June 17, 2026 20:57
@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 more-elaborators branch from da4422a to 1f8396d Compare July 1, 2026 12:15
@grunweg

grunweg commented Jul 1, 2026

Copy link
Copy Markdown
Collaborator Author

Same CI error as before: let me merge this also.

@grunweg grunweg merged commit d6bf67a into master Jul 1, 2026
1 check failed
@grunweg grunweg deleted the more-elaborators branch July 1, 2026 12:32
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