Zulip Chat Archive

Stream: general

Topic: two minor tactic bugs

Floris van Doorn (Jun 27 2022 at 09:56):

I opened two minor tactic bug reports for apply' (#14993) and nth_rewrite (#14994).
I don't particularly care if they get fixed, but I wanted to at least document the failure.

Last updated: May 02 2025 at 03:31 UTC