Zulip Chat Archive
Stream: general
Topic: missing doc
Patrick Massot (Feb 21 2020 at 23:13):
It seems https://github.com/leanprover-community/mathlib/pull/1953 was merged without updating tactics.md
Floris van Doorn (Feb 22 2020 at 07:07):
Good point, I will make a new PR for that at some point!
Last updated: May 02 2025 at 03:31 UTC