diff options
author | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-13 12:18:17 -0400 |
---|---|---|
committer | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-22 11:40:13 -0400 |
commit | 55c35435dc383a3f488a706605ba57607fd88681 (patch) | |
tree | a81f6e34b9946962f5f1a6f79bc6cb62d63e4681 /doc/sphinx/README.rst | |
parent | 3ae50f0ba006e77e27fbe81b192234de1ee617c5 (diff) |
[doc] Add a list of common mistakes
Diffstat (limited to 'doc/sphinx/README.rst')
-rw-r--r-- | doc/sphinx/README.rst | 56 |
1 files changed, 56 insertions, 0 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 5f2f21f2b..eae5c71f9 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -291,6 +291,62 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_ and reference its tokens using ``:token:`…```. +Common mistakes +=============== + +Improper nesting +---------------- + +DO + .. code:: + + .. cmd:: Foo @bar + + Foo the first instance of :token:`bar`\ s. + + .. cmdv:: Foo All + + Foo all the :token:`bar`\ s in + the current context + +DON'T + .. code:: + + .. cmd:: Foo @bar + + Foo the first instance of :token:`bar`\ s. + + .. cmdv:: Foo All + + Foo all the :token:`bar`\ s in + the current context + +Overusing ``:token:`` +--------------------- + +DO + .. code:: + + This is equivalent to :n:`Axiom @ident : @term`. + +DON'T + .. code:: + + This is equivalent to ``Axiom`` :token`ident` : :token:`term`. + +Omitting annotations +-------------------- + +DO + .. code:: + + .. tacv:: assert @form as @intro_pattern + +DON'T + .. code:: + + .. tacv:: assert form as intro_pattern + Tips and tricks =============== |