diff options
| author | Clément Pit-Claudel | 2018-05-18 00:07:36 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | e45bada261c42152e0b835cae7e989a7fccc0fb7 (patch) | |
| tree | e266ff1997f354f8727ea0dd9fe0f76d1c49e268 | |
| parent | 196f36e1db08c80c0e2d1de538a4c0fe6bae062b (diff) | |
[doc] Add more common mistakes to the documentation-writing guide
| -rw-r--r-- | doc/sphinx/README.rst | 43 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 43 |
2 files changed, 86 insertions, 0 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 2884f70477..6d5545ec3c 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -362,6 +362,32 @@ DON'T This is equivalent to ``Axiom`` :token`ident` : :token:`term`. +.. + +DO + .. code:: + + :n:`power_tac @term [@ltac]` + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +DON'T + .. code:: + + power_tac :n:`@term` [:n:`@ltac`] + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +.. + +DO + .. code:: + + :n:`name={*; attr}` + +DON'T + .. code:: + + ``name=``:n:`{*; attr}` + Omitting annotations -------------------- @@ -408,6 +434,23 @@ DONT first [ t1 | … | tn ]. +Overusing plain quotes +---------------------- + +DO + .. code:: + + The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception. + The term :g:`let a = 1 in a a` is ill-typed. + +DON'T + .. code:: + + The ``refine`` tactic can raise the ``Invalid argument`` exception. + The term ``let a = 1 in a a`` is ill-typed. + +Plain quotes produce plain text, without highlighting or cross-references. + Tips and tricks =============== diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index d1052d48b2..73b2e96dcb 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -140,6 +140,32 @@ DON'T This is equivalent to ``Axiom`` :token`ident` : :token:`term`. +.. + +DO + .. code:: + + :n:`power_tac @term [@ltac]` + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +DON'T + .. code:: + + power_tac :n:`@term` [:n:`@ltac`] + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +.. + +DO + .. code:: + + :n:`name={*; attr}` + +DON'T + .. code:: + + ``name=``:n:`{*; attr}` + Omitting annotations -------------------- @@ -186,6 +212,23 @@ DONT first [ t1 | … | tn ]. +Overusing plain quotes +---------------------- + +DO + .. code:: + + The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception. + The term :g:`let a = 1 in a a` is ill-typed. + +DON'T + .. code:: + + The ``refine`` tactic can raise the ``Invalid argument`` exception. + The term ``let a = 1 in a a`` is ill-typed. + +Plain quotes produce plain text, without highlighting or cross-references. + Tips and tricks =============== |