feat(docs/contribute/doc): template for documentation
c686578f
doc(data/padics/padic_norm): new doc style
ea874540
doc(docs/contribute/code-review): add link to doc requirements
c6561246
doc(.github/PULL_REQUEST_TEMPLATE): add link to doc requirements
d7a88a8e
doc(topology/basic): adds new style documentation
83e2c2ec
feat(tactic/doc_blame): a user command #doc_blame
7b0aceba
perf(tactic/doc_blame): filter declarations earlier
c168f977
doc(contribute/doc): More doc style explanations
cd52d354
doc(data/padics/padic_norm): finish documenting
fdc2fa7e
doc(docs/contribute/docs): more text about documentation requirements
5cb269df
feat(tactic/doc_blame): add option to blame theorems also
0f727be8
doc(cardinal/ordinal): add some documentation
3fa84685
fix(data/padics): remove leftover exit command
3160296c
bryangingechen
commented
on 2019-07-15
Vtec234
commented
on 2019-07-15
doc(*): update proposed doc style
370a5640
doc(docs/contribute/doc.md): update doc style guide
d8048584
feat(docs/references): add mathlib references bibtex
f0698981
Merge branch 'master' into doc_style
669a675d
update doc style in times_cont_diff and add to list of examples
699f1717
fix(docs/contribute/doc): clarify implementation notes
9d47e31e
doc(tactic/doc_blame): add header
b0ae35b0
jcommelin
approved these changes
on 2019-07-25
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into doc_style
3ab9e78a
Reviewers
Assignees
No one assigned
Labels
RFC
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub