14 files changed, 289 insertions, 233 deletions

diff --git a/clib/dyn.ml b/clib/dyn.ml
index e9b041988..6c4576724 100644
--- a/clib/dyn.ml
+++ b/clib/dyn.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module type TParam =
+module type ValueS =
 sig
   type 'a t
 end
@@ -16,40 +16,38 @@ end
 module type MapS =
 sig
   type t
-  type 'a obj
   type 'a key
+  type 'a value
   val empty : t
-  val add : 'a key -> 'a obj -> t -> t
+  val add : 'a key -> 'a value -> t -> t
   val remove : 'a key -> t -> t
-  val find : 'a key -> t -> 'a obj
+  val find : 'a key -> t -> 'a value
   val mem : 'a key -> t -> bool
 
-  type any = Any : 'a key * 'a obj -> any
-
-  type map = { map : 'a. 'a key -> 'a obj -> 'a obj }
+  type map = { map : 'a. 'a key -> 'a value -> 'a value }
   val map : map -> t -> t
 
+  type any = Any : 'a key * 'a value -> any
   val iter : (any -> unit) -> t -> unit
   val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
 end
 
 module type PreS =
 sig
-type 'a tag
-type t = Dyn : 'a tag * 'a -> t
-
-val create : string -> 'a tag
-val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
-val repr : 'a tag -> string
+  type 'a tag
+  type t = Dyn : 'a tag * 'a -> t
 
-type any = Any : 'a tag -> any
+  val create : string -> 'a tag
+  val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+  val repr : 'a tag -> string
 
-val name : string -> any option
+  val dump : unit -> (int * string) list
 
-module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
-
-val dump : unit -> (int * string) list
+  type any = Any : 'a tag -> any
+  val name : string -> any option
 
+  module Map(Value : ValueS) :
+    MapS with type 'a key = 'a tag and type 'a value = 'a Value.t
 end
 
 module type S =
@@ -57,104 +55,100 @@ sig
   include PreS
 
   module Easy : sig
-
     val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
     val make_dyn : string -> ('a -> t) * (t -> 'a)
     val inj : 'a -> 'a tag -> t
     val prj : t -> 'a tag -> 'a option
   end
-
 end
 
 module Make () = struct
-module Self : PreS = struct
-(* Dynamics, programmed with DANGER !!! *)
-
-type 'a tag = int
 
-type t = Dyn : 'a tag * 'a -> t
-
-type any = Any : 'a tag -> any
-
-let dyntab = ref (Int.Map.empty : string Int.Map.t)
-(** Instead of working with tags as strings, which are costly, we use their
-    hash. We ensure unicity of the hash in the [create] function. If ever a
-    collision occurs, which is unlikely, it is sufficient to tweak the offending
-    dynamic tag. *)
-
-let create (s : string) =
-  let hash = Hashtbl.hash s in
-  let () =
-    if Int.Map.mem hash !dyntab then
-      let old = Int.Map.find hash !dyntab in
-      let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in
+module Self : PreS = struct
+  (* Dynamics, programmed with DANGER !!! *)
+
+  type 'a tag = int
+
+  type t = Dyn : 'a tag * 'a -> t
+
+  type any = Any : 'a tag -> any
+
+  let dyntab = ref (Int.Map.empty : string Int.Map.t)
+  (** Instead of working with tags as strings, which are costly, we use their
+      hash. We ensure unicity of the hash in the [create] function. If ever a
+      collision occurs, which is unlikely, it is sufficient to tweak the offending
+      dynamic tag. *)
+
+  let create (s : string) =
+    let hash = Hashtbl.hash s in
+    let () =
+      if Int.Map.mem hash !dyntab then
+        let old = Int.Map.find hash !dyntab in
+        let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in
+        assert false
+    in
+    let () = dyntab := Int.Map.add hash s !dyntab in
+    hash
+
+  let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
+    fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
+
+  let repr s =
+    try Int.Map.find s !dyntab
+    with Not_found ->
+      let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in
       assert false
-  in
-  let () = dyntab := Int.Map.add hash s !dyntab in
-  hash
-
-let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
-  fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
-
-let repr s =
-  try Int.Map.find s !dyntab
-  with Not_found ->
-    let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in
-    assert false
-
-let name s =
-  let hash = Hashtbl.hash s in
-  if Int.Map.mem hash !dyntab then Some (Any hash) else None
-
-let dump () = Int.Map.bindings !dyntab
-
-module Map(M : TParam) =
-struct
-type t = Obj.t M.t Int.Map.t
-type 'a obj = 'a M.t
-type 'a key = 'a tag
-let cast : 'a M.t -> 'b M.t = Obj.magic
-let empty = Int.Map.empty
-let add tag v m = Int.Map.add tag (cast v) m
-let remove tag m = Int.Map.remove tag m
-let find tag m = cast (Int.Map.find tag m)
-let mem = Int.Map.mem
-
-type any = Any : 'a tag * 'a M.t -> any
-
-type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
-let map f m = Int.Map.mapi f.map m
-
-let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m
-let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu
-end
 
+  let name s =
+    let hash = Hashtbl.hash s in
+    if Int.Map.mem hash !dyntab then Some (Any hash) else None
+
+  let dump () = Int.Map.bindings !dyntab
+
+  module Map(Value: ValueS) =
+  struct
+    type t = Obj.t Value.t Int.Map.t
+    type 'a key = 'a tag
+    type 'a value = 'a Value.t
+    let cast : 'a value -> 'b value = Obj.magic
+    let empty = Int.Map.empty
+    let add tag v m = Int.Map.add tag (cast v) m
+    let remove tag m = Int.Map.remove tag m
+    let find tag m = cast (Int.Map.find tag m)
+    let mem = Int.Map.mem
+
+    type map = { map : 'a. 'a tag -> 'a value -> 'a value }
+    let map f m = Int.Map.mapi f.map m
+
+    type any = Any : 'a tag * 'a value -> any
+    let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m
+    let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu
+  end
 end
 include Self
 
 module Easy = struct
-
-(* now tags are opaque, we can do the trick *)
-let make_dyn_tag (s : string) =
- (fun (type a) (tag : a tag) ->
-  let infun : (a -> t) = fun x -> Dyn (tag, x) in
-  let outfun : (t -> a) = fun (Dyn (t, x)) ->
-    match eq tag t with
-    | None -> assert false
-    | Some CSig.Refl -> x
-  in
-  infun, outfun, tag)
- (create s)
-
-let make_dyn (s : string) =
-  let inf, outf, _ = make_dyn_tag s in inf, outf
-
-let inj x tag = Dyn(tag,x)
-let prj : type a. t -> a tag -> a option =
+  (* now tags are opaque, we can do the trick *)
+  let make_dyn_tag (s : string) =
+   (fun (type a) (tag : a tag) ->
+    let infun : (a -> t) = fun x -> Dyn (tag, x) in
+    let outfun : (t -> a) = fun (Dyn (t, x)) ->
+      match eq tag t with
+      | None -> assert false
+      | Some CSig.Refl -> x
+    in
+    infun, outfun, tag)
+   (create s)
+
+  let make_dyn (s : string) =
+    let inf, outf, _ = make_dyn_tag s in inf, outf
+
+  let inj x tag = Dyn(tag,x)
+  let prj : type a. t -> a tag -> a option =
     fun (Dyn(tag',x)) tag ->
-    match eq tag tag' with
-    | None -> None
-    | Some CSig.Refl -> Some x
+      match eq tag tag' with
+      | None -> None
+      | Some CSig.Refl -> Some x
 end
 
 end
diff --git a/clib/dyn.mli b/clib/dyn.mli
index 51d309142..ff9762bd6 100644
--- a/clib/dyn.mli
+++ b/clib/dyn.mli
@@ -10,7 +10,7 @@
 
 (** Dynamically typed values *)
 
-module type TParam =
+module type ValueS =
 sig
   type 'a t
 end
@@ -18,51 +18,66 @@ end
 module type MapS =
 sig
   type t
-  type 'a obj
   type 'a key
+  type 'a value
   val empty : t
-  val add : 'a key -> 'a obj -> t -> t
+  val add : 'a key -> 'a value -> t -> t
   val remove : 'a key -> t -> t
-  val find : 'a key -> t -> 'a obj
+  val find : 'a key -> t -> 'a value
   val mem : 'a key -> t -> bool
 
-  type any = Any : 'a key * 'a obj -> any
-
-  type map = { map : 'a. 'a key -> 'a obj -> 'a obj }
+  type map = { map : 'a. 'a key -> 'a value -> 'a value }
   val map : map -> t -> t
 
+  type any = Any : 'a key * 'a value -> any
   val iter : (any -> unit) -> t -> unit
   val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
 end
 
 module type S =
 sig
-type 'a tag
-type t = Dyn : 'a tag * 'a -> t
+  type 'a tag
+  (** Type of dynamic tags *)
 
-val create : string -> 'a tag
-val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
-val repr : 'a tag -> string
+  type t = Dyn : 'a tag * 'a -> t
+  (** Type of dynamic values *)
 
-type any = Any : 'a tag -> any
+  val create : string -> 'a tag
+  (** [create n] returns a tag describing a type called [n].
+      [create] raises an exception if [n] is already registered.
+      Type names are hashed, so [create] may raise even if no type with
+      the exact same name was registered due to a collision. *)
 
-val name : string -> any option
+  val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+  (** [eq t1 t2] returns [Some witness] if [t1] is the same as [t2], [None] otherwise. *)
 
-module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
+  val repr : 'a tag -> string
+  (** [repr tag] returns the name of the type represented by [tag]. *)
 
-val dump : unit -> (int * string) list
+  val dump : unit -> (int * string) list
+  (** [dump ()] returns a list of (tag, name) pairs for every type tag registered
+      in this [Dyn.Make] instance. *)
 
-module Easy : sig
+  type any = Any : 'a tag -> any
+  (** Type of boxed dynamic tags *)
 
-  (* To create a dynamic type on the fly *)
-  val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
-  val make_dyn : string -> ('a -> t) * (t -> 'a)
+  val name : string -> any option
+  (** [name n] returns [Some t] where t is a boxed tag previously registered
+      with [create n], or [None] if there is no such tag. *)
 
-  (* For types declared with the [create] function above *)
-  val inj : 'a -> 'a tag -> t
-  val prj : t -> 'a tag -> 'a option
-end
+  module Map(Value : ValueS) :
+    MapS with type 'a key = 'a tag and type 'a value = 'a Value.t
+  (** Map from type tags to values parameterized by the tag type *)
+
+  module Easy : sig
+    (* To create a dynamic type on the fly *)
+    val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
+    val make_dyn : string -> ('a -> t) * (t -> 'a)
 
+    (* For types declared with the [create] function above *)
+    val inj : 'a -> 'a tag -> t
+    val prj : t -> 'a tag -> 'a option
+  end
 end
 
 module Make () : S
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/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 135c24aed..8127d3df3 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -104,7 +104,6 @@ exclude_patterns = [
     'Thumbs.db',
     '.DS_Store',
     'introduction.rst',
-    'credits.rst',
     'README.rst',
     'README.template.rst'
 ]
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index a75659798..2562dec46 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1,3 +1,8 @@
+.. include:: preamble.rst
+.. include:: replaces.rst
+
+.. _credits:
+
 -------------------------------------------
 Credits
 -------------------------------------------
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 136f9088b..f3ae49381 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -1,16 +1,31 @@
-.. _introduction:
-
 .. include:: preamble.rst
 .. include:: replaces.rst
 
 .. include:: introduction.rst
-.. include:: credits.rst
 
 ------------------
 Table of contents
 ------------------
 
 .. toctree::
+   :caption: Indexes
+
+   genindex
+   coq-cmdindex
+   coq-tacindex
+   coq-optindex
+   coq-exnindex
+
+.. No entries yet
+  * :index:`thmindex`
+
+.. toctree::
+   :caption: Preamble
+
+   self
+   credits
+
+.. toctree::
    :caption: The language
 
    language/gallina-specification-language
@@ -65,18 +80,6 @@ Table of contents
 
    zebibliography
 
-.. toctree::
-   :caption: Indexes
-	     
-   genindex
-   coq-cmdindex
-   coq-tacindex	      
-   coq-optindex	      
-   coq-exnindex	      
-   
-.. No entries yet
-  * :index:`thmindex`
-
 This material (the Coq Reference Manual) may be distributed only subject to the
 terms and conditions set forth in the Open Publication License, v1.0 or later
 (the latest version is presently available at
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 75ff72c4d..20e4069f4 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -1,3 +1,5 @@
+.. _introduction:
+
 ------------------------
 Introduction
 ------------------------
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 1c554acdb..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
@@ -5242,7 +5242,7 @@ Notation scope
 
 Module name
 
-.. prodn:: name ::= @qualid
+.. prodn:: modname ::= @qualid
 
 Natural number
 
@@ -5252,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`.
 
@@ -5354,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 }
@@ -5369,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 }
@@ -5382,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/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
index cedd60d3b..57adcb287 100644
--- a/doc/tools/coqrst/coqdoc/main.py
+++ b/doc/tools/coqrst/coqdoc/main.py
@@ -20,6 +20,7 @@ lexer.
 """
 
 import os
+import platform
 from tempfile import mkstemp
 from subprocess import check_output
 
@@ -36,6 +37,9 @@ def coqdoc(coq_code, coqdoc_bin=None):
     """Get the output of coqdoc on coq_code."""
     coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc")
     fd, filename = mkstemp(prefix="coqdoc-", suffix=".v")
+    if platform.system().startswith("CYGWIN"):
+        # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..."
+        filename = check_output(["cygpath", "-w", filename]).decode("utf-8").strip()
     try:
         os.write(fd, COQDOC_HEADER.encode("utf-8"))
         os.write(fd, coq_code.encode("utf-8"))
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
diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli
index fa522e9c3..606a6ebea 100644
--- a/pretyping/geninterp.mli
+++ b/pretyping/geninterp.mli
@@ -42,8 +42,8 @@ sig
 
 end
 
-module ValTMap (M : Dyn.TParam) :
-  Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ
+module ValTMap (Value : Dyn.ValueS) :
+  Dyn.MapS with type 'a key = 'a Val.typ and type 'a value = 'a Value.t
 
 (** Dynamic types for toplevel values. While the generic types permit to relate
     objects at various levels of interpretation, toplevel values are wearing
diff --git a/tools/inferior-coq.el b/tools/inferior-coq.el
index b79d97d66..453bd1391 100644
--- a/tools/inferior-coq.el
+++ b/tools/inferior-coq.el
@@ -265,7 +265,7 @@ With argument, position cursor at end of buffer."
     (let ((end (point)))
       (beginning-of-line)
       (coq-send-region (point) end)))
-  (next-line 1))
+  (forward-line 1))
 
 (defun coq-send-abort ()
   "Send the command \"Abort.\" to the inferior Coq process."
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index e61f830f3..e1d35e537 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -92,6 +92,14 @@ let libs_init_load_path ~load_init =
   let coqpath = Envars.coqpath in
   let coq_path = Names.DirPath.make [Libnames.coq_root] in
 
+  (* current directory (not recursively!) *)
+  [ { recursive = false;
+      path_spec = VoPath { unix_path = ".";
+                           coq_path = Libnames.default_root_prefix;
+                           implicit = false;
+                           has_ml = AddTopML }
+    } ] @
+
   (* then standard library and plugins *)
   [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false;
    build_stdlib_path ~load_init ~unix_path:(coqlib/"plugins")  ~coq_path ~with_ml:true ] @
@@ -102,15 +110,7 @@ let libs_init_load_path ~load_init =
   ) @
 
   (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *)
-  List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) @
-
-  (* then current directory (not recursively!) *)
-  [ { recursive = false;
-      path_spec = VoPath { unix_path = ".";
-                           coq_path = Libnames.default_root_prefix;
-                           implicit = false;
-                           has_ml = AddTopML }
-    } ]
+  List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath)
 
 (* Initialises the Ocaml toplevel before launching it, so that it can
    find the "include" file in the *source* directory *)