mathlib
c8946c9d - chore(tactic/*): remove some unused args in commands (#2498)

Commit

5 years ago

chore(tactic/*): remove some unused args in commands (#2498) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

References

Author

khoek

Parents