aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tools/coqrst
diff options
context:
space:
mode:
authorGravatar Clément Pit-Claudel <clement.pitclaudel@live.com>2018-05-04 19:02:11 -0400
committerGravatar Clément Pit-Claudel <clement.pitclaudel@live.com>2018-05-15 12:05:44 -0400
commitd5bb8a4ae2f509532ecfb4a53bb91c64d992c2e6 (patch)
tree6cf4a3d6bcb485265340dad79dc6f4698342f1ca /doc/tools/coqrst
parenta6545a120c6587af38883597d20ac28131b813a9 (diff)
[doc] Address feedback on doc writer guide
Co-Authored-By: @Zimmi48
Diffstat (limited to 'doc/tools/coqrst')
-rw-r--r--doc/tools/coqrst/coqdomain.py17
-rwxr-xr-xdoc/tools/coqrst/regen_readme.py2
2 files changed, 12 insertions, 7 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 3cad394e6..f8bb113a7 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -215,8 +215,8 @@ class VernacVariantObject(VernacObject):
.. cmd:: Axiom @ident : @term.
- This command links *term* to the name *ident* as its specification in
- the global context. The fact asserted by *term* is thus assumed as a
+ This command links :token:`term` to the name :token:`term` as its specification in
+ the global context. The fact asserted by :token:`term` is thus assumed as a
postulate.
.. cmdv:: Parameter @ident : @term.
@@ -340,7 +340,7 @@ class ExceptionObject(NotationObject):
.. exn:: Proof is not complete
- Raised is :n:`@tactic` does not fully solve the goal.
+ Raised if :n:`@tactic` does not fully solve the goal.
"""
subdomain = "exn"
index_suffix = "(err)"
@@ -362,8 +362,8 @@ class WarningObject(NotationObject):
.. warn:: Ambiguous path
- When the coercion `qualid` is added to the inheritance graph, non
- valid coercion paths are ignored.
+ When the coercion :token:`qualid` is added to the inheritance graph, non
+ valid coercion paths are ignored.
"""
subdomain = "warn"
index_suffix = "(warn)"
@@ -377,7 +377,8 @@ def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
#pylint: disable=unused-argument, dangerous-default-value
"""Any text using the notation syntax (``@id``, ``{+, …}``, etc.).
- Use this to explain tactic equivalences (for example, you might write this::
+ Use this to explain tactic equivalences. For example, you might write
+ this::
:n:`generalize @term as @ident` is just like :n:`generalize @term`, but
it names the introduced hypothesis :token:`ident`.
@@ -445,6 +446,10 @@ class CoqtopDirective(Directive):
- ``reset``: Send a ``Reset Initial`` command before running this block
- ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after
running all the commands in this block
+
+ ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
+ of the same document (``coqrst`` creates a single ``coqtop`` process per
+ reST source file). Use the ``reset`` option to reset Coq's state.
"""
has_content = True
required_arguments = 0
diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py
index 050ca4956..e56882a52 100755
--- a/doc/tools/coqrst/regen_readme.py
+++ b/doc/tools/coqrst/regen_readme.py
@@ -1,7 +1,7 @@
#!/usr/bin/env python3
# -*- coding: utf-8 -*-
-"""Rebuild README.rst from README.template.rst."""
+"""Rebuild sphinx/README.rst from sphinx/README.template.rst."""
import re
from os import sys, path