From acfea8d9515504d4842ae5d24fc39186303d1cde Mon Sep 17 00:00:00 2001
From: Paolo G. Giarrusso
Date: Mon, 27 Jan 2020 21:39:59 +0100
Subject: Rephrase to reduce ambiguity

This is the smallest possible change to clarify the text without making it
even more formal.
---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 6d3259bb4d..46215f16a6 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2222,14 +2222,14 @@ 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_{n + 1 − k}` and the
+      in focus. Subgoal :math:`G_{n + 1 − k}` becomes the first, and the
       circular order of subgoals remains unchanged.
 
    .. tacn:: first @num last
 
       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 + 1 \bmod n}` and the circular order
+      in focus. Subgoal :math:`G_{k + 1 \bmod n}` becomes the first, and the circular order
       of subgoals remains unchanged.
 
 Finally, the tactics ``last`` and ``first`` combine with the branching syntax
-- 
cgit v1.2.3