A few fixes of unexisting tokens.

4 files changed, 18 insertions, 18 deletions

diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index cb267576b2..7b8a86d1ab 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -31,9 +31,9 @@ A variable pattern matches any value, and the identifier is bound to
 that value. The pattern “``_``” (called “don't care” or “wildcard” symbol)
 also matches any value, but does not bind anything. It may occur an
 arbitrary number of times in a pattern. Alias patterns written
-:n:`(@pattern as @identifier)` are also accepted. This pattern matches the
-same values as ``pattern`` does and ``identifier`` is bound to the matched
-value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A
+:n:`(@pattern as @ident)` are also accepted. This pattern matches the
+same values as :token:`pattern` does and :token:`ident` is bound to the matched
+value. A pattern of the form :n:`@pattern | @pattern` is called disjunctive. A
 list of patterns separated with commas is also considered as a pattern
 and is called *multiple pattern*. However multiple patterns can only
 occur at the root of pattern matching equations. Disjunctions of
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index a1a27a1186..b7d05fd6ef 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -47,30 +47,30 @@ extraction. They both display extracted term(s) inside |Coq|.
 All the following commands produce real ML files. User can choose to
 produce one monolithic file or one file per |Coq| library.
 
-.. cmd:: Extraction "@file" {+ @qualid }
+.. cmd:: Extraction @string {+ @qualid }
 
    Recursive extraction of all the mentioned objects and all
-   their dependencies in one monolithic `file`.
+   their dependencies in one monolithic file :token:`string`.
    Global and local identifiers are renamed according to the chosen ML
    language to fulfill its syntactic conventions, keeping original
    names as much as possible.
   
 .. cmd:: Extraction Library @ident
 
-   Extraction of the whole |Coq| library ``ident.v`` to an ML module
-   ``ident.ml``. In case of name clash, identifiers are here renamed
+   Extraction of the whole |Coq| library :n:`@ident.v` to an ML module
+   :n:`@ident.ml`. In case of name clash, identifiers are here renamed
    using prefixes ``coq_``  or ``Coq_`` to ensure a session-independent
    renaming.
 
 .. cmd:: Recursive Extraction Library @ident
 
-   Extraction of the |Coq| library ``ident.v`` and all other modules 
-   ``ident.v`` depends on.
+   Extraction of the |Coq| library :n:`@ident.v` and all other modules
+   :n:`@ident.v` depends on.
 
 .. cmd:: Separate Extraction {+ @qualid }
 
    Recursive extraction of all the mentioned objects and all
-   their dependencies, just as ``Extraction "file"``,
+   their dependencies, just as :n:`Extraction @string {+ @qualid }`,
    but instead of producing one monolithic file, this command splits
    the produced code in separate ML files, one per corresponding Coq
    ``.v`` file. This command is hence quite similar to
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 93375c42f1..64e2d7c4ab 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -40,9 +40,9 @@ In addition to these user-defined classes, we have two built-in classes:
 Formally, the syntax of a classes is defined as:
 
 .. productionlist::
-   class: qualid
-        : | `Sortclass`
-        : | `Funclass`
+   class: `qualid`
+        : | Sortclass
+        : | Funclass
 
 
 Coercions
@@ -202,10 +202,10 @@ grammar of inductive types from Figure :ref:`vernacular` as follows:
    \comindex{CoInductive \mbox{\rm (and coercions)}}
 
 .. productionlist::
-   inductive : `Inductive` ind_body `with` ... `with` ind_body
-             : | `CoInductive` ind_body `with` ... `with` ind_body
-   ind_body : ident [binders] : term := [[|] constructor | ... | constructor]
-   constructor : ident [binders] [:[>] term]
+   inductive : Inductive `ind_body` with ... with `ind_body`
+             : | CoInductive `ind_body` with ... with `ind_body`
+   ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ]
+   constructor : `ident` [ `binders` ] [:[>] `term` ]
 
 Especially, if the extra ``>`` is present in a constructor
 declaration, this constructor is declared as a coercion.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index e153c7cbe2..429dcbee69 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -181,7 +181,7 @@ Program Definition
 Program Fixpoint
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term
+.. cmd:: Program Fixpoint @ident @binders {? {@order}} : @type := @term
 
    The optional order annotation follows the grammar: