mathlib3
chore(README,docs/*): replace tactic doc files with links to mathlib docs
#2225
Merged
Merged
chore(README,docs/*): replace tactic doc files with links to mathlib docs #2225
mergify
merged
4 commits into
master
from
tactic_doc_markdown_cleanup
chore(README,doc/*): replace tactic doc files with links to mathlib docs
f405f34e
bryangingechen
changed the title
reword contributor suggestion for tactic tests
8d04c1f3
reviewer comments
2306301b
robertylewis
approved these changes
on 2020-03-24
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into tactic_doc_markdown_cleanup
2e5713e7
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub