-
Notifications
You must be signed in to change notification settings - Fork 259
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.
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
[Merged by Bors] - bump: update Aesop to 2022-02-24 #2484
Conversation
The errors go away after changing |
In the most basic way possible! inductive A : Prop where
| intro No wonder |
Good lord I'm an idiot. Thanks for debugging this. |
1224f31
to
0b0432b
Compare
Fixed now. |
bors d+ |
✌️ JLimperg can now approve this pull request. To approve and merge a pull request, simply reply with |
This version of Aesop supports local and scoped rules.
This one doesn't clobber the global namespace. :)
This reverts commit 1224f31.
aade8bb
to
d9a52cc
Compare
bors r+ |
This version of Aesop supports local and scoped rules.
Pull request successfully merged into master. Build succeeded:
|
This version of Aesop supports local and scoped rules.
I'm really confused about the changes in
Tactic.Positivity.Core
andTactic.Ring.Basic
. Without these changes, the files don't compile locally. But these files have nothing to do with Aesop and I didn't change anything else afaict. (Edit: theMfldSetTac
test also needs these weird changes.)