mathlib3
chore(*): replace uses of `---` delimiter in tactic docs
#2372

Merged

chore(*): replace uses of `---` delimiter in tactic docs #2372

mergify merged 3 commits into master from tac-doc-comments

update abel doc string

a4063aa1

replace uses of --- in docs

4c988985

robertylewis added awaiting-review

bryangingechen approved these changes on 2020-04-09

bryangingechen removed awaiting-review

bryangingechen added ready-to-merge

Merge branch 'master' into tac-doc-comments

058f0f7c

mergify merged b15c213a into master 5 years ago

mergify deleted the tac-doc-comments branch 5 years ago

Reviewers

bryangingechen

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone