New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Elab strategy removal alt #18050

Closed

PatrickMassot wants to merge 2 commits into master from elab_strategy_removal_alt

Member

PatrickMassot commented Jan 3, 2023

Alternative to #18049

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/elab_strategy


          chore(data/fin/basic): Remove elab_strategy

a164fa9

PatrickMassot added the awaiting-CI label


          chore(data/fin/basic): remove elab_strategy

e93ab41

github-actions bot removed the awaiting-CI label

Member Author

PatrickMassot commented Jan 3, 2023

Closed in favor of #18049.

PatrickMassot closed this

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment