From c5156ef960467334fb5ae38dfd5a8740115ee09b Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Mar 2019 00:06:08 +0100
Subject: [doc] ssr: Fix the documentation of `by [tacs]`

Closes coq/coq#9669
---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 237b534d67..b81830f06b 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2094,9 +2094,9 @@ into a closing one (similar to :tacn:`now`). Its general syntax is:
    :name: by
    :undocumented:
 
-The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to
-:n:`[by @tactic | by @tactic | ...]` and this form should be preferred
-to the former.
+The Ltac expression :n:`by [@tactic | @tactic | …]` is equivalent to
+:n:`do [done | by @tactic | by @tactic | …]`, which corresponds to the
+standard Ltac expression :n:`first [done | @tactic; done | @tactic; done | …]`.
 
 In the script provided as example in section :ref:`indentation_ssr`, the
 paragraph corresponding to each sub-case ends with a tactic line prefixed
-- 
cgit v1.2.3