8 files changed, 175 insertions, 128 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 35a605ddd..32de15ee3 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -123,11 +123,24 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
           :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
           induction principles.
 
-``.. prodn::`` :black_nib: Grammar productions.
+``.. prodn::`` A grammar production.
     This is useful if you intend to document individual grammar productions.
     Otherwise, use Sphinx's `production lists
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
 
+    Unlike ``.. productionlist``\ s, this directive accepts notation syntax.
+
+
+    Usage::
+
+       .. prodn:: token += production
+       .. prodn:: token ::= production
+
+    Example::
+
+        .. prodn:: term += let: @pattern := @term in @term
+        .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+
 ``.. tacn::`` :black_nib: A tactic, or a tactic notation.
     Example::
 
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index e10e16c10..e4d24a1f7 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -106,7 +106,7 @@ argument.
 
 Morphisms can also be contravariant in one or more of their arguments.
 A morphism is contravariant on an argument associated to the relation
-instance :math`R` if it is covariant on the same argument when the inverse
+instance :math:`R` if it is covariant on the same argument when the inverse
 relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->``
 is used in signatures for contravariant morphisms.
 
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 47d3a7d7c..6a9b343ba 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -310,16 +310,15 @@ The :n:`@ident` is not relevant. It is just used for error messages. The
 axioms. The optional list of modifiers is used to tailor the behavior
 of the tactic. The following list describes their syntax and effects:
 
-.. prodn::
-   ring_mod ::= abstract %| decidable @term %| morphism @term
-                %| setoid @term @term 
-                %| constants [@ltac] 
-                %| preprocess [@ltac]
-                %| postprocess [@ltac]
-                %| power_tac @term [@ltac] 
-                %| sign @term
-                %| div @term
-
+.. productionlist:: coq
+   ring_mod : abstract | decidable `term` | morphism `term`
+            : | setoid `term` `term`
+            : | constants [`ltac`]
+            : | preprocess [`ltac`]
+            : | postprocess [`ltac`]
+            : | power_tac `term` [`ltac`]
+            : | sign `term`
+            : | div `term`
 
 abstract
   declares the ring as abstract. This is the default.
@@ -663,8 +662,8 @@ messages. :n:`@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.
 
-.. prodn::
-   field_mod := @ring_mod %| completeness @term
+.. 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
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index f65400e88..135c24aed 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -201,9 +201,9 @@ html_static_path = ['_static']
 # The empty string is equivalent to '%b %d, %Y'.
 #html_last_updated_fmt = None
 
-# If true, SmartyPants will be used to convert quotes and dashes to
-# typographically correct entities.
-html_use_smartypants = False # FIXME wrap code in <code> tags, otherwise quotesget converted in there
+# FIXME: this could be re-enabled after ensuring that smart quotes are locally
+# disabled for all relevant directives
+smartquotes = False
 
 # Custom sidebar templates, maps document names to template names.
 #html_sidebars = {}
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ff5d352c9..c21d8d4ec 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1925,74 +1925,75 @@ applied to an unknown structure instance (an implicit argument) and a
 value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
-Assume that `qualid` denotes an object ``(Build_struc`` |c_1| … |c_n| ``)`` in the
-structure *struct* of which the fields are |x_1|, …, |x_n|. Assume that
-`qualid` is declared as a canonical structure using the command
-
 .. cmd:: Canonical Structure @qualid
 
-Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
-solved during the type-checking process, `qualid` is used as a solution.
-Otherwise said, `qualid` is canonically used to extend the field |c_i|
-into a complete structure built on |c_i|.
+   This command declares :token:`qualid` as a canonical structure.
 
-Canonical structures are particularly useful when mixed with coercions
-and strict implicit arguments. Here is an example.
+   Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
+   structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
+   Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
+   solved during the type-checking process, :token:`qualid` is used as a solution.
+   Otherwise said, :token:`qualid` is canonically used to extend the field |c_i|
+   into a complete structure built on |c_i|.
 
-.. coqtop:: all
+   Canonical structures are particularly useful when mixed with coercions
+   and strict implicit arguments.
 
-   Require Import Relations.
+   .. example::
 
-   Require Import EqNat.
+      Here is an example.
 
-   Set Implicit Arguments.
+      .. coqtop:: all
 
-   Unset Strict Implicit.
+         Require Import Relations.
 
-   Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
-                               Prf_equiv : equivalence Carrier Equal}.
+         Require Import EqNat.
 
-   Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
+         Set Implicit Arguments.
 
-   Axiom eq_nat_equiv : equivalence nat eq_nat.
+         Unset Strict Implicit.
 
-   Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
+         Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
+                                     Prf_equiv : equivalence Carrier Equal}.
 
-   Canonical Structure nat_setoid.
+         Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
 
-Thanks to ``nat_setoid`` declared as canonical, the implicit arguments ``A``
-and ``B`` can be synthesized in the next statement.
+         Axiom eq_nat_equiv : equivalence nat eq_nat.
 
-.. coqtop:: all
+         Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
 
-   Lemma is_law_S : is_law S.
+         Canonical Structure nat_setoid.
 
-Remark: If a same field occurs in several canonical structure, then
-only the structure declared first as canonical is considered.
+      Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A`
+      and :g:`B` can be synthesized in the next statement.
 
-.. cmdv:: Canonical Structure @ident := @term : @type
+      .. coqtop:: all
 
-.. cmdv:: Canonical Structure @ident := @term
+         Lemma is_law_S : is_law S.
 
-.. cmdv:: Canonical Structure @ident : @type := @term
+   .. note::
+      If a same field occurs in several canonical structures, then
+      only the structure declared first as canonical is considered.
 
-These are equivalent to a regular definition of `ident` followed by the declaration
-``Canonical Structure`` `ident`.
+   .. cmdv:: Canonical Structure @ident {? : @type } := @term
 
-See also: more examples in user contribution category (Rocq/ALGEBRA).
+      This is equivalent to a regular definition of :token:`ident` followed by the
+      declaration :n:`Canonical Structure @ident`.
 
 
-Print Canonical Projections.
-++++++++++++++++++++++++++++
+.. cmd:: Print Canonical Projections
 
-This displays the list of global names that are components of some
-canonical structure. For each of them, the canonical structure of
-which it is a projection is indicated. For instance, the above example
-gives the following output:
+   This displays the list of global names that are components of some
+   canonical structure. For each of them, the canonical structure of
+   which it is a projection is indicated.
 
-.. coqtop:: all
+   .. example::
+
+      For instance, the above example gives the following output:
+
+      .. coqtop:: all
 
-   Print Canonical Projections.
+         Print Canonical Projections.
 
 
 Implicit types of variables
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 3b2009657..ab52c2ce7 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1484,7 +1484,7 @@ The abstract tactic
 ```````````````````
 
 .. tacn:: abstract: {+ d_item}
-   :name abstract (ssreflect)
+   :name: abstract (ssreflect)
 
 This tactic assigns an abstract constant previously introduced with the ``[:
 name ]`` intro pattern (see section :ref:`introduction_ssr`).
@@ -2402,7 +2402,7 @@ tactic:
 The behavior of the defective have tactic makes it possible to
 generalize it in the following general construction:
 
-.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @binder } } {? : @term } {? := @term | by @tactic }
+.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic }
 
 Open syntax is supported for both :token:`term`. For the description
 of :token:`i_item` and :token:`s_item` see section
@@ -3657,7 +3657,8 @@ selective rewriting, blocking on the fly the reduction in the term ``t``.
 
   .. coqtop:: reset
 
-     From Coq Require Import ssreflect ssrfun ssrbool List.
+     From Coq Require Import ssreflect ssrfun ssrbool.
+     From Coq Require Import List.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -5241,7 +5242,7 @@ Notation scope
 
 Module name
 
-.. prodn:: name ::= @qualid
+.. prodn:: modname ::= @qualid
 
 Natural number
 
@@ -5251,14 +5252,10 @@ where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral
 (should not be the name of a tactic which can be followed by a
 bracket ``[``, like ``do``, ``have``,…)
 
-Pattern
-
-.. prodn:: pattern ::= @term
-
 Items and switches
 ~~~~~~~~~~~~~~~~~~
 
-.. prodn:: binder ::= @ident %| ( @ident {? : @term } )
+.. prodn:: ssr_binder ::= @ident %| ( @ident {? : @term } )
 
 binder see :ref:`abbreviations_ssr`.
 
@@ -5353,8 +5350,8 @@ case analysis see :ref:`the_defective_tactics_ssr`
 
 rewrite  see :ref:`rewriting_ssr`
 
-.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } {? : @term } := @term
-.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } : @term {? by @tactic }
+.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term
+.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic }
 .. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term
 .. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
 .. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic }
@@ -5368,9 +5365,9 @@ forward  chaining see :ref:`structure_ssr`
 
 specializing see :ref:`structure_ssr`
 
-.. tacn:: suff {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic }
+.. tacn:: suff {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic }
    :name: suff
-.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic }
+.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic }
    :name: suffices
 .. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
 .. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
@@ -5381,7 +5378,7 @@ backchaining see :ref:`structure_ssr`
 
 local definition :ref:`definitions_ssr`
 
-.. tacv:: pose @ident {+ @binder } := @term
+.. tacv:: pose @ident {+ @ssr_binder } := @term
 
 local function definition
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 29c2f8b81..d0a0d568e 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3949,9 +3949,20 @@ succeeds, and results in an error otherwise.
    :name: constr_eq
 
    This tactic checks whether its arguments are equal modulo alpha
-   conversion and casts.
+   conversion, casts and universe constraints. It may unify universes.
 
 .. exn:: Not equal.
+.. exn:: Not equal (due to universes).
+
+.. tacn:: constr_eq_strict @term @term
+   :name: constr_eq_strict
+
+   This tactic checks whether its arguments are equal modulo alpha
+   conversion, casts and universe constraints. It does not add new
+   constraints.
+
+.. exn:: Not equal.
+.. exn:: Not equal (due to universes).
 
 .. tacn:: unify @term @term
    :name: unify
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index ab3a485b2..c9487abf0 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -28,6 +28,7 @@ from docutils.parsers.rst.directives.admonitions import BaseAdmonition
 
 from sphinx import addnodes
 from sphinx.roles import XRefRole
+from sphinx.errors import ExtensionError
 from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode
 from sphinx.util.logging import getLogger
 from sphinx.directives import ObjectDescription
@@ -103,10 +104,16 @@ class CoqObject(ObjectDescription):
         'undocumented': directives.flag
     }
 
-    def _subdomain(self):
+    def subdomain_data(self):
         if self.subdomain is None:
             raise ValueError()
-        return self.subdomain
+        return self.env.domaindata['coq']['objects'][self.subdomain]
+
+    def _render_annotation(self, signode):
+        if self.annotation:
+            annot_node = nodes.inline(self.annotation, self.annotation, classes=['sigannot'])
+            signode += addnodes.desc_annotation(self.annotation, '', annot_node)
+            signode += nodes.Text(' ')
 
     def handle_signature(self, signature, signode):
         """Prefix signature with the proper annotation, then render it using
@@ -114,29 +121,32 @@ class CoqObject(ObjectDescription):
 
         :returns: the name given to the resulting node, if any
         """
-        if self.annotation:
-            annotation = self.annotation + ' '
-            signode += addnodes.desc_annotation(annotation, annotation)
+        self._render_annotation(signode)
         self._render_signature(signature, signode)
         return self._names.get(signature) or self._name_from_signature(signature)
 
+    def _warn_if_duplicate_name(self, objects, name):
+        """Check that two objects in the same domain don't have the same name."""
+        if name in objects:
+            MSG = 'Duplicate object: {}; other is at {}'
+            msg = MSG.format(name, self.env.doc2path(objects[name][0]))
+            self.state_machine.reporter.warning(msg, line=self.lineno)
+
     def _record_name(self, name, target_id):
         """Record a name, mapping it to target_id
 
         Warns if another object of the same name already exists.
         """
-        names_in_subdomain = self.env.domaindata['coq']['objects'][self._subdomain()]
-        # Check that two objects in the same domain don't have the same name
-        if name in names_in_subdomain:
-            self.state_machine.reporter.warning(
-                'Duplicate Coq object: {}; other is at {}'.format(
-                    name, self.env.doc2path(names_in_subdomain[name][0])),
-                line=self.lineno)
+        names_in_subdomain = self.subdomain_data()
+        self._warn_if_duplicate_name(names_in_subdomain, name)
         names_in_subdomain[name] = (self.env.docname, self.objtype, target_id)
 
+    def _target_id(self, name):
+        return make_target(self.objtype, nodes.make_id(name))
+
     def _add_target(self, signode, name):
         """Register a link target ‘name’, pointing to signode."""
-        targetid = make_target(self.objtype, nodes.make_id(name))
+        targetid = self._target_id(name)
         if targetid not in self.state.document.ids:
             signode['ids'].append(targetid)
             signode['names'].append(name)
@@ -314,50 +324,71 @@ class OptionObject(NotationObject):
     def _name_from_signature(self, signature):
         return stringify_with_ellipses(signature)
 
-class ProductionObject(NotationObject):
-    """Grammar productions.
+class ProductionObject(CoqObject):
+    r"""A grammar production.
 
     This is useful if you intend to document individual grammar productions.
     Otherwise, use Sphinx's `production lists
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
+
+    Unlike ``.. productionlist``\ s, this directive accepts notation syntax.
+
+
+    Usage::
+
+       .. prodn:: token += production
+       .. prodn:: token ::= production
+
+    Example::
+
+        .. prodn:: term += let: @pattern := @term in @term
+        .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+
     """
-    # FIXME (CPC): I have no idea what this does :/  Someone should add an example.
     subdomain = "prodn"
-    index_suffix = None
-    annotation = None
+    #annotation = "Grammar production"
 
-    # override to create link targets for production left-hand sides
-    def run(self):
+    def _render_signature(self, signature, signode):
+        raise NotImplementedError(self)
+
+    SIG_ERROR = ("Invalid syntax in ``.. prodn::`` directive"
+                 + "\nExpected ``name ::= ...`` or ``name += ...``"
+                 + " (e.g. ``pattern += constr:(@ident)``)")
+
+    def handle_signature(self, signature, signode):
+        nsplits = 2
+        parts = signature.split(maxsplit=nsplits)
+        if len(parts) != 3:
+            raise ExtensionError(ProductionObject.SIG_ERROR)
+
+        lhs, op, rhs = (part.strip() for part in parts)
+        if op not in ["::=", "+="]:
+            raise ExtensionError(ProductionObject.SIG_ERROR)
+
+        self._render_annotation(signode)
+
+        lhs_op = '{} {} '.format(lhs, op)
+        lhs_node = nodes.literal(lhs_op, lhs_op)
+
+        position = self.state_machine.get_source_and_line(self.lineno)
+        rhs_node = parse_notation(rhs, *position)
+        signode += addnodes.desc_name(signature, '', lhs_node, rhs_node)
+
+        return ('token', lhs) if op == '::=' else None
+
+    def _add_index_entry(self, name, target):
+        pass
+
+    def _target_id(self, name):
+        # Use `name[1]` instead of ``nodes.make_id(name[1])`` to work around
+        # https://github.com/sphinx-doc/sphinx/issues/4983
+        return 'grammar-token-{}'.format(name[1])
+
+    def _record_name(self, name, targetid):
         env = self.state.document.settings.env
         objects = env.domaindata['std']['objects']
-
-        class ProdnError(Exception):
-            """Exception for ill-formed prodn"""
-            pass
-
-        [idx, node] = super().run()
-        try:
-            # find LHS of production
-            inline_lhs = node[0][0][0][0]  # may be fragile !!!
-            lhs_str = str(inline_lhs)
-            if lhs_str[0:7] != "<inline":
-                raise ProdnError("Expected atom on LHS")
-            lhs = inline_lhs[0]
-            # register link target
-            subnode = addnodes.production()
-            subnode['tokenname'] = lhs
-            idname = 'grammar-token-%s' % subnode['tokenname']
-            if idname not in self.state.document.ids:
-                subnode['ids'].append(idname)
-            self.state.document.note_implicit_target(subnode, subnode)
-            objects['token', subnode['tokenname']] = env.docname, idname
-            subnode.extend(token_xrefs(lhs))
-            # patch in link target
-            inline_lhs['ids'].append(idname)
-        except ProdnError as err:
-            getLogger(__name__).warning("Could not create link target for prodn: " + str(err) +
-                                        "\nSphinx represents the prodn as: " + str(node) + "\n")
-        return [idx, node]
+        self._warn_if_duplicate_name(objects, name)
+        objects[name] = env.docname, targetid
 
 class ExceptionObject(NotationObject):
     """An error raised by a Coq command or tactic.
@@ -841,11 +872,6 @@ class CoqOptionIndex(CoqSubdomainsIndex):
 class CoqGallinaIndex(CoqSubdomainsIndex):
     name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"]
 
-# we specify an index to make productions fit into the framework of notations
-# but not likely to include a link to this index
-class CoqProductionIndex(CoqSubdomainsIndex):
-    name, localname, shortname, subdomains = "prodnindex", "Production Index", "productions", ["prodn"]
-
 class CoqExceptionIndex(CoqSubdomainsIndex):
     name, localname, shortname, subdomains = "exnindex", "Errors and Warnings Index", "errors", ["exn", "warn"]
 
@@ -952,7 +978,7 @@ class CoqDomain(Domain):
         'g': CoqCodeRole
     }
 
-    indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex]
+    indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqExceptionIndex]
 
     data_version = 1
     initial_data = {
@@ -1047,7 +1073,7 @@ def setup(app):
 
     # A few sanity checks:
     subdomains = set(obj.subdomain for obj in CoqDomain.directives.values())
-    assert subdomains == set(chain(*(idx.subdomains for idx in CoqDomain.indices)))
+    assert subdomains.issuperset(chain(*(idx.subdomains for idx in CoqDomain.indices)))
     assert subdomains.issubset(CoqDomain.roles.keys())
 
     # Add domain, directives, and roles