Update documentation of Arguments after recent changes.

2 files changed, 13 insertions, 13 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 51e881bff4..b475a5233c 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1315,10 +1315,10 @@ command:
 \begin{quote}
 \tt Arguments {\qualid} \nelist{\possiblybracketedident}{}
 \end{quote}
-where the list of {\possiblybracketedident} is the list of all arguments of
-{\qualid} where the ones to be declared implicit are surrounded by
-square brackets and the ones to be declared as maximally inserted implicits
-are surrounded by curly braces.
+where the list of {\possiblybracketedident} is a prefix of the list of arguments
+of {\qualid} where the ones to be declared implicit are surrounded by square
+brackets and the ones to be declared as maximally inserted implicits are
+surrounded by curly braces.
 
 After the above declaration is issued, implicit arguments can just (and
 have to) be skipped in any expression involving an application of
@@ -1591,7 +1591,7 @@ Implicit arguments names can be redefined using the following syntax:
 {\tt Arguments {\qualid} \nelist{\name}{}  : rename}
 \end{quote}
 
-Without the {\tt rename} flag, {\tt Arguments} can be used to assert
+With the {\tt assert} flag, {\tt Arguments} can be used to assert
 that a given object has the expected number of arguments and that
 these arguments are named as expected.
 
@@ -1600,7 +1600,7 @@ these arguments are named as expected.
 Arguments p [s t] _ [u] _: rename.
 Check (p r1 (u:=c)).
 Check (p (s:=a) (t:=b) r1 (u:=c) r2).
-Fail Arguments p [s t] _ [w] _.
+Fail Arguments p [s t] _ [w] _ : assert.
 \end{coq_example}
 
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 92107b750b..1fcc1c0df4 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -811,13 +811,13 @@ constant have to be interpreted in a given scope. The command is
 \begin{quote}
 {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
 \end{quote}
-where the list is the list of the arguments of {\qualid} eventually
-annotated with their {\scope}. Grouping round parentheses can
-be used to decorate multiple arguments with the same scope.
-{\scope} can be either a scope name or its delimiting key. For example
-the following command puts the first two arguments of {\tt plus\_fct}
-in the scope delimited by the key {\tt F} ({\tt Rfun\_scope}) and the
-last argument in the scope delimited by the key {\tt R} ({\tt R\_scope}).
+where the list is a prefix of the list of the arguments of {\qualid} eventually
+annotated with their {\scope}. Grouping round parentheses can be used to
+decorate multiple arguments with the same scope.  {\scope} can be either a scope
+name or its delimiting key. For example the following command puts the first two
+arguments of {\tt plus\_fct} in the scope delimited by the key {\tt F} ({\tt
+  Rfun\_scope}) and the last argument in the scope delimited by the key {\tt R}
+({\tt R\_scope}).
 
 \begin{coq_example*}
 Arguments plus_fct (f1 f2)%F x%R.