Remove some productionlists

10 files changed, 215 insertions, 152 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 89b4bda71a..0802b5d0b4 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -3,8 +3,8 @@
 =============================
 
 ..
-   README.rst is auto-generated from README.template.rst and the coqrst docs;
-   use ``doc/tools/coqrst/regen_readme.py`` to rebuild it.
+   README.rst is auto-generated from README.template.rst and the coqrst/*.py files
+   (in particular coqdomain.py).  Use ``doc/tools/coqrst/regen_readme.py`` to rebuild it.
 
 Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_.
 
@@ -97,7 +97,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
 ``.. cmd::`` :black_nib: A Coq command.
     Example::
 
-       .. cmd:: Infix @string := @term1_extended {? ( {+, @syntax_modifier } ) } {? : @ident }
+       .. cmd:: Infix @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @ident }
 
           This command is equivalent to :n:`…`.
 
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index c5e0007e78..5762967c36 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -3,8 +3,8 @@
 =============================
 
 ..
-   README.rst is auto-generated from README.template.rst and the coqrst docs;
-   use ``doc/tools/coqrst/regen_readme.py`` to rebuild it.
+   README.rst is auto-generated from README.template.rst and the coqrst/*.py files
+   (in particular coqdomain.py).  Use ``doc/tools/coqrst/regen_readme.py`` to rebuild it.
 
 Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_.
 
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 94ab6e789c..315c9d4a80 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -713,48 +713,119 @@ 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
+combined to create custom rewriting procedures. Its set of strategies is based
 on the programmable rewriting strategies with generic traversals by Visser et al.
 :cite:`Luttik97specificationof` :cite:`Visser98`, which formed the core of
 the Stratego transformation language :cite:`Visser01`. Rewriting 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:: 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 `red_expr`             (apply reduction)
-            : fold `term`               (unify)
-            : ( `strategy` )
-
-Actually a few of these are defined in term of the others using a
+are applied using the tactic :n:`rewrite_strat @rewstrategy`.
+
+.. insertprodn rewstrategy rewstrategy
+
+.. prodn::
+   rewstrategy ::= @one_term
+   | <- @one_term
+   | fail
+   | id
+   | refl
+   | progress @rewstrategy
+   | try @rewstrategy
+   | @rewstrategy ; @rewstrategy
+   | choice @rewstrategy @rewstrategy
+   | repeat @rewstrategy
+   | any @rewstrategy
+   | subterm @rewstrategy
+   | subterms @rewstrategy
+   | innermost @rewstrategy
+   | outermost @rewstrategy
+   | bottomup @rewstrategy
+   | topdown @rewstrategy
+   | hints @ident
+   | terms {* @one_term }
+   | eval @red_expr
+   | fold @one_term
+   | ( @rewstrategy )
+   | old_hints @ident
+
+:n:`@one_term`
+   lemma, left to right
+
+:n:`<- @one_term`
+   lemma, right to left
+
+:n:`fail`
+   failure
+
+:n:`id`
+  identity
+
+:n:`refl`
+   reflexivity
+
+:n:`progress @rewstrategy`
+   progress
+
+:n:`try @rewstrategy`
+   try catch
+
+:n:`@rewstrategy ; @rewstrategy`
+   composition
+
+:n:`choice @rewstrategy @rewstrategy`
+   left_biased_choice
+
+:n:`repeat @rewstrategy`
+   one or more
+
+:n:`any @rewstrategy`
+   zero or more
+
+:n:`subterm @rewstrategy`
+   one subterm
+
+:n:`subterms @rewstrategy`
+   all subterms
+
+:n:`innermost @rewstrategy`
+   innermost first
+
+:n:`outermost @rewstrategy`
+   outermost first
+
+:n:`bottomup @rewstrategy`
+   bottom-up
+
+:n:`topdown @rewstrategy`
+   top-down
+
+:n:`hints @ident`
+   apply hints from hint database
+
+:n:`terms {* @one_term }`
+   any of the terms
+
+:n:`eval @red_expr`
+   apply reduction
+
+:n:`fold @term`
+   unify
+
+:n:`( @rewstrategy )`
+   to be documented
+
+:n:`old_hints @ident`
+   to be documented
+
+
+A few of these are defined in terms of the others using a
 primitive fixpoint operator:
 
-- :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))`
+- :n:`try @rewstrategy := choice @rewstrategy id`
+- :n:`any @rewstrategy := fix @ident. try (@rewstrategy ; @ident)`
+- :n:`repeat @rewstrategy := @rewstrategy; any @rewstrategy`
+- :n:`bottomup @rewstrategy := fix @ident. (choice (progress (subterms @ident)) @rewstrategy) ; try @ident`
+- :n:`topdown @rewstrategy := fix @ident. (choice @rewstrategy (progress (subterms @ident))) ; try @ident`
+- :n:`innermost @rewstrategy := fix @ident. (choice (subterm @ident) @rewstrategy)`
+- :n:`outermost @rewstrategy := fix @ident. (choice @rewstrategy (subterm @ident))`
 
 The basic control strategy semantics are straightforward: strategies
 are applied to subterms of the term to rewrite, starting from the root
@@ -764,18 +835,18 @@ hand-side. Composition can be used to continue rewriting on the
 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 :token:`strategy` and fails if no
+``progress`` tests progress of the argument :n:`@rewstrategy` 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
 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 :token:`strategy` to
+The ``subterm`` and ``subterms`` strategies apply their argument :n:`@rewstrategy` to
 respectively one or all subterms of the current term under
 consideration, left-to-right. ``subterm`` stops at the first subterm for
-which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost``
+which :n:`@rewstrategy` made progress. The composite strategies ``innermost`` and ``outermost``
 perform a single innermost or outermost rewrite using their argument
-:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many
+:n:`@rewstrategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many
 rewritings as possible, starting from the bottom or the top of the
 term.
 
@@ -793,7 +864,7 @@ Usage
 ~~~~~
 
 
-.. tacn:: rewrite_strat @strategy {? in @ident }
+.. tacn:: rewrite_strat @rewstrategy {? in @ident }
    :name: rewrite_strat
 
    Rewrite using the strategy s in hypothesis ident or the conclusion.
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index b007509b2e..1f33775a01 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -37,12 +37,13 @@ In addition to these user-defined classes, we have two built-in classes:
   * ``Funclass``, the class of functions; its objects are all the terms with a functional
     type, i.e. of form :g:`forall x:A,B`.
 
-Formally, the syntax of classes is defined as:
+   .. insertprodn class class
+
+   .. prodn::
+      class ::= Funclass
+      | Sortclass
+      | @smart_qualid
 
-.. productionlist::
-   class: `qualid`
-        : Sortclass
-        : Funclass
 
 
 Coercions
@@ -186,37 +187,12 @@ Declaring Coercions
      This defines :token:`ident` just like :n:`Let @ident := @term  {? @type }`,
      and then declares :token:`ident` as a coercion between it source and its target.
 
-Assumptions can be declared as coercions at declaration time.
-This extends the grammar of assumptions from
-Figure :ref:`vernacular` as follows:
-
-..
-  FIXME:
-   \comindex{Variable \mbox{\rm (and coercions)}}
-   \comindex{Axiom \mbox{\rm (and coercions)}}
-   \comindex{Parameter \mbox{\rm (and coercions)}}
-   \comindex{Hypothesis \mbox{\rm (and coercions)}}
-
-.. productionlist::
-   assumption : `assumption_token` `assums` .
-   assums : `simple_assums`
-          : (`simple_assums`) ... (`simple_assums`)
-   simple_assums : `ident` ... `ident` :[>] `term`
-
-If the extra ``>`` is present before the type of some assumptions, these
-assumptions are declared as coercions.
-
-Similarly, constructors of inductive types can be declared as coercions at
-definition time of the inductive type. This extends and modifies the
-grammar of inductive types from Figure :ref:`vernacular` as follows:
-
-..
-  FIXME:
-   \comindex{Inductive \mbox{\rm (and coercions)}}
-   \comindex{CoInductive \mbox{\rm (and coercions)}}
-
-Especially, if the extra ``>`` is present in a constructor
-declaration, this constructor is declared as a coercion.
+Some objects can be declared as coercions when they are defined.
+This applies to :ref:`assumptions<gallina-assumptions>` and
+constructors of :ref:`inductive types and record fields<gallina-inductive-definitions>`.
+Use :n:`:>` instead of :n:`:` before the
+:n:`@type` of the assumption to do so.  See :n:`@of_type`.
+
 
 .. cmd:: Identity Coercion @ident : @class >-> @class
 
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 1098aa75da..76174e32b5 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -300,70 +300,79 @@ following property:
 
 The syntax for adding a new ring is 
 
-.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}
-
-   The :token:`ident` is not relevant. It is used just for error messages. The
-   :token:`term` is a proof that the ring signature satisfies the (semi-)ring
+.. cmd:: Add Ring @ident : @one_term {? ( {+, @ring_mod } ) }
+
+   .. insertprodn ring_mod ring_mod
+
+   .. prodn::
+      ring_mod ::= decidable @one_term
+      | abstract
+      | morphism @one_term
+      | constants [ @ltac_expr ]
+      | preprocess [ @ltac_expr ]
+      | postprocess [ @ltac_expr ]
+      | setoid @one_term @one_term
+      | sign @one_term
+      | power @one_term [ {+ @qualid } ]
+      | power_tac @one_term [ @ltac_expr ]
+      | div @one_term
+      | closed [ {+ @qualid } ]
+
+   The :n:`@ident` is used only for error messages. The
+   :n:`@one_term` is a proof that the ring signature satisfies the (semi-)ring
    axioms. The optional list of modifiers is used to tailor the behavior
-   of the tactic. The following list describes their syntax and effects:
-
-   .. productionlist:: coq
-      ring_mod : abstract | decidable `term` | morphism `term`
-               : setoid `term` `term`
-               : constants [ `tactic` ]
-               : preprocess [ `tactic` ]
-               : postprocess [ `tactic` ]
-               : power_tac `term` [ `tactic` ]
-               : sign `term`
-               : div `term`
-
-   abstract
+   of the tactic. Here are their effects:
+
+   :n:`abstract`
       declares the ring as abstract. This is the default.
 
-   decidable :n:`@term`
+   :n:`decidable @one_term`
       declares the ring as computational. The expression
-      :n:`@term` is the correctness proof of an equality test ``?=!``
+      :n:`@one_term` is the correctness proof of an equality test ``?=!``
       (which should be evaluable). Its type should be of the form
       ``forall x y, x ?=! y = true → x == y``.
 
-   morphism :n:`@term`
+   :n:`morphism @one_term`
       declares the ring as a customized one. The expression
-      :n:`@term` is a proof that there exists a morphism between a set of
+      :n:`@one_term` is a proof that there exists a morphism between a set of
       coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and
       ``Ring_theory.semi_morph``).
 
-   setoid :n:`@term` :n:`@term`
+   :n:`setoid @one_term @one_term`
       forces the use of given setoid. The first
-      :n:`@term` is a proof that the equality is indeed a setoid (see
-      ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the
+      :n:`@one_term` is a proof that the equality is indeed a setoid (see
+      ``Setoid.Setoid_Theory``), and the second a proof that the
       ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and
       ``Ring_theory.sring_eq_ext``).
       This modifier needs not be used if the setoid and morphisms have been
       declared.
 
-   constants [ :n:`@tactic` ]
-      specifies a tactic expression :n:`@tactic` that, given a
+   :n:`constants [ @ltac_expr ]`
+      specifies a tactic expression :n:`@ltac_expr` 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:`@tactic` ]
-      specifies a tactic :n:`@tactic` that is applied as a
+   :n:`preprocess [ @ltac_expr ]`
+      specifies a tactic :n:`@ltac_expr` 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:`@tactic` ]
-      specifies a tactic :n:`@tactic` that is applied as a final
+   :n:`postprocess [ @ltac_expr ]`
+      specifies a tactic :n:`@ltac_expr` 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:`@tactic` ]
+   :n:`power @one_term [ {+ @qualid } ]`
+      to be documented
+
+   :n:`power_tac @one_term @ltac_expr ]`
       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
+      :math:`x^2` ). The term :n:`@one_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:`@tactic` specifies a tactic expression
       that, given a term, “abstracts” it into an object of type |N| whose
@@ -374,22 +383,25 @@ The syntax for adding a new ring is
       and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic
       does not recognize power expressions as ring expressions.
 
-   sign :n:`@term`
+   :n:`sign @one_term`
       allows :tacn:`ring_simplify` to use a minus operation when
       outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The
       term :token:`term` is a proof that a given sign function indicates expressions
       that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See
       ``plugins/setoid_ring/InitialRing.v`` for examples of sign function.
 
-   div :n:`@term`
+   :n:`div @one_term`
       allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with
-      coefficients other than 1 in the rewriting. The term :n:`@term` is a proof
+      coefficients other than 1 in the rewriting. The term :n:`@one_term` is a proof
       that a given division function satisfies the specification of an
-      euclidean division function (:n:`@term` has to be a proof of
+      euclidean division function (:n:`@one_term` has to be a proof of
       ``Ring_theory.div_theory``). For example, this function is called when
       trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See
       ``plugins/setoid_ring/InitialRing.v`` for examples of div function.
 
+   :n:`closed [ {+ @qualid } ]`
+      to be documented
+
 Error messages:
 
 .. exn:: Bad ring structure.
@@ -653,24 +665,27 @@ zero for the correctness of the algorithm.
 
 The syntax for adding a new field is 
 
-.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}
+.. cmd:: Add Field @ident : @one_term {? ( {+, @field_mod } ) }
 
-   The :n:`@ident` is not relevant. It is used just for error
-   messages. :n:`@term` is a proof that the field signature satisfies the
+   .. insertprodn field_mod field_mod
+
+   .. prodn::
+      field_mod ::= @ring_mod
+      | completeness @one_term
+
+   The :n:`@ident` is used only for error
+   messages. :n:`@one_term` is a proof that the field signature satisfies the
    (semi-)field axioms. The optional list of modifiers is used to tailor
    the behavior of the tactic.
 
-   .. productionlist:: coq
-      field_mod : `ring_mod` | completeness `term`
-
    Since field tactics are built upon ``ring``
-   tactics, all modifiers of the ``Add Ring`` apply. There is only one
+   tactics, all modifiers of :cmd:`Add Ring` apply. There is only one
    specific modifier:
 
-   completeness :n:`@term`
+   completeness :n:`@one_term`
       allows the field tactic to prove automatically
       that the image of nonzero coefficients are mapped to nonzero
-      elements of the field. :n:`@term` is a proof of
+      elements of the field. :n:`@one_term` is a proof of
       :g:`forall x y, [x] == [y] ->  x ?=! y = true`,
       which is the completeness of equality on coefficients
       w.r.t. the field equality.
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index c069782add..0e326f45d2 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -372,16 +372,11 @@ to universes and explicitly instantiate polymorphic definitions.
    universe quantification will be discharged on each section definition
    independently.
 
-.. cmd:: Constraint @universe_constraint
-         Polymorphic Constraint @universe_constraint
+.. cmd:: Constraint @univ_constraint
+         Polymorphic Constraint @univ_constraint
 
    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
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 22102aa3ab..d864f8549d 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,9 +183,9 @@ todo_include_todos = False
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
+    'assums',
     'binders',
     'collection',
-    'command',
     'definition',
     'dirpath',
     'inductive',
@@ -194,7 +194,6 @@ nitpick_ignore = [ ('token', token) for token in [
     'module',
     'simple_tactic',
     'symbol',
-    'tactic',
     'term_pattern',
     'term_pattern_string',
     'toplevel_selector',
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index e12ff1ba98..4f0cf5f815 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -158,6 +158,8 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
    | @term1
    arg ::= ( @ident := @term )
    | @term1
+   one_term ::= @term1
+   | @ @qualid {? @univ_annot }
    term1 ::= @term_projection
    | @term0 % @ident
    | @term0
@@ -175,6 +177,13 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
    | ltac : ( @ltac_expr )
    field_def ::= @qualid {* @binder } := @term
 
+.. note::
+
+   Many commands and tactics use :n:`@one_term` rather than :n:`@term`.
+   The former need to be enclosed in parentheses unless they're very
+   simple, such as a single identifier.  This avoids confusing a space-separated
+   list of terms with a :n:`@term1` applied to a list of arguments.
+
 .. _types:
 
 Types
@@ -591,17 +600,15 @@ Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`).
 Recursive and co-recursive functions: fix and cofix
 ---------------------------------------------------
 
-.. insertprodn term_fix term1_extended
+.. insertprodn term_fix fixannot
 
 .. prodn::
    term_fix ::= let fix @fix_body in @term
    | fix @fix_body {? {+ with @fix_body } for @ident }
    fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term
    fixannot ::= %{ struct @ident %}
-   | %{ wf @term1_extended @ident %}
-   | %{ measure @term1_extended {? @ident } {? @term1_extended } %}
-   term1_extended ::= @term1
-   | @ @qualid {? @univ_annot }
+   | %{ wf @one_term @ident %}
+   | %{ measure @one_term {? @ident } {? @one_term } %}
 
 
 The expression ":n:`fix @ident__1 @binder__1 : @type__1 := @term__1 with … with @ident__n @binder__n : @type__n := @term__n for @ident__i`" denotes the
@@ -1472,11 +1479,11 @@ Computations
    | vm_compute {? @ref_or_pattern_occ }
    | native_compute {? @ref_or_pattern_occ }
    | unfold {+, @unfold_occ }
-   | fold {+ @term1_extended }
+   | fold {+ @one_term }
    | pattern {+, @pattern_occ }
    | @ident
-   delta_flag ::= {? - } [ {+ @smart_global } ]
-   smart_global ::= @qualid
+   delta_flag ::= {? - } [ {+ @smart_qualid } ]
+   smart_qualid ::= @qualid
    | @by_notation
    by_notation ::= @string {? % @ident }
    strategy_flag ::= {+ @red_flags }
@@ -1488,16 +1495,16 @@ Computations
    | cofix
    | zeta
    | delta {? @delta_flag }
-   ref_or_pattern_occ ::= @smart_global {? at @occs_nums }
-   | @term1_extended {? at @occs_nums }
+   ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums }
+   | @one_term {? at @occs_nums }
    occs_nums ::= {+ @num_or_var }
    | - @num_or_var {* @int_or_var }
    num_or_var ::= @num
    | @ident
    int_or_var ::= @int
    | @ident
-   unfold_occ ::= @smart_global {? at @occs_nums }
-   pattern_occ ::= @term1_extended {? at @occs_nums }
+   unfold_occ ::= @smart_qualid {? at @occs_nums }
+   pattern_occ ::= @one_term {? at @occs_nums }
 
 See :ref:`Conversion-rules`.
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2bfd810ea1..4f2f74aae4 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -72,7 +72,7 @@ specified, the default selector is used.
 .. _bindingslist:
 
 Bindings list
-~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~
 
 Tactics that take a term as an argument may also support a bindings list
 to instantiate some parameters of the term by name or position.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index fd95a5cef4..669975ba7e 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -947,7 +947,7 @@ notations are given below. The optional :production:`scope` is described in
 
 .. prodn::
    decl_notations ::= where @decl_notation {* and @decl_notation }
-   decl_notation ::= @string := @term1_extended [(only parsing)] {? : @ident }
+   decl_notation ::= @string := @one_term {? ( only parsing ) } {? : @ident }
 
 .. note:: No typing of the denoted expression is performed at definition
           time. Type checking is done only at the time of use of the notation.
@@ -1194,7 +1194,7 @@ Binding arguments of a constant to an interpretation scope
 Binding types of arguments to an interpretation scope
 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 
-.. cmd:: Bind Scope @scope with @qualid
+.. cmd:: Bind Scope @ident with {+ @class }
 
    When an interpretation scope is naturally associated to a type (e.g.  the
    scope of operations on the natural numbers), it may be convenient to bind it