Closed MSoegtropIMC closed 4 months ago
Maybe of interest is #113.
For the record, I'm pretty sure nobody is working on #36 right now.
This isn't about retype, see https://github.com/coq-community/aac-tactics/pull/136/commits/36aef56d275a11fd673824925f1c69ab805d0cc9
@SkySkimmer : thanks for the fast fix!
AAC tactics apparently don't handle goal selectors properly.
This might be an effect of #36.
Here is an example: