From 9e1a30ce69b3ebdd8f1617d7c3a0b92641c771fd Mon Sep 17 00:00:00 2001
From: Paolo G. Giarrusso
Date: Mon, 27 Jan 2020 21:38:26 +0100
Subject: Fix off-by-one in docs of `first num last` (fix #11463)

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 853ddfd6dc..6d3259bb4d 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2229,7 +2229,7 @@ tactics to *permute* the subgoals generated by a tactic.
 
       If :token:`num`\'s value is :math:`k`,
       this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n`
-      in focus. The first subgoal becomes :math:`G_k` and the circular order
+      in focus. The first subgoal becomes :math:`G_{k + 1 \bmod n}` and the circular order
       of subgoals remains unchanged.
 
 Finally, the tactics ``last`` and ``first`` combine with the branching syntax
-- 
cgit v1.2.3