aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
authorClément Pit-Claudel2018-05-16 20:07:30 -0400
committerThéo Zimmermann2018-09-20 10:12:55 +0200
commitddc4391be1214ea4d929ba0a8737be4eda6b87ad (patch)
tree2d2b523153c858ccdbe09f615f5f914422049b8b /doc/sphinx
parentdf1f5bcd406a87c77601942f21d16555a8f6086e (diff)
[doc] Fix a typo in coqdomain.py
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/README.rst4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 4673107e3d..983f4e665f 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -260,8 +260,8 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
.. inference:: name
- newline-separated premisses
- ------------------------
+ newline-separated premises
+ --------------------------
conclusion
Example::