Merge PR #11718: Convert syntax extensions chapter to prodn

Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: cpitclaudel

4 files changed, 16 insertions, 80 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 1772362351..c1eb1f974c 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -474,7 +474,7 @@ Soft cut
 ~~~~~~~~
 
 Another way of restricting backtracking is to restrict a tactic to a
-single success *a posteriori*:
+single success:
 
 .. tacn:: once @ltac_expr
    :name: once
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 06106a6b4c..35062e0057 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -510,9 +510,9 @@ Static semantics
 ****************
 
 During internalization, Coq variables are resolved and antiquotations are
-type-checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq
+type checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq
 implementation terminology. Note that although it went through the
-type-checking of **Ltac2**, the resulting term has not been fully computed and
+type checking of **Ltac2**, the resulting term has not been fully computed and
 is potentially ill-typed as a runtime **Coq** term.
 
 .. example::
@@ -523,12 +523,12 @@ is potentially ill-typed as a runtime **Coq** term.
 
       Ltac2 myconstr () := constr:(nat -> 0).
 
-Term antiquotations are type-checked in the enclosing Ltac2 typing context
+Term antiquotations are type checked in the enclosing Ltac2 typing context
 of the corresponding term expression.
 
 .. example::
 
-   The following will type-check, with type `constr`.
+   The following will type check, with type `constr`.
 
    .. coqdoc::
 
@@ -539,7 +539,7 @@ expanded by the Coq binders from the term.
 
   .. example::
 
-     The following Ltac2 expression will **not** type-check::
+     The following Ltac2 expression will **not** type check::
 
      `constr:(fun x : nat => ltac2:(exact x))`
      `(* Error: Unbound variable 'x' *)`
@@ -583,7 +583,7 @@ Dynamic semantics
 *****************
 
 During evaluation, a quoted term is fully evaluated to a kernel term, and is
-in particular type-checked in the current environment.
+in particular type checked in the current environment.
 
 Evaluation of a quoted term goes as follows.
 
@@ -602,7 +602,7 @@ whole expression will thus evaluate to the term :g:`fun H : nat => H`.
 
 `let tac () := hyp @H in constr:(fun H : nat => ltac2:(tac ()))`
 
-Many standard tactics perform type-checking of their argument before going
+Many standard tactics perform type checking of their argument before going
 further. It is your duty to ensure that terms are well-typed when calling
 such tactics. Failure to do so will result in non-recoverable exceptions.
 
@@ -700,7 +700,7 @@ The following scopes are built-in.
 
   + parses :n:`c = @term` and produces :n:`constr:(c)`
 
-  This scope can be parameterized by a list of delimiting keys of interpretation
+  This scope can be parameterized by a list of delimiting keys of notation
   scopes (as described in :ref:`LocalInterpretationRulesForNotations`),
   describing how to interpret the parsed term. For instance, :n:`constr(A, B)`
   parses :n:`c = @term` and produces :n:`constr:(c%A%B)`.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7e6da490fb..8989dd29ab 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3129,6 +3129,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    head normal form according to the :math:`\beta`:math:`\delta`:math:`\iota`:math:`\zeta`-reduction rules, i.e. it
    reduces the head of the goal until it becomes a product or an
    irreducible term. All inner :math:`\beta`:math:`\iota`-redexes are also reduced.
+   The behavior of both :tacn:`hnf` can be tuned using the :cmd:`Arguments` command.
 
    Example: The term :g:`fun n : nat => S n + S n` is not reduced by :n:`hnf`.
 
@@ -3155,76 +3156,10 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and
    :tacn:`lazy`. The behavior of both :tacn:`simpl` and :tacn:`cbn`
-   can be tuned using the Arguments vernacular command as follows:
+   can be tuned using the :cmd:`Arguments` command.
 
-   + A constant can be marked to be never unfolded by :tacn:`cbn` or
-     :tacn:`simpl`:
-
-     .. 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 applied to enough
-     arguments. The number of arguments required can be specified using the
-     ``/`` symbol in the argument list of the :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)`.
-
-   + A special heuristic to determine if a constant has to be unfolded
-     can be activated with the following command:
-
-     .. example::
-
-        .. coqtop:: all
-
-           Arguments minus n m : simpl nomatch.
-
-     The heuristic avoids to perform a simplification step that would expose a
-     match construct in head position. For example the expression
-     :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.
+   .. todo add "See <subsection about controlling the behavior of reduction strategies>"
+      to TBA section
 
    Notice that only transparent constants whose name can be reused in the
    recursive calls are possibly unfolded by :tacn:`simpl`. For instance a
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 60fdbf0a9d..3d69126b2d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -201,7 +201,8 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
    or an accessible theorem, axiom, etc.:
    its kind (module, constant, assumption, inductive,
    constructor, abbreviation, …), long name, type, implicit arguments and
-   argument scopes. It does not print the body of definitions or proofs.
+   argument scopes (as set in the definition of :token:`smart_qualid` or
+   subsequently with the :cmd:`Arguments` command). It does not print the body of definitions or proofs.
 
 .. cmd:: Check @term
 
@@ -230,7 +231,7 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
 
    .. prodn::
       search_item ::= @one_term
-      | @string {? % @scope }
+      | @string {? % @scope_key }
 
    Displays the name and type of all hypotheses of the
    selected goal (if any) and theorems of the current context