Remove some productionlists

15 files changed, 527 insertions, 464 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
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index d6ecf311f1..4d5c837e5c 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -294,7 +294,7 @@ class VernacObject(NotationObject):
 
     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/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 3524d77380..7a165988a6 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -57,14 +57,15 @@ DELETE: [
 | check_for_coloneq
 | local_test_lpar_id_colon
 | lookup_at_as_comma
-| only_starredidentrefs
+| test_only_starredidentrefs
 | test_bracket_ident
 | test_lpar_id_colon
 | test_lpar_id_coloneq  (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *)
 | test_lpar_id_rpar
 | test_lpar_idnum_coloneq
-| test_nospace_pipe_closedcurly
 | test_show_goal
+| test_name_colon
+| test_pipe_closedcurly
 | ensure_fixannot
 
   (* SSR *)
@@ -332,8 +333,8 @@ typeclass_constraint: [
 | EDIT ADD_OPT "!" operconstr200
 | REPLACE "{" name "}" ":" [ "!" | ] operconstr200
 | WITH "{" name "}" ":" OPT "!"  operconstr200
-| REPLACE name_colon [ "!" | ] operconstr200
-| WITH name_colon OPT "!" operconstr200
+| REPLACE name ":" [ "!" | ] operconstr200
+| WITH name ":" OPT "!" operconstr200
 ]
 
 (* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*)
@@ -409,19 +410,6 @@ DELETE: [
 | cumulativity_token
 ]
 
-opt_coercion: [
-| OPTINREF
-]
-
-opt_constructors_or_fields: [
-| OPTINREF
-]
-
-SPLICE: [
-| opt_coercion
-| opt_constructors_or_fields
-]
-
 constructor_list_or_record_decl: [
 | OPTINREF
 ]
@@ -433,11 +421,6 @@ record_fields: [
 | DELETE (* empty *)
 ]
 
-decl_notation: [
-| REPLACE "where" LIST1 one_decl_notation SEP decl_sep
-| WITH "where" one_decl_notation LIST0 ( decl_sep one_decl_notation )
-]
-
 assumptions_token: [
 | DELETENT
 ]
@@ -767,13 +750,13 @@ vernacular: [
 ]
 
 rec_definition: [
-| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
-| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
+| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
+| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
 
 corec_definition: [
-| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
-| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
+| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
+| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
 
 type_cstr: [
@@ -782,13 +765,9 @@ type_cstr: [
 | OPTINREF
 ]
 
-decl_notation: [
-| OPTINREF
-]
-
 inductive_definition: [
-| REPLACE OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation
-| WITH OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation
+| REPLACE opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
+| WITH opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations
 ]
 
 constructor_list_or_record_decl: [
@@ -807,6 +786,31 @@ record_binder: [
 | DELETE name
 ]
 
+in_clause: [
+| DELETE in_clause'
+| REPLACE LIST0 hypident_occ SEP "," "|-" concl_occ
+| WITH LIST0 hypident_occ SEP "," OPT ( "|-" concl_occ )
+| DELETE LIST0 hypident_occ SEP ","
+]
+
+concl_occ: [
+| OPTINREF
+]
+
+opt_coercion: [
+| OPTINREF
+]
+
+opt_constructors_or_fields: [
+| OPTINREF
+]
+
+decl_notations: [
+| REPLACE "where" LIST1 decl_notation SEP decl_sep
+| WITH "where" decl_notation LIST0 (decl_sep decl_notation )
+| OPTINREF
+]
+
 SPLICE: [
 | noedit_mode
 | command_entry
@@ -941,11 +945,12 @@ SPLICE: [
 | record_fields
 | constructor_type
 | record_binder
+| opt_coercion
+| opt_constructors_or_fields
 ] (* end SPLICE *)
 
 RENAME: [
 | clause clause_dft_concl
-| in_clause' in_clause
 
 | tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
 | tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
@@ -980,7 +985,7 @@ RENAME: [
 | nat_or_var num_or_var
 | fix_decl fix_body
 | cofix_decl cofix_body
-| constr term1_extended
+| constr one_term
 | appl_arg arg
 | rec_definition fix_definition
 | corec_definition cofix_definition
@@ -988,12 +993,12 @@ RENAME: [
 | univ_instance univ_annot
 | simple_assum_coe assumpt
 | of_type_with_opt_coercion of_type
-| decl_notation decl_notations
-| one_decl_notation decl_notation
 | attribute attr
 | attribute_value attr_value
 | constructor_list_or_record_decl constructors_or_record
 | record_binder_body field_body
+| class_rawexpr class
+| smart_global smart_qualid
 ]
 
 
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 5fcb56f5f2..366b70a1f7 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -1717,7 +1717,7 @@ let process_rst g file args seen tac_prods cmd_prods =
             else begin
               let line3 = getline() in
               if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "prodn::" then
-                error "%s line %d: expecting 'prodn' after 'insertprodn'\n" file !linenum
+                error "%s line %d: expecting '.. prodn::' after 'insertprodn'\n" file !linenum
               else begin
                 let indent = Str.matched_group 1 line3 in
                 let rec skip_to_end () =
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 529d81e424..6897437457 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -152,7 +152,7 @@ binder_constr: [
 ]
 
 appl_arg: [
-| lpar_id_coloneq lconstr ")"
+| test_lpar_id_coloneq "(" ident ":=" lconstr ")"
 | operconstr9
 ]
 
@@ -335,7 +335,7 @@ closed_binder: [
 typeclass_constraint: [
 | "!" operconstr200
 | "{" name "}" ":" [ "!" | ] operconstr200
-| name_colon [ "!" | ] operconstr200
+| test_name_colon name ":" [ "!" | ] operconstr200
 | operconstr200
 ]
 
@@ -449,7 +449,7 @@ bigint: [
 ]
 
 bar_cbrace: [
-| test_nospace_pipe_closedcurly "|" "}"
+| test_pipe_closedcurly "|" "}"
 ]
 
 vernac_toplevel: [
@@ -511,8 +511,8 @@ command: [
 | "Load" [ "Verbose" | ] [ ne_string | IDENT ]
 | "Declare" "ML" "Module" LIST1 ne_string
 | "Locate" locatable
-| "Add" "LoadPath" ne_string as_dirpath
-| "Add" "Rec" "LoadPath" ne_string as_dirpath
+| "Add" "LoadPath" ne_string "as" dirpath
+| "Add" "Rec" "LoadPath" ne_string "as" dirpath
 | "Remove" "LoadPath" ne_string
 | "Type" lconstr
 | "Print" printable
@@ -522,7 +522,6 @@ command: [
 | "Print" "Namespace" dirpath
 | "Inspect" natural
 | "Add" "ML" "Path" ne_string
-| "Add" "Rec" "ML" "Path" ne_string
 | "Set" option_table option_setting
 | "Unset" option_table
 | "Print" "Table" option_table
@@ -655,6 +654,7 @@ command: [
 | "Add" "CstOp" constr      (* micromega plugin *)
 | "Add" "BinRel" constr      (* micromega plugin *)
 | "Add" "PropOp" constr      (* micromega plugin *)
+| "Add" "PropBinOp" constr      (* micromega plugin *)
 | "Add" "PropUOp" constr      (* micromega plugin *)
 | "Add" "Spec" constr      (* micromega plugin *)
 | "Add" "BinOpSpec" constr      (* micromega plugin *)
@@ -924,16 +924,16 @@ reduce: [
 |
 ]
 
-one_decl_notation: [
-| ne_lstring ":=" constr OPT [ ":" IDENT ]
+decl_notation: [
+| ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ]
 ]
 
 decl_sep: [
 | "and"
 ]
 
-decl_notation: [
-| "where" LIST1 one_decl_notation SEP decl_sep
+decl_notations: [
+| "where" LIST1 decl_notation SEP decl_sep
 |
 ]
 
@@ -943,7 +943,7 @@ opt_constructors_or_fields: [
 ]
 
 inductive_definition: [
-| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation
+| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
 ]
 
 constructor_list_or_record_decl: [
@@ -961,11 +961,11 @@ opt_coercion: [
 ]
 
 rec_definition: [
-| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
+| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
 
 corec_definition: [
-| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
+| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
 
 scheme: [
@@ -982,7 +982,7 @@ scheme_kind: [
 ]
 
 record_field: [
-| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notation
+| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notations
 ]
 
 record_fields: [
@@ -1148,7 +1148,7 @@ module_type: [
 ]
 
 section_subset_expr: [
-| only_starredidentrefs LIST0 starredidentref
+| test_only_starredidentrefs LIST0 starredidentref
 | ssexpr35
 ]
 
@@ -1172,8 +1172,8 @@ ssexpr50: [
 
 ssexpr0: [
 | starredidentref
-| "(" only_starredidentrefs LIST0 starredidentref ")"
-| "(" only_starredidentrefs LIST0 starredidentref ")" "*"
+| "(" test_only_starredidentrefs LIST0 starredidentref ")"
+| "(" test_only_starredidentrefs LIST0 starredidentref ")" "*"
 | "(" ssexpr35 ")"
 | "(" ssexpr35 ")" "*"
 ]
@@ -1331,10 +1331,6 @@ option_table: [
 | LIST1 IDENT
 ]
 
-as_dirpath: [
-| OPT [ "as" dirpath ]
-]
-
 ne_in_or_out_modules: [
 | "inside" LIST1 global
 | "outside" LIST1 global
@@ -1684,6 +1680,8 @@ simple_tactic: [
 | "eenough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
 | "assert" constr as_ipat by_tactic
 | "eassert" constr as_ipat by_tactic
+| "pose" "proof" test_lpar_id_coloneq "(" identref ":=" lconstr ")"
+| "epose" "proof" test_lpar_id_coloneq "(" identref ":=" lconstr ")"
 | "pose" "proof" lconstr as_ipat
 | "epose" "proof" lconstr as_ipat
 | "enough" constr as_ipat by_tactic
@@ -1740,10 +1738,11 @@ simple_tactic: [
 | "psatz_R" tactic      (* micromega plugin *)
 | "psatz_Q" int_or_var tactic      (* micromega plugin *)
 | "psatz_Q" tactic      (* micromega plugin *)
-| "zify_iter_specs" tactic      (* micromega plugin *)
+| "zify_iter_specs"      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
 | "zify_saturate"      (* micromega plugin *)
 | "zify_iter_let" tactic      (* micromega plugin *)
+| "zify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
 | "rtauto"
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 908e3ccd51..f26a174722 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -58,6 +58,11 @@ arg: [
 | term1
 ]
 
+one_term: [
+| term1
+| "@" qualid OPT univ_annot
+]
+
 term1: [
 | term_projection
 | term0 "%" ident
@@ -238,13 +243,8 @@ fix_body: [
 
 fixannot: [
 | "{" "struct" ident "}"
-| "{" "wf" term1_extended ident "}"
-| "{" "measure" term1_extended OPT ident OPT term1_extended "}"
-]
-
-term1_extended: [
-| term1
-| "@" qualid OPT univ_annot
+| "{" "wf" one_term ident "}"
+| "{" "measure" one_term OPT ident OPT one_term "}"
 ]
 
 term_cofix: [
@@ -400,7 +400,7 @@ decl_notations: [
 ]
 
 decl_notation: [
-| string ":=" term1_extended OPT [ ":" ident ]
+| string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" ident ]
 ]
 
 register_token: [
@@ -484,16 +484,16 @@ red_expr: [
 | "vm_compute" OPT ref_or_pattern_occ
 | "native_compute" OPT ref_or_pattern_occ
 | "unfold" LIST1 unfold_occ SEP ","
-| "fold" LIST1 term1_extended
+| "fold" LIST1 one_term
 | "pattern" LIST1 pattern_occ SEP ","
 | ident
 ]
 
 delta_flag: [
-| OPT "-" "[" LIST1 smart_global "]"
+| OPT "-" "[" LIST1 smart_qualid "]"
 ]
 
-smart_global: [
+smart_qualid: [
 | qualid
 | by_notation
 ]
@@ -518,8 +518,8 @@ red_flags: [
 ]
 
 ref_or_pattern_occ: [
-| smart_global OPT ( "at" occs_nums )
-| term1_extended OPT ( "at" occs_nums )
+| smart_qualid OPT ( "at" occs_nums )
+| one_term OPT ( "at" occs_nums )
 ]
 
 occs_nums: [
@@ -538,11 +538,11 @@ int_or_var: [
 ]
 
 unfold_occ: [
-| smart_global OPT ( "at" occs_nums )
+| smart_qualid OPT ( "at" occs_nums )
 ]
 
 pattern_occ: [
-| term1_extended OPT ( "at" occs_nums )
+| one_term OPT ( "at" occs_nums )
 ]
 
 finite_token: [
@@ -587,11 +587,11 @@ scheme: [
 ]
 
 scheme_kind: [
-| "Induction" "for" smart_global "Sort" sort_family
-| "Minimality" "for" smart_global "Sort" sort_family
-| "Elimination" "for" smart_global "Sort" sort_family
-| "Case" "for" smart_global "Sort" sort_family
-| "Equality" "for" smart_global
+| "Induction" "for" smart_qualid "Sort" sort_family
+| "Minimality" "for" smart_qualid "Sort" sort_family
+| "Elimination" "for" smart_qualid "Sort" sort_family
+| "Case" "for" smart_qualid "Sort" sort_family
+| "Equality" "for" smart_qualid
 ]
 
 sort_family: [
@@ -615,21 +615,21 @@ gallina_ext: [
 | "Export" LIST1 qualid
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
 | "Include" "Type" module_type_inl LIST0 ( "<+" module_type_inl )
-| "Transparent" LIST1 smart_global
-| "Opaque" LIST1 smart_global
-| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ]
+| "Transparent" LIST1 smart_qualid
+| "Opaque" LIST1 smart_qualid
+| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ]
 | "Canonical" OPT "Structure" qualid OPT [ OPT univ_decl def_body ]
 | "Canonical" OPT "Structure" by_notation
 | "Coercion" qualid OPT univ_decl def_body
-| "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr
-| "Coercion" qualid ":" class_rawexpr ">->" class_rawexpr
-| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
+| "Identity" "Coercion" ident ":" class ">->" class
+| "Coercion" qualid ":" class ">->" class
+| "Coercion" by_notation ":" class ">->" class
 | "Context" LIST1 binder
 | "Instance" instance_name ":" term hint_info [ ":=" "{" [ LIST1 field_def SEP ";" | ] "}" | ":=" term | ]
 | "Existing" "Instance" qualid hint_info
 | "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
 | "Existing" "Class" qualid
-| "Arguments" smart_global LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
 | "Implicit" "Type" reserv_list
 | "Implicit" "Types" reserv_list
 | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 ident ]
@@ -643,14 +643,8 @@ option_setting: [
 | string
 ]
 
-class_rawexpr: [
-| "Funclass"
-| "Sortclass"
-| smart_global
-]
-
 hint_info: [
-| "|" OPT num OPT term1_extended
+| "|" OPT num OPT one_term
 |
 ]
 
@@ -780,11 +774,11 @@ command: [
 | "Load" [ "Verbose" | ] [ string | ident ]
 | "Declare" "ML" "Module" LIST1 string
 | "Locate" locatable
-| "Add" "LoadPath" string as_dirpath
-| "Add" "Rec" "LoadPath" string as_dirpath
+| "Add" "LoadPath" string "as" dirpath
+| "Add" "Rec" "LoadPath" string "as" dirpath
 | "Remove" "LoadPath" string
 | "Type" term
-| "Print" "Term" smart_global OPT ( "@{" LIST0 name "}" )
+| "Print" "Term" smart_qualid OPT ( "@{" LIST0 name "}" )
 | "Print" "All"
 | "Print" "Section" qualid
 | "Print" "Grammar" ident
@@ -798,36 +792,35 @@ command: [
 | "Print" "Graph"
 | "Print" "Classes"
 | "Print" "TypeClasses"
-| "Print" "Instances" smart_global
+| "Print" "Instances" smart_qualid
 | "Print" "Coercions"
-| "Print" "Coercion" "Paths" class_rawexpr class_rawexpr
-| "Print" "Canonical" "Projections" LIST0 smart_global
+| "Print" "Coercion" "Paths" class class
+| "Print" "Canonical" "Projections" LIST0 smart_qualid
 | "Print" "Typing" "Flags"
 | "Print" "Tables"
 | "Print" "Options"
 | "Print" "Hint"
-| "Print" "Hint" smart_global
+| "Print" "Hint" smart_qualid
 | "Print" "Hint" "*"
 | "Print" "HintDb" ident
 | "Print" "Scopes"
 | "Print" "Scope" ident
 | "Print" "Visibility" OPT ident
-| "Print" "Implicit" smart_global
+| "Print" "Implicit" smart_qualid
 | "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
-| "Print" "Assumptions" smart_global
-| "Print" "Opaque" "Dependencies" smart_global
-| "Print" "Transparent" "Dependencies" smart_global
-| "Print" "All" "Dependencies" smart_global
-| "Print" "Strategy" smart_global
+| "Print" "Assumptions" smart_qualid
+| "Print" "Opaque" "Dependencies" smart_qualid
+| "Print" "Transparent" "Dependencies" smart_qualid
+| "Print" "All" "Dependencies" smart_qualid
+| "Print" "Strategy" smart_qualid
 | "Print" "Strategies"
 | "Print" "Registered"
-| "Print" smart_global OPT ( "@{" LIST0 name "}" )
+| "Print" smart_qualid OPT ( "@{" LIST0 name "}" )
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
 | "Print" "Namespace" dirpath
 | "Inspect" num
 | "Add" "ML" "Path" string
-| "Add" "Rec" "ML" "Path" string
 | "Set" LIST1 ident option_setting
 | "Unset" LIST1 ident
 | "Print" "Table" LIST1 ident
@@ -849,7 +842,7 @@ command: [
 | "Debug" "Off"
 | "Declare" "Reduction" ident ":=" red_expr
 | "Declare" "Custom" "Entry" ident
-| "Derive" ident "SuchThat" term1_extended "As" ident      (* derive plugin *)
+| "Derive" ident "SuchThat" one_term "As" ident      (* derive plugin *)
 | "Proof"
 | "Proof" "Mode" string
 | "Proof" term
@@ -907,31 +900,31 @@ command: [
 | "Obligations"
 | "Preterm" "of" ident
 | "Preterm"
-| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
-| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
-| "Add" "Relation" term1_extended term1_extended "as" ident
-| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
-| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Relation" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Setoid" term1_extended term1_extended term1_extended "as" ident
-| "Add" "Parametric" "Setoid" LIST0 binder ":" term1_extended term1_extended term1_extended "as" ident
-| "Add" "Morphism" term1_extended ":" ident
-| "Declare" "Morphism" term1_extended ":" ident
-| "Add" "Morphism" term1_extended "with" "signature" term "as" ident
-| "Add" "Parametric" "Morphism" LIST0 binder ":" term1_extended "with" "signature" term "as" ident
+| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident
+| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "as" ident
+| "Add" "Relation" one_term one_term "as" ident
+| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "as" ident
+| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
+| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
+| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
+| "Add" "Relation" one_term one_term "transitivity" "proved" "by" one_term "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "transitivity" "proved" "by" one_term "as" ident
+| "Add" "Setoid" one_term one_term one_term "as" ident
+| "Add" "Parametric" "Setoid" LIST0 binder ":" one_term one_term one_term "as" ident
+| "Add" "Morphism" one_term ":" ident
+| "Declare" "Morphism" one_term ":" ident
+| "Add" "Morphism" one_term "with" "signature" term "as" ident
+| "Add" "Parametric" "Morphism" LIST0 binder ":" one_term "with" "signature" term "as" ident
 | "Grab" "Existential" "Variables"
 | "Unshelve"
-| "Declare" "Equivalent" "Keys" term1_extended term1_extended
+| "Declare" "Equivalent" "Keys" one_term one_term
 | "Print" "Equivalent" "Keys"
 | "Optimize" "Proof"
 | "Optimize" "Heap"
@@ -940,24 +933,25 @@ command: [
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
 | "Show" "Lia" "Profile"      (* micromega plugin *)
-| "Add" "InjTyp" term1_extended      (* micromega plugin *)
-| "Add" "BinOp" term1_extended      (* micromega plugin *)
-| "Add" "UnOp" term1_extended      (* micromega plugin *)
-| "Add" "CstOp" term1_extended      (* micromega plugin *)
-| "Add" "BinRel" term1_extended      (* micromega plugin *)
-| "Add" "PropOp" term1_extended      (* micromega plugin *)
-| "Add" "PropUOp" term1_extended      (* micromega plugin *)
-| "Add" "Spec" term1_extended      (* micromega plugin *)
-| "Add" "BinOpSpec" term1_extended      (* micromega plugin *)
-| "Add" "UnOpSpec" term1_extended      (* micromega plugin *)
-| "Add" "Saturate" term1_extended      (* micromega plugin *)
+| "Add" "InjTyp" one_term      (* micromega plugin *)
+| "Add" "BinOp" one_term      (* micromega plugin *)
+| "Add" "UnOp" one_term      (* micromega plugin *)
+| "Add" "CstOp" one_term      (* micromega plugin *)
+| "Add" "BinRel" one_term      (* micromega plugin *)
+| "Add" "PropOp" one_term      (* micromega plugin *)
+| "Add" "PropBinOp" one_term      (* micromega plugin *)
+| "Add" "PropUOp" one_term      (* micromega plugin *)
+| "Add" "Spec" one_term      (* micromega plugin *)
+| "Add" "BinOpSpec" one_term      (* micromega plugin *)
+| "Add" "UnOpSpec" one_term      (* micromega plugin *)
+| "Add" "Saturate" one_term      (* micromega plugin *)
 | "Show" "Zify" "InjTyp"      (* micromega plugin *)
 | "Show" "Zify" "BinOp"      (* micromega plugin *)
 | "Show" "Zify" "UnOp"      (* micromega plugin *)
 | "Show" "Zify" "CstOp"      (* micromega plugin *)
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
 | "Show" "Zify" "Spec"      (* micromega plugin *)
-| "Add" "Ring" ident ":" term1_extended OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* setoid_ring plugin *)
+| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* setoid_ring plugin *)
 | "Hint" "Cut" "[" hints_path "]" opthints
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
@@ -996,20 +990,20 @@ command: [
 | "Show" "Extraction"      (* extraction plugin *)
 | "Functional" "Case" fun_scheme_arg      (* funind plugin *)
 | "Generate" "graph" "for" qualid      (* funind plugin *)
-| "Hint" "Rewrite" orient LIST1 term1_extended ":" LIST0 ident
-| "Hint" "Rewrite" orient LIST1 term1_extended "using" ltac_expr ":" LIST0 ident
-| "Hint" "Rewrite" orient LIST1 term1_extended
-| "Hint" "Rewrite" orient LIST1 term1_extended "using" ltac_expr
-| "Derive" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
-| "Derive" "Inversion_clear" ident "with" term1_extended
-| "Derive" "Inversion" ident "with" term1_extended "Sort" sort_family
-| "Derive" "Inversion" ident "with" term1_extended
-| "Derive" "Dependent" "Inversion" ident "with" term1_extended "Sort" sort_family
-| "Derive" "Dependent" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
-| "Declare" "Left" "Step" term1_extended
-| "Declare" "Right" "Step" term1_extended
+| "Hint" "Rewrite" orient LIST1 one_term ":" LIST0 ident
+| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr ":" LIST0 ident
+| "Hint" "Rewrite" orient LIST1 one_term
+| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr
+| "Derive" "Inversion_clear" ident "with" one_term "Sort" sort_family
+| "Derive" "Inversion_clear" ident "with" one_term
+| "Derive" "Inversion" ident "with" one_term "Sort" sort_family
+| "Derive" "Inversion" ident "with" one_term
+| "Derive" "Dependent" "Inversion" ident "with" one_term "Sort" sort_family
+| "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family
+| "Declare" "Left" "Step" one_term
+| "Declare" "Right" "Step" one_term
 | "Print" "Rings"      (* setoid_ring plugin *)
-| "Add" "Field" ident ":" term1_extended OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
+| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
 | "Print" "Fields"      (* setoid_ring plugin *)
 | "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption
 | "String" "Notation" qualid qualid qualid ":" ident
@@ -1059,8 +1053,8 @@ dirpath: [
 ]
 
 locatable: [
-| smart_global
-| "Term" smart_global
+| smart_qualid
+| "Term" smart_qualid
 | "File" string
 | "Library" qualid
 | "Module" qualid
@@ -1071,19 +1065,15 @@ option_ref_value: [
 | string
 ]
 
-as_dirpath: [
-| OPT [ "as" dirpath ]
-]
-
 comment: [
-| term1_extended
+| one_term
 | string
 | num
 ]
 
 reference_or_constr: [
 | qualid
-| term1_extended
+| one_term
 ]
 
 hint: [
@@ -1100,7 +1090,7 @@ hint: [
 | "Mode" qualid LIST1 [ "+" | "!" | "-" ]
 | "Unfold" LIST1 qualid
 | "Constructors" LIST1 qualid
-| "Extern" num OPT term1_extended "=>" ltac_expr
+| "Extern" num OPT one_term "=>" ltac_expr
 ]
 
 constr_body: [
@@ -1157,23 +1147,23 @@ fun_scheme_arg: [
 ]
 
 ring_mod: [
-| "decidable" term1_extended      (* setoid_ring plugin *)
+| "decidable" one_term      (* setoid_ring plugin *)
 | "abstract"      (* setoid_ring plugin *)
-| "morphism" term1_extended      (* setoid_ring plugin *)
+| "morphism" one_term      (* setoid_ring plugin *)
 | "constants" "[" ltac_expr "]"      (* setoid_ring plugin *)
-| "closed" "[" LIST1 qualid "]"      (* setoid_ring plugin *)
 | "preprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
 | "postprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
-| "setoid" term1_extended term1_extended      (* setoid_ring plugin *)
-| "sign" term1_extended      (* setoid_ring plugin *)
-| "power" term1_extended "[" LIST1 qualid "]"      (* setoid_ring plugin *)
-| "power_tac" term1_extended "[" ltac_expr "]"      (* setoid_ring plugin *)
-| "div" term1_extended      (* setoid_ring plugin *)
+| "setoid" one_term one_term      (* setoid_ring plugin *)
+| "sign" one_term      (* setoid_ring plugin *)
+| "power" one_term "[" LIST1 qualid "]"      (* setoid_ring plugin *)
+| "power_tac" one_term "[" ltac_expr "]"      (* setoid_ring plugin *)
+| "div" one_term      (* setoid_ring plugin *)
+| "closed" "[" LIST1 qualid "]"      (* setoid_ring plugin *)
 ]
 
 field_mod: [
 | ring_mod      (* setoid_ring plugin *)
-| "completeness" term1_extended      (* setoid_ring plugin *)
+| "completeness" one_term      (* setoid_ring plugin *)
 ]
 
 debug: [
@@ -1216,15 +1206,21 @@ query_command: [
 | "Eval" red_expr "in" term "."
 | "Compute" term "."
 | "Check" term "."
-| "About" smart_global OPT ( "@{" LIST0 name "}" ) "."
-| "SearchHead" term1_extended in_or_out_modules "."
-| "SearchPattern" term1_extended in_or_out_modules "."
-| "SearchRewrite" term1_extended in_or_out_modules "."
+| "About" smart_qualid OPT ( "@{" LIST0 name "}" ) "."
+| "SearchHead" one_term in_or_out_modules "."
+| "SearchPattern" one_term in_or_out_modules "."
+| "SearchRewrite" one_term in_or_out_modules "."
 | "Search" searchabout_query searchabout_queries "."
 | "SearchAbout" searchabout_query searchabout_queries "."
 | "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
 ]
 
+class: [
+| "Funclass"
+| "Sortclass"
+| smart_qualid
+]
+
 ne_in_or_out_modules: [
 | "inside" LIST1 qualid
 | "outside" LIST1 qualid
@@ -1242,7 +1238,7 @@ positive_search_mark: [
 
 searchabout_query: [
 | positive_search_mark string OPT ( "%" ident )
-| positive_search_mark term1_extended
+| positive_search_mark one_term
 ]
 
 searchabout_queries: [
@@ -1256,10 +1252,10 @@ syntax: [
 | "Close" "Scope" ident
 | "Delimit" "Scope" ident "with" ident
 | "Undelimit" "Scope" ident
-| "Bind" "Scope" ident "with" LIST1 class_rawexpr
-| "Infix" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
-| "Notation" ident LIST0 ident ":=" term1_extended OPT ( "(" "only" "parsing" ")" )
-| "Notation" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
+| "Bind" "Scope" ident "with" LIST1 class
+| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
+| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
+| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
 | "Format" "Notation" string string string
 | "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
 | "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
@@ -1314,17 +1310,17 @@ at_level_opt: [
 
 simple_tactic: [
 | "reflexivity"
-| "exact" term1_extended
+| "exact" one_term
 | "assumption"
 | "etransitivity"
-| "cut" term1_extended
-| "exact_no_check" term1_extended
-| "vm_cast_no_check" term1_extended
-| "native_cast_no_check" term1_extended
-| "casetype" term1_extended
-| "elimtype" term1_extended
-| "lapply" term1_extended
-| "transitivity" term1_extended
+| "cut" one_term
+| "exact_no_check" one_term
+| "vm_cast_no_check" one_term
+| "native_cast_no_check" one_term
+| "casetype" one_term
+| "elimtype" one_term
+| "lapply" one_term
+| "transitivity" one_term
 | "left"
 | "eleft"
 | "left" "with" bindings
@@ -1377,11 +1373,11 @@ simple_tactic: [
 | "clear" LIST0 ident
 | "clear" "-" LIST1 ident
 | "clearbody" LIST1 ident
-| "generalize" "dependent" term1_extended
-| "replace" term1_extended "with" term1_extended clause_dft_concl by_arg_tac
-| "replace" "->" term1_extended clause_dft_concl
-| "replace" "<-" term1_extended clause_dft_concl
-| "replace" term1_extended clause_dft_concl
+| "generalize" "dependent" one_term
+| "replace" one_term "with" one_term clause_dft_concl by_arg_tac
+| "replace" "->" one_term clause_dft_concl
+| "replace" "<-" one_term clause_dft_concl
+| "replace" one_term clause_dft_concl
 | "simplify_eq"
 | "simplify_eq" destruction_arg
 | "esimplify_eq"
@@ -1400,64 +1396,64 @@ simple_tactic: [
 | "einjection" destruction_arg "as" LIST0 simple_intropattern
 | "simple" "injection"
 | "simple" "injection" destruction_arg
-| "dependent" "rewrite" orient term1_extended
-| "dependent" "rewrite" orient term1_extended "in" ident
-| "cutrewrite" orient term1_extended
-| "cutrewrite" orient term1_extended "in" ident
-| "decompose" "sum" term1_extended
-| "decompose" "record" term1_extended
-| "absurd" term1_extended
+| "dependent" "rewrite" orient one_term
+| "dependent" "rewrite" orient one_term "in" ident
+| "cutrewrite" orient one_term
+| "cutrewrite" orient one_term "in" ident
+| "decompose" "sum" one_term
+| "decompose" "record" one_term
+| "absurd" one_term
 | "contradiction" OPT constr_with_bindings
 | "autorewrite" "with" LIST1 ident clause_dft_concl
 | "autorewrite" "with" LIST1 ident clause_dft_concl "using" ltac_expr
 | "autorewrite" "*" "with" LIST1 ident clause_dft_concl
 | "autorewrite" "*" "with" LIST1 ident clause_dft_concl "using" ltac_expr
-| "rewrite" "*" orient term1_extended "in" ident "at" occurrences by_arg_tac
-| "rewrite" "*" orient term1_extended "at" occurrences "in" ident by_arg_tac
-| "rewrite" "*" orient term1_extended "in" ident by_arg_tac
-| "rewrite" "*" orient term1_extended "at" occurrences by_arg_tac
-| "rewrite" "*" orient term1_extended by_arg_tac
-| "refine" term1_extended
-| "simple" "refine" term1_extended
-| "notypeclasses" "refine" term1_extended
-| "simple" "notypeclasses" "refine" term1_extended
+| "rewrite" "*" orient one_term "in" ident "at" occurrences by_arg_tac
+| "rewrite" "*" orient one_term "at" occurrences "in" ident by_arg_tac
+| "rewrite" "*" orient one_term "in" ident by_arg_tac
+| "rewrite" "*" orient one_term "at" occurrences by_arg_tac
+| "rewrite" "*" orient one_term by_arg_tac
+| "refine" one_term
+| "simple" "refine" one_term
+| "notypeclasses" "refine" one_term
+| "simple" "notypeclasses" "refine" one_term
 | "solve_constraints"
 | "subst" LIST1 ident
 | "subst"
 | "simple" "subst"
 | "evar" "(" ident ":" term ")"
-| "evar" term1_extended
+| "evar" one_term
 | "instantiate" "(" ident ":=" term ")"
 | "instantiate" "(" int ":=" term ")" hloc
 | "instantiate"
-| "stepl" term1_extended "by" ltac_expr
-| "stepl" term1_extended
-| "stepr" term1_extended "by" ltac_expr
-| "stepr" term1_extended
+| "stepl" one_term "by" ltac_expr
+| "stepl" one_term
+| "stepr" one_term "by" ltac_expr
+| "stepr" one_term
 | "generalize_eqs" ident
 | "dependent" "generalize_eqs" ident
 | "generalize_eqs_vars" ident
 | "dependent" "generalize_eqs_vars" ident
 | "specialize_eqs" ident
-| "hresolve_core" "(" ident ":=" term1_extended ")" "at" int_or_var "in" term1_extended
-| "hresolve_core" "(" ident ":=" term1_extended ")" "in" term1_extended
+| "hresolve_core" "(" ident ":=" one_term ")" "at" int_or_var "in" one_term
+| "hresolve_core" "(" ident ":=" one_term ")" "in" one_term
 | "hget_evar" int_or_var
 | "destauto"
 | "destauto" "in" ident
 | "transparent_abstract" ltac_expr3
 | "transparent_abstract" ltac_expr3 "using" ident
-| "constr_eq" term1_extended term1_extended
-| "constr_eq_strict" term1_extended term1_extended
-| "constr_eq_nounivs" term1_extended term1_extended
-| "is_evar" term1_extended
-| "has_evar" term1_extended
-| "is_var" term1_extended
-| "is_fix" term1_extended
-| "is_cofix" term1_extended
-| "is_ind" term1_extended
-| "is_constructor" term1_extended
-| "is_proj" term1_extended
-| "is_const" term1_extended
+| "constr_eq" one_term one_term
+| "constr_eq_strict" one_term one_term
+| "constr_eq_nounivs" one_term one_term
+| "is_evar" one_term
+| "has_evar" one_term
+| "is_var" one_term
+| "is_fix" one_term
+| "is_cofix" one_term
+| "is_ind" one_term
+| "is_constructor" one_term
+| "is_proj" one_term
+| "is_const" one_term
 | "shelve"
 | "shelve_unifiable"
 | "unshelve" ltac_expr1
@@ -1466,7 +1462,7 @@ simple_tactic: [
 | "swap" int_or_var int_or_var
 | "revgoals"
 | "guard" int_or_var comparison int_or_var
-| "decompose" "[" LIST1 term1_extended "]" term1_extended
+| "decompose" "[" LIST1 one_term "]" one_term
 | "optimize_heap"
 | "start" "ltac" "profiling"
 | "stop" "ltac" "profiling"
@@ -1478,14 +1474,14 @@ simple_tactic: [
 | "finish_timing" OPT string
 | "finish_timing" "(" string ")" OPT string
 | "eassumption"
-| "eexact" term1_extended
+| "eexact" one_term
 | "trivial" auto_using hintbases
 | "info_trivial" auto_using hintbases
 | "debug" "trivial" auto_using hintbases
 | "auto" OPT int_or_var auto_using hintbases
 | "info_auto" OPT int_or_var auto_using hintbases
 | "debug" "auto" OPT int_or_var auto_using hintbases
-| "prolog" "[" LIST0 term1_extended "]" int_or_var
+| "prolog" "[" LIST0 one_term "]" int_or_var
 | "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
 | "new" "auto" OPT int_or_var auto_using hintbases
 | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
@@ -1494,17 +1490,17 @@ simple_tactic: [
 | "autounfold" hintbases clause_dft_concl
 | "autounfold_one" hintbases "in" ident
 | "autounfold_one" hintbases
-| "unify" term1_extended term1_extended
-| "unify" term1_extended term1_extended "with" ident
-| "convert_concl_no_check" term1_extended
+| "unify" one_term one_term
+| "unify" one_term one_term "with" ident
+| "convert_concl_no_check" one_term
 | "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 ident
 | "typeclasses" "eauto" OPT int_or_var "with" LIST1 ident
 | "typeclasses" "eauto" OPT int_or_var
-| "head_of_constr" ident term1_extended
-| "not_evar" term1_extended
-| "is_ground" term1_extended
-| "autoapply" term1_extended "using" ident
-| "autoapply" term1_extended "with" ident
+| "head_of_constr" ident one_term
+| "not_evar" one_term
+| "is_ground" one_term
+| "autoapply" one_term "using" ident
+| "autoapply" one_term "with" ident
 | "progress_evars" ltac_expr
 | "rewrite_strat" rewstrategy
 | "rewrite_db" ident "in" ident
@@ -1518,10 +1514,10 @@ simple_tactic: [
 | "setoid_symmetry"
 | "setoid_symmetry" "in" ident
 | "setoid_reflexivity"
-| "setoid_transitivity" term1_extended
+| "setoid_transitivity" one_term
 | "setoid_etransitivity"
 | "decide" "equality"
-| "compare" term1_extended term1_extended
+| "compare" one_term one_term
 | "rewrite_strat" rewstrategy "in" ident
 | "intros" intropattern_list_opt
 | "eintros" intropattern_list_opt
@@ -1536,41 +1532,43 @@ simple_tactic: [
 | "fix" ident num "with" LIST1 fixdecl
 | "cofix" ident "with" LIST1 cofixdecl
 | "pose" bindings_with_parameters
-| "pose" term1_extended as_name
+| "pose" one_term as_name
 | "epose" bindings_with_parameters
-| "epose" term1_extended as_name
+| "epose" one_term as_name
 | "set" bindings_with_parameters clause_dft_concl
-| "set" term1_extended as_name clause_dft_concl
+| "set" one_term as_name clause_dft_concl
 | "eset" bindings_with_parameters clause_dft_concl
-| "eset" term1_extended as_name clause_dft_concl
-| "remember" term1_extended as_name eqn_ipat clause_dft_all
-| "eremember" term1_extended as_name eqn_ipat clause_dft_all
+| "eset" one_term as_name clause_dft_concl
+| "remember" one_term as_name eqn_ipat clause_dft_all
+| "eremember" one_term as_name eqn_ipat clause_dft_all
 | "assert" "(" ident ":=" term ")"
 | "eassert" "(" ident ":=" term ")"
 | "assert" "(" ident ":" term ")" by_tactic
 | "eassert" "(" ident ":" term ")" by_tactic
 | "enough" "(" ident ":" term ")" by_tactic
 | "eenough" "(" ident ":" term ")" by_tactic
-| "assert" term1_extended as_ipat by_tactic
-| "eassert" term1_extended as_ipat by_tactic
+| "assert" one_term as_ipat by_tactic
+| "eassert" one_term as_ipat by_tactic
+| "pose" "proof" "(" ident ":=" term ")"
+| "epose" "proof" "(" ident ":=" term ")"
 | "pose" "proof" term as_ipat
 | "epose" "proof" term as_ipat
-| "enough" term1_extended as_ipat by_tactic
-| "eenough" term1_extended as_ipat by_tactic
-| "generalize" term1_extended
-| "generalize" term1_extended LIST1 term1_extended
-| "generalize" term1_extended OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ]
+| "enough" one_term as_ipat by_tactic
+| "eenough" one_term as_ipat by_tactic
+| "generalize" one_term
+| "generalize" one_term LIST1 one_term
+| "generalize" one_term OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ]
 | "induction" induction_clause_list
 | "einduction" induction_clause_list
 | "destruct" induction_clause_list
 | "edestruct" induction_clause_list
 | "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
 | "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
-| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" term1_extended ]
+| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" one_term ]
 | "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
 | "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
 | "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list
-| "inversion" quantified_hypothesis "using" term1_extended in_hyp_list
+| "inversion" quantified_hypothesis "using" one_term in_hyp_list
 | "red" clause_dft_concl
 | "hnf" clause_dft_concl
 | "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl
@@ -1581,7 +1579,7 @@ simple_tactic: [
 | "vm_compute" OPT ref_or_pattern_occ clause_dft_concl
 | "native_compute" OPT ref_or_pattern_occ clause_dft_concl
 | "unfold" LIST1 unfold_occ SEP "," clause_dft_concl
-| "fold" LIST1 term1_extended clause_dft_concl
+| "fold" LIST1 one_term clause_dft_concl
 | "pattern" LIST1 pattern_occ SEP "," clause_dft_concl
 | "change" conversion clause_dft_concl
 | "change_no_check" conversion clause_dft_concl
@@ -1589,16 +1587,16 @@ simple_tactic: [
 | "rtauto"
 | "congruence"
 | "congruence" int
-| "congruence" "with" LIST1 term1_extended
-| "congruence" int "with" LIST1 term1_extended
+| "congruence" "with" LIST1 one_term
+| "congruence" int "with" LIST1 one_term
 | "f_equal"
 | "firstorder" OPT ltac_expr firstorder_using
 | "firstorder" OPT ltac_expr "with" LIST1 ident
 | "firstorder" OPT ltac_expr firstorder_using "with" LIST1 ident
 | "gintuition" OPT ltac_expr
 | "functional" "inversion" quantified_hypothesis OPT qualid      (* funind plugin *)
-| "functional" "induction" LIST1 term1_extended fun_ind_using with_names      (* funind plugin *)
-| "soft" "functional" "induction" LIST1 term1_extended fun_ind_using with_names      (* funind plugin *)
+| "functional" "induction" LIST1 one_term fun_ind_using with_names      (* funind plugin *)
+| "soft" "functional" "induction" LIST1 one_term fun_ind_using with_names      (* funind plugin *)
 | "psatz_Z" int_or_var ltac_expr      (* micromega plugin *)
 | "psatz_Z" ltac_expr      (* micromega plugin *)
 | "xlia" ltac_expr      (* micromega plugin *)
@@ -1614,16 +1612,17 @@ simple_tactic: [
 | "psatz_R" ltac_expr      (* micromega plugin *)
 | "psatz_Q" int_or_var ltac_expr      (* micromega plugin *)
 | "psatz_Q" ltac_expr      (* micromega plugin *)
-| "zify_iter_specs" ltac_expr      (* micromega plugin *)
+| "zify_iter_specs"      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
 | "zify_saturate"      (* micromega plugin *)
 | "zify_iter_let" ltac_expr      (* micromega plugin *)
-| "nsatz_compute" term1_extended      (* nsatz plugin *)
+| "zify_elim_let"      (* micromega plugin *)
+| "nsatz_compute" one_term      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
 | "protect_fv" string "in" ident      (* setoid_ring plugin *)
 | "protect_fv" string      (* setoid_ring plugin *)
-| "ring_lookup" ltac_expr0 "[" LIST0 term1_extended "]" LIST1 term1_extended      (* setoid_ring plugin *)
-| "field_lookup" ltac_expr "[" LIST0 term1_extended "]" LIST1 term1_extended      (* setoid_ring plugin *)
+| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
+| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
 ]
 
 hloc: [
@@ -1646,11 +1645,23 @@ by_arg_tac: [
 ]
 
 in_clause: [
-| in_clause
+| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ )
+| "*" "|-" OPT concl_occ
 | "*" OPT ( "at" occs_nums )
-| "*" "|-" concl_occ
-| LIST0 hypident_occ SEP "," "|-" concl_occ
-| LIST0 hypident_occ SEP ","
+]
+
+concl_occ: [
+| "*" OPT ( "at" occs_nums )
+]
+
+hypident_occ: [
+| hypident OPT ( "at" occs_nums )
+]
+
+hypident: [
+| ident
+| "(" "type" "of" ident ")"
+| "(" "value" "of" ident ")"
 ]
 
 as_ipat: [
@@ -1707,7 +1718,7 @@ induction_clause_list: [
 ]
 
 auto_using: [
-| "using" LIST1 term1_extended SEP ","
+| "using" LIST1 one_term SEP ","
 |
 ]
 
@@ -1762,7 +1773,7 @@ simple_binding: [
 
 bindings: [
 | LIST1 simple_binding
-| LIST1 term1_extended
+| LIST1 one_term
 ]
 
 comparison: [
@@ -1783,16 +1794,6 @@ bindings_with_parameters: [
 | "(" ident LIST0 simple_binder ":=" term ")"
 ]
 
-hypident: [
-| ident
-| "(" "type" "of" ident ")"
-| "(" "value" "of" ident ")"
-]
-
-hypident_occ: [
-| hypident OPT ( "at" occs_nums )
-]
-
 clause_dft_concl: [
 | "in" in_clause
 | OPT ( "at" occs_nums )
@@ -1810,11 +1811,6 @@ opt_clause: [
 |
 ]
 
-concl_occ: [
-| "*" OPT ( "at" occs_nums )
-|
-]
-
 in_hyp_list: [
 | "in" LIST1 ident
 |
@@ -1844,7 +1840,7 @@ cofixdecl: [
 ]
 
 constr_with_bindings: [
-| term1_extended with_bindings
+| one_term with_bindings
 ]
 
 with_bindings: [
@@ -1869,9 +1865,9 @@ quantified_hypothesis: [
 ]
 
 conversion: [
-| term1_extended
-| term1_extended "with" term1_extended
-| term1_extended "at" occs_nums "with" term1_extended
+| one_term
+| one_term "with" one_term
+| one_term "at" occs_nums "with" one_term
 ]
 
 firstorder_using: [
@@ -1897,29 +1893,29 @@ occurrences: [
 ]
 
 rewstrategy: [
-| term1_extended
-| "<-" term1_extended
-| "subterms" rewstrategy
-| "subterm" rewstrategy
-| "innermost" rewstrategy
-| "outermost" rewstrategy
-| "bottomup" rewstrategy
-| "topdown" rewstrategy
-| "id"
+| one_term
+| "<-" one_term
 | "fail"
+| "id"
 | "refl"
 | "progress" rewstrategy
 | "try" rewstrategy
-| "any" rewstrategy
-| "repeat" rewstrategy
 | rewstrategy ";" rewstrategy
-| "(" rewstrategy ")"
 | "choice" rewstrategy rewstrategy
-| "old_hints" ident
+| "repeat" rewstrategy
+| "any" rewstrategy
+| "subterm" rewstrategy
+| "subterms" rewstrategy
+| "innermost" rewstrategy
+| "outermost" rewstrategy
+| "bottomup" rewstrategy
+| "topdown" rewstrategy
 | "hints" ident
-| "terms" LIST0 term1_extended
+| "terms" LIST0 one_term
 | "eval" red_expr
-| "fold" term1_extended
+| "fold" one_term
+| "(" rewstrategy ")"
+| "old_hints" ident
 ]
 
 ltac_expr: [
@@ -2037,7 +2033,7 @@ tactic_arg: [
 | "context" ident "[" term "]"
 | "type" "of" term
 | "fresh" LIST0 fresh_id
-| "type_term" term1_extended
+| "type_term" one_term
 | "numgoals"
 ]