Merge PR #8372: Grammar rule in the documentation of ssreflect's anonymous arguments

1 files changed, 10 insertions, 5 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7c3ea1a28c..8656e5eb3e 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -444,11 +444,16 @@ not its name, one usually uses “arrow” abstractions for prenex
 arguments, or the ``(_ : term)`` syntax for inner arguments. In |SSR|,
 the latter can be replaced by the open syntax ``of term`` or
 (equivalently) ``& term``, which are both syntactically equivalent to a
-``(_ : term)`` expression.
+``(_ : term)`` expression. This feature almost behaves as the
+following extension of the binder syntax:
 
-For instance, the usual two-constructor polymorphic type list, i.e.
-the one of the standard List library, can be defined by the following
-declaration:
+.. prodn::
+   binder += & @term | of @term
+
+Caveat: ``& T`` and ``of T`` abbreviations have to appear at the end
+of a binder list. For instance, the usual two-constructor polymorphic
+type list, i.e. the one of the standard ``List`` library, can be
+defined by the following declaration:
 
 .. example::
 
@@ -5387,7 +5392,7 @@ Tacticals
 
 discharge :ref:`discharge_ssr`
 
-.. prodn:: tactic += @tacitc => {+ @i_item }
+.. prodn:: tactic += @tactic => {+ @i_item }
 
 introduction see :ref:`introduction_ssr`