aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools')
-rw-r--r--doc/tools/coqrst/coqdomain.py4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 40554c3ca3..d81355e865 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -632,8 +632,8 @@ class InferenceDirective(Directive):
.. inference:: name
- newline-separated premisses
- ------------------------
+ newline-separated premises
+ --------------------------
conclusion
Example::