Define many undefined tokens, and other misc fixes.

Progress towards #9411, extracted from #10118, rebased ontop of #10192.

3 files changed, 72 insertions, 90 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 68f6d4008a..e58049b8d0 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -528,7 +528,7 @@ pass additional arguments such as ``using relation``.
 .. tacv:: setoid_reflexivity
           setoid_symmetry {? in @ident}
           setoid_transitivity
-          setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident}
+          setoid_rewrite {? @orientation} @term {? at @occurrences} {? in @ident}
           setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic}
    :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; setoid_replace
 
@@ -567,13 +567,13 @@ Printing relations and morphisms
 Deprecated syntax and backward incompatibilities
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Add Setoid @A @Aeq @ST as @ident
+.. cmd:: Add Setoid @qualid__1 @qualid__2 @qualid__3 as @ident
 
    This command for declaring setoids and morphisms is also accepted due
    to backward compatibility reasons.
 
-   Here ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier
-   and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record
+   Here :n:`@qualid__2` is a congruence relation without parameters, :n:`@qualid__1` is its carrier
+   and :n:`@qualid__3` is an object of type (:n:`Setoid_Theory @qualid__1 @qualid__2`) (i.e. a record
    packing together the reflexivity, symmetry and transitivity lemmas).
    Notice that the syntax is not completely backward compatible since the
    identifier was not required.
@@ -708,91 +708,65 @@ Definitions
 The generalized rewriting tactic is based on a set of strategies that can be
 combined to obtain custom rewriting procedures. Its set of strategies is based
 on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting
-strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a
+strategies are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a
 strategy expression. Strategies are defined inductively as described by the
 following grammar:
 
-.. productionlist:: rewriting
-   s, t, u : `strategy`
-           : `lemma`
-           : `lemma_right_to_left`
-           : `failure`
-           : `identity`
-           : `reflexivity`
-           : `progress`
-           : `failure_catch`
-           : `composition`
-           : `left_biased_choice`
-           : `iteration_one_or_more`
-           : `iteration_zero_or_more`
-           : `one_subterm`
-           : `all_subterms`
-           : `innermost_first`
-           : `outermost_first`
-           : `bottom_up`
-           : `top_down`
-           : `apply_hint`
-           : `any_of_the_terms`
-           : `apply_reduction`
-           : `fold_expression`
-
-.. productionlist:: rewriting
-   strategy : ( `s` )
-   lemma : `c`
-   lemma_right_to_left : <- `c`
-   failure : fail
-   identity : id
-   reflexivity : refl
-   progress : progress `s`
-   failure_catch : try `s`
-   composition : `s` ; `u`
-   left_biased_choice : choice `s` `t`
-   iteration_one_or_more : repeat `s`
-   iteration_zero_or_more : any `s`
-   one_subterm : subterm `s`
-   all_subterms : subterms `s`
-   innermost_first : innermost `s`
-   outermost_first : outermost `s`
-   bottom_up : bottomup `s`
-   top_down : topdown `s`
-   apply_hint : hints `hintdb`
-   any_of_the_terms : terms (`c`)+
-   apply_reduction : eval `redexpr`
-   fold_expression : fold `c`
-
+.. productionlist:: coq
+   strategy : `qualid`                   (lemma, left to right)
+            : <- `qualid`                (lemma, right to left)
+            : fail                    (failure)
+            : id                      (identity)
+            : refl                    (reflexivity)
+            : progress `strategy`        (progress)
+            : try `strategy`             (try catch)
+            : `strategy` ; `strategy`       (composition)
+            : choice `strategy` `strategy`  (left_biased_choice)
+            : repeat `strategy`          (one or more)
+            : any `strategy`             (zero or more)
+            : subterm `strategy`         (one subterm)
+            : subterms `strategy`        (all subterms)
+            : innermost `strategy`       (innermost first)
+            : outermost `strategy`       (outermost first)
+            : bottomup `strategy`        (bottom-up)
+            : topdown `strategy`         (top-down)
+            : hints `ident`              (apply hints from hint database)
+            : terms `term` ... `term`      (any of the terms)
+            : eval `redexpr`             (apply reduction)
+            : fold `term`               (unify)
+            : ( `strategy` )
 
 Actually a few of these are defined in term of the others using a
 primitive fixpoint operator:
 
-.. productionlist:: rewriting
-   try `s` : choice `s` `id`
-   any `s` : fix `u`. try (`s` ; `u`)
-   repeat `s` : `s` ; any `s`
-   bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu
-   topdown s : fix `td`. (choice s (progress (subterms td))) ; try td
-   innermost s : fix `i`. (choice (subterm i) s)
-   outermost s : fix `o`. (choice s (subterm o))
+- :n:`try @strategy := choice @strategy id`
+- :n:`any @strategy := fix @ident. try (@strategy ; @ident)`
+- :n:`repeat @strategy := @strategy; any @strategy`
+- :n:`bottomup @strategy := fix @ident. (choice (progress (subterms @ident)) @strategy) ; try @ident`
+- :n:`topdown @strategy := fix @ident. (choice @strategy (progress (subterms @ident))) ; try @ident`
+- :n:`innermost @strategy := fix @ident. (choice (subterm @ident) @strategy)`
+- :n:`outermost @strategy := fix @ident. (choice @strategy (subterm @ident))`
 
 The basic control strategy semantics are straightforward: strategies
 are applied to subterms of the term to rewrite, starting from the root
 of the term. The lemma strategies unify the left-hand-side of the
 lemma with the current subterm and on success rewrite it to the right-
 hand-side. Composition can be used to continue rewriting on the
-current subterm. The fail strategy always fails while the identity
+current subterm. The ``fail`` strategy always fails while the identity
 strategy succeeds without making progress. The reflexivity strategy
 succeeds, making progress using a reflexivity proof of rewriting.
-Progress tests progress of the argument strategy and fails if no
+``progress`` tests progress of the argument :token:`strategy` and fails if no
 progress was made, while ``try`` always succeeds, catching failures.
-Choice is left-biased: it will launch the first strategy and fall back
+``choice`` is left-biased: it will launch the first strategy and fall back
 on the second one in case of failure. One can iterate a strategy at
 least 1 time using ``repeat`` and at least 0 times using ``any``.
 
-The ``subterm`` and ``subterms`` strategies apply their argument strategy ``s`` to
+The ``subterm`` and ``subterms`` strategies apply their argument :token:`strategy` to
 respectively one or all subterms of the current term under
 consideration, left-to-right. ``subterm`` stops at the first subterm for
-which ``s`` made progress. The composite strategies ``innermost`` and ``outermost``
+which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost``
 perform a single innermost or outermost rewrite using their argument
-strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many
+:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many
 rewritings as possible, starting from the bottom or the top of the
 term.
 
@@ -802,15 +776,15 @@ lemmas at the current subterm. The ``terms`` strategy takes the lemma
 names directly as arguments. The ``eval`` strategy expects a reduction
 expression (see :ref:`performingcomputations`) and succeeds
 if it reduces the subterm under consideration. The ``fold`` strategy takes
-a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c``
-on success, it is stronger than the tactic ``fold``.
+a :token:`term` and tries to *unify* it to the current subterm, converting it to :token:`term`
+on success. It is stronger than the tactic ``fold``.
 
 
 Usage
 ~~~~~
 
 
-.. tacn:: rewrite_strat @s {? in @ident }
+.. tacn:: rewrite_strat @strategy {? in @ident }
    :name: rewrite_strat
 
    Rewrite using the strategy s in hypothesis ident or the conclusion.
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 3b350d5dc0..3f4d5cc784 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -310,10 +310,10 @@ The syntax for adding a new ring is
    .. productionlist:: coq
       ring_mod : abstract | decidable `term` | morphism `term`
                : setoid `term` `term`
-               : constants [`ltac`]
-               : preprocess [`ltac`]
-               : postprocess [`ltac`]
-               : power_tac `term` [`ltac`]
+               : constants [ `tactic` ]
+               : preprocess [ `tactic` ]
+               : postprocess [ `tactic` ]
+               : power_tac `term` [ `tactic` ]
                : sign `term`
                : div `term`
 
@@ -341,31 +341,31 @@ The syntax for adding a new ring is
       This modifier needs not be used if the setoid and morphisms have been
       declared.
 
-   constants [ :n:`@ltac` ]
-      specifies a tactic expression :n:`@ltac` that, given a
+   constants [ :n:`@tactic` ]
+      specifies a tactic expression :n:`@tactic` that, given a
       term, returns either an object of the coefficient set that is mapped
       to the expression via the morphism, or returns
       ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1
       to their counterpart in the coefficient set. This is generally not
       desirable for non trivial computational rings.
 
-   preprocess [ :n:`@ltac` ]
-      specifies a tactic :n:`@ltac` that is applied as a
+   preprocess [ :n:`@tactic` ]
+      specifies a tactic :n:`@tactic` that is applied as a
       preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to
       transform a goal so that it is better recognized. For instance, ``S n``
       can be changed to ``plus 1 n``.
 
-   postprocess [ :n:`@ltac` ]
-      specifies a tactic :n:`@ltac` that is applied as a final
+   postprocess [ :n:`@tactic` ]
+      specifies a tactic :n:`@tactic` that is applied as a final
       step for :tacn:`ring_simplify`. For instance, it can be used to undo
       modifications of the preprocessor.
 
-   power_tac :n:`@term` [ :n:`@ltac` ]
+   power_tac :n:`@term` [ :n:`@tactic` ]
       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize
       power expressions with a constant positive integer exponent (example:
       :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies
       the specification of a power function (term has to be a proof of
-      ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression
+      ``Ring_theory.power_theory``) and :n:`@tactic` specifies a tactic expression
       that, given a term, “abstracts” it into an object of type |N| whose
       interpretation via ``Cp_phi`` (the evaluation function of power
       coefficient) is the original term, or returns ``InitialRing.NotConstant``
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 1aa2111816..395b5ce2d3 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -366,24 +366,32 @@ The syntax has been extended to allow users to explicitly bind names
 to universes and explicitly instantiate polymorphic definitions.
 
 .. cmd:: Universe @ident
+         Polymorphic Universe @ident
 
    In the monorphic case, this command declares a new global universe
    named :g:`ident`, which can be referred to using its qualified name
    as well. Global universe names live in a separate namespace. The
-   command supports the polymorphic flag only in sections, meaning the
+   command supports the ``Polymorphic`` flag only in sections, meaning the
    universe quantification will be discharged on each section definition
    independently. One cannot mix polymorphic and monomorphic
    declarations in the same section.
 
 
-.. cmd:: Constraint @ident @ord @ident
+.. cmd:: Constraint @universe_constraint
+         Polymorphic Constraint @universe_constraint
 
-   This command declares a new constraint between named universes. The
-   order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint
-   is then enforced in the global environment. Like ``Universe``, it can be
-   used with the ``Polymorphic`` prefix in sections only to declare
-   constraints discharged at section closing time. One cannot declare a
-   global constraint on polymorphic universes.
+   This command declares a new constraint between named universes.
+
+   .. productionlist:: coq
+      universe_constraint : `qualid` < `qualid`
+                          : `qualid` <= `qualid`
+                          : `qualid` = `qualid`
+
+   If consistent, the constraint is then enforced in the global
+   environment. Like :cmd:`Universe`, it can be used with the
+   ``Polymorphic`` prefix in sections only to declare constraints
+   discharged at section closing time. One cannot declare a global
+   constraint on polymorphic universes.
 
    .. exn:: Undeclared universe @ident.
       :undocumented: