PR #1229 doc(*): new documentation requirements

feat(docs/contribute/doc): template for documentation

robertylewis committed 7 years ago

doc(data/padics/padic_norm): new doc style

robertylewis committed 7 years ago

doc(docs/contribute/code-review): add link to doc requirements

robertylewis committed 7 years ago

doc(.github/PULL_REQUEST_TEMPLATE): add link to doc requirements

robertylewis committed 7 years ago

doc(topology/basic): adds new style documentation

PatrickMassot committed 7 years ago

feat(tactic/doc_blame): a user command #doc_blame

PatrickMassot committed 7 years ago

perf(tactic/doc_blame): filter declarations earlier

robertylewis committed 7 years ago

doc(contribute/doc): More doc style explanations

PatrickMassot committed 7 years ago

doc(data/padics/padic_norm): finish documenting

robertylewis committed 7 years ago

doc(docs/contribute/docs): more text about documentation requirements

robertylewis committed 7 years ago

feat(tactic/doc_blame): add option to blame theorems also

robertylewis committed 7 years ago

doc(cardinal/ordinal): add some documentation

fpvandoorn committed 7 years ago

fix(data/padics): remove leftover exit command

robertylewis committed 7 years ago

doc(*): update proposed doc style

robertylewis committed 7 years ago

doc(docs/contribute/doc.md): update doc style guide

robertylewis committed 7 years ago

feat(docs/references): add mathlib references bibtex

robertylewis committed 7 years ago

Merge branch 'master' into doc_style

robertylewis committed 7 years ago

update doc style in times_cont_diff and add to list of examples

robertylewis committed 7 years ago

fix(docs/contribute/doc): clarify implementation notes

robertylewis committed 7 years ago

doc(tactic/doc_blame): add header

robertylewis committed 7 years ago

Merge branch 'master' into doc_style

mergify[bot] committed 7 years ago

mathlib3 doc(*): new documentation requirements #1229 Merged