Convert syntax extensions chapter to prodn

3 files changed, 484 insertions, 243 deletions

diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
new file mode 100644
index 0000000000..34a48b368b
--- /dev/null
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -0,0 +1,440 @@
+.. _ArgumentsCommand:
+
+Setting properties of a function's arguments
+++++++++++++++++++++++++++++++++++++++++++++
+
+.. cmd:: Arguments @smart_qualid {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } }
+   :name: Arguments
+
+   .. insertprodn smart_qualid args_modifier
+
+   .. prodn::
+      smart_qualid ::= @qualid
+      | @by_notation
+      by_notation ::= @string {? % @scope_key }
+      argument_spec ::= {? ! } @name {? % @scope_key }
+      arg_specs ::= @argument_spec
+      | /
+      | &
+      | ( {+ @argument_spec } ) {? % @scope_key }
+      | [ {+ @argument_spec } ] {? % @scope_key }
+      | %{ {+ @argument_spec } %} {? % @scope_key }
+      implicits_alt ::= @name
+      | [ {+ @name } ]
+      | %{ {+ @name } %}
+      args_modifier ::= simpl nomatch
+      | simpl never
+      | default implicits
+      | clear implicits
+      | clear scopes
+      | clear bidirectionality hint
+      | rename
+      | assert
+      | extra scopes
+      | clear scopes and implicits
+      | clear implicits and scopes
+
+   Specifies properties of the arguments of a function after the function has already
+   been defined.  It gives fine-grained
+   control over the elaboration process (i.e. the translation of Gallina language
+   extensions into the core language used by the kernel).  The command's effects include:
+
+   * Making arguments implicit. Afterward, implicit arguments
+     must be omitted in any expression that applies :token:`smart_qualid`.
+   * Declaring that some arguments of a given function should
+     be interpreted in a given scope.
+   * Affecting when the :tacn:`simpl` and :tacn:`cbn` tactics unfold the function.
+     See :ref:`Args_effect_on_unfolding`.
+   * Providing bidirectionality hints.  See :ref:`bidirectionality_hints`.
+
+   This command supports the :attr:`local` and :attr:`global` attributes.
+   Default behavior is to limit the effect to the current section but also to
+   extend their effect outside the current module or library file.
+   Applying :attr:`local` limits the effect of the command to the current module if
+   it's not in a section.  Applying :attr:`global` within a section extends the
+   effect outside the current sections and current module in which the command appears.
+
+      `/`
+         the function will be unfolded only if it's applied to at least the
+         arguments appearing before the `/`.  See :ref:`Args_effect_on_unfolding`.
+
+         .. exn:: The / modifier may only occur once.
+            :undocumented:
+
+      `&`
+         tells the type checking algorithm to first type check the arguments
+         before the `&` and then to propagate information from that typing context
+         to type check the remaining arguments. See :ref:`bidirectionality_hints`.
+
+         .. exn:: The & modifier may only occur once.
+            :undocumented:
+
+      :n:`( ... ) {? % @scope }`
+         :n:`(@name__1 @name__2 ...)%@scope` is shorthand for :n:`@name__1%@scope @name__2%@scope ...`
+
+      :n:`[ ... ] {? % @scope }`
+         declares the enclosed names as implicit, non-maximally inserted.
+         :n:`[@name__1 @name__2 ... ]%@scope` is equivalent to :n:`[@name__1]%@scope [@name__2]%@scope ...`
+
+      :n:`%{ ... %} {? % @scope }`
+         declares the enclosed names as implicit, maximally inserted.
+         :n:`%{@name__1 @name__2 ... %}%@scope` is equivalent to :n:`%{@name__1%}%@scope %{@name__2%}%@scope ...`
+
+      `!`
+         the function will be unfolded only if all the arguments marked with `!`
+         evaulate to constructors.  See :ref:`Args_effect_on_unfolding`.
+
+      :n:`@name {? % @scope }`
+         a *formal parameter* of the function :n:`@smart_qualid` (i.e.
+         the parameter name used in the function definition).  Unless `rename` is specified,
+         the list of :n:`@name`\s must be a prefix of the formal parameters, including all implicit
+         arguments.  `_` can be used to skip over a formal parameter.
+         :token:`scope` can be either a scope name or its delimiting key.  See :ref:`binding_to_scope`.
+
+      `clear implicits`
+         makes all implicit arguments into explicit arguments
+      `default implicits`
+         automatically determine the implicit arguments of the object.
+         See :ref:`auto_decl_implicit_args`.
+      `rename`
+         rename implicit arguments for the object.  See the example :ref:`here <renaming_implicit_arguments>`.
+      `assert`
+         assert that the object has the expected number of arguments with the
+         expected names.  See the example here: :ref:`renaming_implicit_arguments`.
+
+         .. warn:: This command is just asserting the names of arguments of @qualid. If this is what you want, add ': assert' to silence the warning. If you want to clear implicit arguments, add ': clear implicits'. If you want to clear notation scopes, add ': clear scopes'
+            :undocumented:
+
+      `clear scopes`
+         clears argument scopes of :n:`@smart_qualid`
+      `extra scopes`
+         defines extra argument scopes, to be used in case of coercion to ``Funclass``
+         (see the :ref:`implicitcoercions` chapter) or with a computed type.
+      `simpl nomatch`
+         prevents performing a simplification step for :n:`@smart_qualid`
+         that would expose a match construct in the head position.  See :ref:`Args_effect_on_unfolding`.
+      `simpl never`
+         prevents performing a simplification step for :n:`@smart_qualid`.  See :ref:`Args_effect_on_unfolding`.
+
+      `clear bidirectionality hint`
+         removes the bidirectionality hint, the `&`
+
+      :n:`@implicits_alt`
+         use to specify alternative implicit argument declarations
+         for functions that can only be
+         applied to a fixed number of arguments (excluding, for instance,
+         functions whose type is polymorphic).
+         For parsing, the longest list of implicit arguments matching the function application
+         is used to select which implicit arguments are inserted.
+         For printing, the alternative with the most implicit arguments is used; the
+         implict arguments will be omitted if :flag:`Printing Implicit` is not set.
+         See the example :ref:`here<example_more_implicits>`.
+
+         .. todo the above feature seems a bit unnatural and doesn't play well with partial
+            application.  See https://github.com/coq/coq/pull/11718#discussion_r408841762
+
+   Use :cmd:`About` to view the current implicit arguments setting for a :token:`smart_qualid`.
+
+   Or use the :cmd:`Print Implicit` command to see the implicit arguments
+   of an object (see :ref:`displaying-implicit-args`).
+
+Manual declaration of implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. example::
+
+   .. coqtop:: reset all
+
+      Inductive list (A : Type) : Type :=
+      | nil : list A
+      | cons : A -> list A -> list A.
+
+      Check (cons nat 3 (nil nat)).
+
+      Arguments cons [A] _ _.
+
+      Arguments nil {A}.
+
+      Check (cons 3 nil).
+
+      Fixpoint map (A B : Type) (f : A -> B) (l : list A) : list B :=
+        match l with nil => nil | cons a t => cons (f a) (map A B f t) end.
+
+      Fixpoint length (A : Type) (l : list A) : nat :=
+        match l with nil => 0 | cons _ m => S (length A m) end.
+
+      Arguments map [A B] f l.
+
+      Arguments length {A} l. (* A has to be maximally inserted *)
+
+      Check (fun l:list (list nat) => map length l).
+
+.. _example_more_implicits:
+
+.. example:: Multiple alternatives with :n:`@implicits_alt`
+
+   .. coqtop:: all
+
+      Arguments map [A B] f l, [A] B f l, A B f l.
+
+      Check (fun l => map length l = map (list nat) nat length l).
+
+.. _auto_decl_implicit_args:
+
+Automatic declaration of implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+   The ":n:`default implicits`" :token:`args_modifier` clause tells |Coq| to automatically determine the
+   implicit arguments of the object.
+
+   Auto-detection is governed by flags specifying whether strict,
+   contextual, or reversible-pattern implicit arguments must be
+   considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-contextual-implicit-args`,
+   :ref:`controlling-rev-pattern-implicit-args` and also :ref:`controlling-insertion-implicit-args`).
+
+.. example:: Default implicits
+
+   .. coqtop:: reset all
+
+      Inductive list (A:Set) : Set :=
+      | nil : list A
+      | cons : A -> list A -> list A.
+
+      Arguments cons : default implicits.
+
+      Print Implicit cons.
+
+      Arguments nil : default implicits.
+
+      Print Implicit nil.
+
+      Set Contextual Implicit.
+
+      Arguments nil : default implicits.
+
+      Print Implicit nil.
+
+The computation of implicit arguments takes account of the unfolding
+of constants. For instance, the variable ``p`` below has type
+``(Transitivity R)`` which is reducible to
+``forall x,y:U, R x y -> forall z:U, R y z -> R x z``. As the variables ``x``, ``y`` and ``z``
+appear strictly in the body of the type, they are implicit.
+
+.. coqtop:: all
+
+   Parameter X : Type.
+
+   Definition Relation := X -> X -> Prop.
+
+   Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z.
+
+   Parameters (R : Relation) (p : Transitivity R).
+
+   Arguments p : default implicits.
+
+   Print p.
+
+   Print Implicit p.
+
+   Parameters (a b c : X) (r1 : R a b) (r2 : R b c).
+
+   Check (p r1 r2).
+
+
+.. _renaming_implicit_arguments:
+
+Renaming implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. example:: (continued)  Renaming implicit arguments
+
+   .. coqtop:: all
+
+      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] _ : assert.
+
+.. _binding_to_scope:
+
+Binding arguments to a scope
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+   The following command declares that the first two arguments of :g:`plus_fct`
+   are in the :token:`scope` delimited by the key ``F`` (``Rfun_scope``) and the third
+   argument is in the scope delimited by the key ``R`` (``R_scope``).
+
+      .. coqdoc::
+
+         Arguments plus_fct (f1 f2)%F x%R.
+
+   When interpreting a term, if some of the arguments of :token:`smart_qualid` are built
+   from a notation, then this notation is interpreted in the scope stack
+   extended by the scope bound (if any) to this argument. The effect of
+   the scope is limited to the argument itself. It does not propagate to
+   subterms but the subterms that, after interpretation of the notation,
+   turn to be themselves arguments of a reference are interpreted
+   accordingly to the argument scopes bound to this reference.
+
+.. note::
+
+   In notations, the subterms matching the identifiers of the
+   notations are interpreted in the scope in which the identifiers
+   occurred at the time of the declaration of the notation. Here is an
+   example:
+
+   .. coqtop:: all
+
+      Parameter g : bool -> bool.
+      Declare Scope mybool_scope.
+
+      Notation "@@" := true (only parsing) : bool_scope.
+      Notation "@@" := false (only parsing): mybool_scope.
+
+      Bind Scope bool_scope with bool.
+      Notation "# x #" := (g x) (at level 40).
+      Check # @@ #.
+      Arguments g _%mybool_scope.
+      Check # @@ #.
+      Delimit Scope mybool_scope with mybool.
+      Check # @@%mybool #.
+
+.. _Args_effect_on_unfolding:
+
+Effects of :cmd:`Arguments` on unfolding
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
++ `simpl never` indicates that a constant should never be unfolded by :tacn:`cbn`,
+  :tacn:`simpl` or :tacn:`hnf`:
+
+  .. example::
+
+     .. coqtop:: all
+
+        Arguments minus n m : simpl never.
+
+  After that command an expression like :g:`(minus (S x) y)` is left
+  untouched by the tactics :tacn:`cbn` and :tacn:`simpl`.
+
++ A constant can be marked to be unfolded only if it's applied to at least
+  the arguments appearing before the `/` in a :cmd:`Arguments` command.
+
+  .. example::
+
+     .. coqtop:: all
+
+        Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
+        Arguments fcomp {A B C} f g x /.
+        Notation "f \o g" := (fcomp f g) (at level 50).
+
+  After that command the expression :g:`(f \o g)` is left untouched by
+  :tacn:`simpl` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`.
+  The same mechanism can be used to make a constant volatile, i.e.
+  always unfolded.
+
+  .. example::
+
+     .. coqtop:: all
+
+        Definition volatile := fun x : nat => x.
+        Arguments volatile / x.
+
++ A constant can be marked to be unfolded only if an entire set of
+  arguments evaluates to a constructor. The ``!`` symbol can be used to mark
+  such arguments.
+
+  .. example::
+
+     .. coqtop:: all
+
+        Arguments minus !n !m.
+
+  After that command, the expression :g:`(minus (S x) y)` is left untouched
+  by :tacn:`simpl`, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`.
+
++ `simpl nomatch` indicates that a constant should not be unfolded if it would expose
+  a `match` construct in the head position.  This affects the :tacn:`cbn`,
+  :tacn:`simpl` and :tacn:`hnf` tactics.
+
+  .. example::
+
+     .. coqtop:: all
+
+        Arguments minus n m : simpl nomatch.
+
+  In this case, :g:`(minus (S (S x)) (S y))` is simplified to :g:`(minus (S x) y)`
+  even if an extra simplification is possible.
+
+  In detail: the tactic :tacn:`simpl` first applies :math:`\beta`:math:`\iota`-reduction. Then, it
+  expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`-reduction.
+  But, when no :math:`\iota` rule is applied after unfolding then
+  :math:`\delta`-reductions are not applied. For instance trying to use :tacn:`simpl` on
+  :g:`(plus n O) = n` changes nothing.
+
+
+.. _bidirectionality_hints:
+
+Bidirectionality hints
+~~~~~~~~~~~~~~~~~~~~~~
+
+When type-checking an application, Coq normally does not use information from
+the context to infer the types of the arguments. It only checks after the fact
+that the type inferred for the application is coherent with the expected type.
+Bidirectionality hints make it possible to specify that after type-checking the
+first arguments of an application, typing information should be propagated from
+the context to help inferring the types of the remaining arguments.
+
+.. todo the following text is a start on better wording but not quite complete.
+   See https://github.com/coq/coq/pull/11718#discussion_r410219992
+
+  ..
+  Two common methods to determine the type of a construct are:
+
+  * *type checking*, which is verifying that a construct matches a known type, and
+  * *type inference*, with is inferring the type of a construct by analyzing the construct.
+
+  Methods that combine these approaches are known as *bidirectional typing*.
+  Coq normally uses only the first approach to infer the types of arguments,
+  then later verifies that the inferred type is consistent with the expected type.
+  *Bidirectionality hints* specify to use both methods: after type checking the
+  first arguments of an application (appearing before the `&` in :cmd:`Arguments`),
+  typing information from them is propagated to the remaining arguments to help infer their types.
+
+An :cmd:`Arguments` command containing :n:`@arg_specs__1 & @arg_specs__2`
+provides bidirectionality hints.
+It tells the typechecking algorithm, when type checking
+applications of :n:`@qualid`, to first type check the arguments in
+:n:`@arg_specs__1` and then propagate information from the typing context to
+type check the remaining arguments (in :n:`@arg_specs__2`).
+
+.. example:: Bidirectionality hints
+
+   In a context where a coercion was declared from ``bool`` to ``nat``:
+
+   .. coqtop:: in reset
+
+      Definition b2n (b : bool) := if b then 1 else 0.
+      Coercion b2n : bool >-> nat.
+
+   Coq cannot automatically coerce existential statements over ``bool`` to
+   statements over ``nat``, because the need for inserting a coercion is known
+   only from the expected type of a subterm:
+
+   .. coqtop:: all
+
+      Fail Check (ex_intro _ true _ : exists n : nat, n > 0).
+
+   However, a suitable bidirectionality hint makes the example work:
+
+   .. coqtop:: all
+
+      Arguments ex_intro _ _ & _ _.
+      Check (ex_intro _ true _ : exists n : nat, n > 0).
+
+Coq will attempt to produce a term which uses the arguments you
+provided, but in some cases involving Program mode the arguments after
+the bidirectionality starts may be replaced by convertible but
+syntactically different terms.
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index 36ce2fdd25..d93dc00e24 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -105,28 +105,26 @@ This corresponds to a class of non-dependent implicit arguments that
 are solved based on the structure of their type only.
 
 
-Maximal or non maximal insertion of implicit arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Maximal and non-maximal insertion of implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-In case a function is partially applied, and the next argument to be
-applied is an implicit argument, two disciplines are applicable. In
-the first case, the function is considered to have no arguments
-furtherly: one says that the implicit argument is not maximally
-inserted. In the second case, the function is considered to be
-implicitly applied to the implicit arguments it is waiting for: one
-says that the implicit argument is maximally inserted.
+When a function is partially applied and the next argument to
+apply is an implicit argument, the application can be interpreted in two ways.
+If the next argument is declared as *maximally inserted*, the partial
+application will include that argument.  Otherwise, the argument is
+*non-maximally inserted* and the partial application will not include that argument.
 
 Each implicit argument can be declared to be inserted maximally or non
-maximally. In Coq, maximally-inserted implicit arguments are written between curly braces
-"{ }" and non-maximally-inserted implicit arguments are written in square brackets "[ ]".
+maximally. In Coq, maximally inserted implicit arguments are written between curly braces
+"{ }" and non-maximally inserted implicit arguments are written in square brackets "[ ]".
 
 .. seealso:: :flag:`Maximal Implicit Insertion`
 
 Trailing Implicit Arguments
 +++++++++++++++++++++++++++
 
-An implicit argument is considered trailing when all following arguments are declared
-implicit. Trailing implicit arguments cannot be declared non maximally inserted,
+An implicit argument is considered *trailing* when all following arguments are
+implicit. Trailing implicit arguments must be declared as maximally inserted;
 otherwise they would never be inserted.
 
 .. exn:: Argument @name is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ].
@@ -141,10 +139,9 @@ otherwise they would never be inserted.
 Casual use of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-In a given expression, if it is clear that some argument of a function
-can be inferred from the type of the other arguments, the user can
-force the given argument to be guessed by replacing it by “_”. If
-possible, the correct argument will be automatically generated.
+If an argument of a function application can be inferred from the type
+of the other arguments, the user can force inference of the argument
+by replacing it with `_`.
 
 .. exn:: Cannot infer a term for this placeholder.
    :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments)
@@ -156,12 +153,8 @@ possible, the correct argument will be automatically generated.
 Declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-In case one wants that some arguments of a given object (constant,
-inductive types, constructors, assumptions, local or not) are always
-inferred by |Coq|, one may declare once and for all which are the
-expected implicit arguments of this object. There are two ways to do
-this, *a priori* and *a posteriori*.
-
+Implicit arguments can be declared when a function is declared or
+afterwards, using the :cmd:`Arguments` command.
 
 Implicit Argument Binders
 +++++++++++++++++++++++++
@@ -172,18 +165,20 @@ Implicit Argument Binders
    implicit_binders ::= %{ {+ @name } {? : @type } %}
    | [ {+ @name } {? : @type } ]
 
-In the first setting, one wants to explicitly give the implicit
-arguments of a declared object as part of its definition. To do this,
-one has to surround the bindings of implicit arguments by curly
-braces or square braces:
+In the context of a function definition, these forms specify that
+:token:`name` is an implicit argument.  The first form, with curly
+braces, makes :token:`name` a maximally inserted implicit argument.  The second
+form, with square brackets, makes :token:`name` a non-maximally inserted implicit argument.
+
+For example:
 
 .. coqtop:: all
 
    Definition id {A : Type} (x : A) : A := x.
 
-This automatically declares the argument A of id as a maximally
-inserted implicit argument. One can then do as-if the argument was
-absent in every situation but still be able to specify it if needed:
+declares the argument `A` of `id` as a maximally
+inserted implicit argument. `A` may be omitted
+in applications of `id` but may be specified if needed:
 
 .. coqtop:: all
 
@@ -191,7 +186,7 @@ absent in every situation but still be able to specify it if needed:
 
    Goal forall A, compose id id = id (A:=A).
 
-For non maximally inserted implicit arguments, use square brackets:
+For non-maximally inserted implicit arguments, use square brackets:
 
 .. coqtop:: all
 
@@ -203,8 +198,7 @@ For non maximally inserted implicit arguments, use square brackets:
 
    Print Implicit map.
 
-The syntax is supported in all top-level definitions:
-:cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype
+For (co-)inductive datatype
 declarations, the semantics are the following: an inductive parameter
 declared as an implicit argument need not be repeated in the inductive
 definition and will become implicit for the inductive type and the constructors.
@@ -225,11 +219,12 @@ The syntax is also supported in internal binders. For instance, in the
 following kinds of expressions, the type of each declaration present
 in :token:`binders` can be bracketed to mark the declaration as
 implicit:
-:n:`fun (@ident:forall {* @binder }, @type) => @term`,
-:n:`forall (@ident:forall {* @binder }, @type), @type`,
-:n:`let @ident {* @binder } := @term in @term`,
-:n:`fix @ident {* @binder } := @term in @term` and
-:n:`cofix @ident {* @binder } := @term in @term`.
+* :n:`fun (@ident:forall {* @binder }, @type) => @term`,
+* :n:`forall (@ident:forall {* @binder }, @type), @type`,
+* :n:`let @ident {* @binder } := @term in @term`,
+* :n:`fix @ident {* @binder } := @term in @term` and
+* :n:`cofix @ident {* @binder } := @term in @term`.
+
 Here is an example:
 
 .. coqtop:: all
@@ -259,190 +254,6 @@ Here is an example:
 
       Check let g {x:nat} (H:x=x) {x} (H:x=x) := x in 0.
 
-
-Declaring Implicit Arguments
-++++++++++++++++++++++++++++
-
-
-
-.. cmd:: Arguments @smart_qualid {* @argument_spec_block } {* , {* @more_implicits_block } } {? : {+, @arguments_modifier } }
-   :name: Arguments
-
-   .. insertprodn smart_qualid arguments_modifier
-
-   .. prodn::
-      smart_qualid ::= @qualid
-      | @by_notation
-      by_notation ::= @string {? % @scope }
-      argument_spec_block ::= @argument_spec
-      | /
-      | &
-      | ( {+ @argument_spec } ) {? % @scope }
-      | [ {+ @argument_spec } ] {? % @scope }
-      | %{ {+ @argument_spec } %} {? % @scope }
-      argument_spec ::= {? ! } @name {? % @scope }
-      more_implicits_block ::= @name
-      | [ {+ @name } ]
-      | %{ {+ @name } %}
-      arguments_modifier ::= simpl nomatch
-      | simpl never
-      | default implicits
-      | clear bidirectionality hint
-      | clear implicits
-      | clear scopes
-      | clear scopes and implicits
-      | clear implicits and scopes
-      | rename
-      | assert
-      | extra scopes
-
-   This command sets implicit arguments *a posteriori*,
-   where the list of :n:`@name`\s is a prefix of the list of
-   arguments of :n:`@smart_qualid`.  Arguments in square
-   brackets are declared as implicit and arguments in curly brackets are declared as
-   maximally inserted.
-
-   After the command is issued, implicit arguments can and must be
-   omitted in any expression that applies :token:`qualid`.
-
-   This command supports the :attr:`local` and :attr:`global` attributes.
-   Default behavior is to limit the effect to the current section but also to
-   extend their effect outside the current module or library file.
-   Applying :attr:`local` limits the effect of the command to the current module if
-   it's not in a section.  Applying :attr:`global` within a section extends the
-   effect outside the current sections and current module if the command occurs.
-
-   A command containing :n:`@argument_spec_block & @argument_spec_block`
-   provides :ref:`bidirectionality_hints`.
-
-   Use the :n:`@more_implicits_block` to specify multiple implicit arguments declarations
-   for names of constants, inductive types, constructors and lemmas that can only be
-   applied to a fixed number of arguments (excluding, for instance,
-   constants whose type is polymorphic).
-   The longest applicable list of implicit arguments will be used to select which
-   implicit arguments are inserted.
-   For printing, the omitted arguments are the ones of the longest list of implicit
-   arguments of the sequence.  See the example :ref:`here<example_more_implicits>`.
-
-   The :n:`@arguments_modifier` values have various effects:
-
-   * :n:`clear implicits` - clears implicit arguments
-   * :n:`default implicits` - automatically determine the implicit arguments of the object.
-     See :ref:`auto_decl_implicit_args`.
-   * :n:`rename` - rename implicit arguments for the object
-   * :n:`assert` - assert that the object has the expected number of arguments with the
-     expected names.  See the example here: :ref:`renaming_implicit_arguments`.
-
-.. exn:: The / modifier may only occur once.
-   :undocumented:
-
-.. exn:: The & modifier may only occur once.
-   :undocumented:
-
-.. example::
-
-    .. coqtop:: reset all
-
-       Inductive list (A : Type) : Type :=
-       | nil : list A
-       | cons : A -> list A -> list A.
-
-       Check (cons nat 3 (nil nat)).
-
-       Arguments cons [A] _ _.
-
-       Arguments nil {A}.
-
-       Check (cons 3 nil).
-
-       Fixpoint map (A B : Type) (f : A -> B) (l : list A) : list B :=
-         match l with nil => nil | cons a t => cons (f a) (map A B f t) end.
-
-       Fixpoint length (A : Type) (l : list A) : nat :=
-         match l with nil => 0 | cons _ m => S (length A m) end.
-
-       Arguments map [A B] f l.
-
-       Arguments length {A} l. (* A has to be maximally inserted *)
-
-       Check (fun l:list (list nat) => map length l).
-
-.. _example_more_implicits:
-
-.. example:: Multiple implicit arguments with :n:`@more_implicits_block`
-
-   .. coqtop:: all
-
-       Arguments map [A B] f l, [A] B f l, A B f l.
-
-       Check (fun l => map length l = map (list nat) nat length l).
-
-.. note::
-   Use the :cmd:`Print Implicit` command to see the implicit arguments
-   of an object (see :ref:`displaying-implicit-args`).
-
-.. _auto_decl_implicit_args:
-
-Automatic declaration of implicit arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-   The :n:`default implicits @arguments_modifier` clause tells |Coq| to automatically determine the
-   implicit arguments of the object.
-
-   Auto-detection is governed by flags specifying whether strict,
-   contextual, or reversible-pattern implicit arguments must be
-   considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-contextual-implicit-args`,
-   :ref:`controlling-rev-pattern-implicit-args` and also :ref:`controlling-insertion-implicit-args`).
-
-.. example:: Default implicits
-
-   .. coqtop:: reset all
-
-       Inductive list (A:Set) : Set :=
-       | nil : list A
-       | cons : A -> list A -> list A.
-
-       Arguments cons : default implicits.
-
-       Print Implicit cons.
-
-       Arguments nil : default implicits.
-
-       Print Implicit nil.
-
-       Set Contextual Implicit.
-
-       Arguments nil : default implicits.
-
-       Print Implicit nil.
-
-The computation of implicit arguments takes account of the unfolding
-of constants. For instance, the variable ``p`` below has type
-``(Transitivity R)`` which is reducible to
-``forall x,y:U, R x y -> forall z:U, R y z -> R x z``. As the variables ``x``, ``y`` and ``z``
-appear strictly in the body of the type, they are implicit.
-
-.. coqtop:: all
-
-   Parameter X : Type.
-
-   Definition Relation := X -> X -> Prop.
-
-   Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z.
-
-   Parameters (R : Relation) (p : Transitivity R).
-
-   Arguments p : default implicits.
-
-   Print p.
-
-   Print Implicit p.
-
-   Parameters (a b c : X) (r1 : R a b) (r2 : R b c).
-
-   Check (p r1 r2).
-
-
 Mode for automatic declaration of implicit arguments
 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 
@@ -514,7 +325,7 @@ and the automatic declaration mode in on, the manual implicit arguments are adde
 automatically declared ones.
 
 In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off,
-some trailing implicit arguments can be inferred to be non maximally inserted. In
+some trailing implicit arguments can be inferred to be non-maximally inserted. In
 this case, they are converted to maximally inserted ones.
 
 .. example::
@@ -546,28 +357,17 @@ the hiding of implicit arguments for a single function application using the
 
     .. coqtop:: all
 
+       Parameter X : Type.
+       Definition Relation := X -> X -> Prop.
+       Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z.
+       Parameters (R : Relation) (p : Transitivity R).
+       Arguments p : default implicits.
+       Print Implicit p.
+       Parameters (a b c : X) (r1 : R a b) (r2 : R b c).
        Check (p r1 (z:=c)).
 
        Check (p (x:=a) (y:=b) r1 (z:=c) r2).
 
-
-.. _renaming_implicit_arguments:
-
-Renaming implicit arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-.. example:: (continued)  Renaming implicit arguments
-
-   .. coqtop:: all
-
-      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] _ : assert.
-
 .. _displaying-implicit-args:
 
 Displaying implicit arguments
@@ -668,7 +468,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
       Here is an example.
 
-      .. coqtop:: all
+      .. coqtop:: all reset
 
          Require Import Relations.
 
@@ -827,7 +627,7 @@ surrounding it with \`{ }, or \`[ ] or \`( ).
 
 Terms surrounded by \`{ } introduce their free variables as maximally
 inserted implicit arguments, terms surrounded by \`[ ] introduce them as
-non maximally inserted implicit arguments and terms surrounded by \`( )
+non-maximally inserted implicit arguments and terms surrounded by \`( )
 introduce them as explicit arguments.
 
 Generalizing binders always introduce their free variables as
diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst
index 627e7f0acb..fc2ce03093 100644
--- a/doc/sphinx/language/extensions/index.rst
+++ b/doc/sphinx/language/extensions/index.rst
@@ -20,6 +20,7 @@ language presented in the :ref:`previous chapter <core-language>`.
    implicit-arguments
    ../../addendum/extended-pattern-matching
    ../../user-extensions/syntax-extensions
+   arguments-command
    ../../addendum/implicit-coercions
    ../../addendum/type-classes
    ../../addendum/canonical-structures