17 files changed, 179 insertions, 55 deletions
diff --git a/doc/changelog/02-specification-language/13911-master.rst b/doc/changelog/02-specification-language/13911-master.rst
new file mode 100644
index 0000000000..a0b37dd2d9
--- /dev/null
+++ b/doc/changelog/02-specification-language/13911-master.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  The little used `:>` type cast, which was only interpreted in Program-mode
+  (`#13911 <https://github.com/coq/coq/pull/13911>`_,
+  by Jim Fehrle and Théo Zimmermann).
diff --git a/doc/changelog/04-tactics/14089-ltac2_unify.rst b/doc/changelog/04-tactics/14089-ltac2_unify.rst
new file mode 100644
index 0000000000..5887781db9
--- /dev/null
+++ b/doc/changelog/04-tactics/14089-ltac2_unify.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Ltac2 now has a `unify` tactic
+  (`#14089 <https://github.com/coq/coq/pull/14089>`_,
+  fixes `#14083 <https://github.com/coq/coq/issues/14083>`_,
+  by Samuel Gruetter).
diff --git a/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst b/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst
new file mode 100644
index 0000000000..41bc3329c1
--- /dev/null
+++ b/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Ltac2 notations now correctly take into account their assigned level
+  (`#14094 <https://github.com/coq/coq/pull/14094>`_,
+  fixes `#11866 <https://github.com/coq/coq/issues/11866>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index abb08d98cc..e262a9305d 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -267,6 +267,11 @@ code span.error {
     color: inherit !important;
 }
 
+
+.coqdoc-comment {
+    color: #808080 !important
+}
+
 /* make the error message index readable */
 .indextable code {
     white-space: inherit;  /* break long lines */
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index d718454364..24e35dd85a 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -295,7 +295,7 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands.
    The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``.
 
-.. cmd:: Add Zify @add_zify @one_term
+.. cmd:: Add Zify @add_zify @qualid
 
    .. insertprodn add_zify add_zify
 
@@ -304,6 +304,9 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
       | {| PropOp | PropBinOp | PropUOp | Saturate }
 
    Registers an instance of the specified typeclass.
+   The typeclass type (e.g. :g:`BinOp Z.mul` or :g:`BinRel (@eq Z)`) has the additional constraint that
+   the non-implicit argument (here, :g:`Z.mul` or :g:`(@eq Z)`)
+   is either a :n:`@reference` (here, :g:`Z.mul`) or the application of a :n:`@reference` (here, :g:`@eq`) to a sequence of :n:`@one_term`.
 
 .. cmd:: Show Zify @show_zify
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index a011c81f15..52e47b52ae 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -135,17 +135,6 @@ use the :g:`dec` combinator to get the correct hypotheses as in:
 The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not
 produce an equality, contrary to the let pattern construct
 :g:`let '(x1,..., xn) := t in b`.
-Also, :g:`term :>` explicitly asks the system to
-coerce term to its support type. It can be useful in notations, for
-example:
-
-.. coqtop:: all
-
-   Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing).
-
-This notation denotes equality on subset types using equality on their
-support types, avoiding uses of proof-irrelevance that would come up
-when reasoning with equality on the subset types themselves.
 
 The next two commands are similar to their standard counterparts
 :cmd:`Definition` and :cmd:`Fixpoint`
diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst
index 06b6c61ea9..e53e6ea1cb 100644
--- a/doc/sphinx/language/core/conversion.rst
+++ b/doc/sphinx/language/core/conversion.rst
@@ -4,10 +4,80 @@ Conversion rules
 ----------------
 
 Coq has conversion rules that can be used to determine if two
-terms are equal by definition, or :term:`convertible`.
+terms are equal by definition in |CiC|, or :term:`convertible`.
 Conversion rules consist of reduction rules and expansion rules.
-See :ref:`applyingconversionrules`,
-which describes tactics that apply these conversion rules.
+Equality is determined by
+converting both terms to a normal form, then verifying they are syntactically
+equal (ignoring differences in the names of bound variables by
+:term:`alpha-conversion <alpha-convertible>`).
+
+.. seealso:: :ref:`applyingconversionrules`, which describes tactics that apply these conversion rules.
+
+:gdef:`Reductions <reduction>` convert terms to something that is incrementally
+closer to its normal form.  For example, :term:`zeta-reduction` removes
+:n:`let @ident := @term__1 in @term__2` constructs from a term by replacing
+:n:`@ident` with :n:`@term__1` wherever :n:`@ident` appears in :n:`@term__2`.
+The resulting term may be longer or shorter than the original.
+
+.. coqtop:: all
+
+   Eval cbv zeta in let i := 1 in i + i.
+
+:gdef:`Expansions <expansion>` are reductions applied in the opposite direction,
+for example expanding `2 + 2` to `let i := 2 in i + i`.  While applying
+reductions gives a unique result, the associated
+expansion may not be unique.  For example, `2 + 2` could also be
+expanded to `let i := 2 in i + 2`.  Reductions that have a unique inverse
+expansion are also referred to as :gdef:`contractions <contraction>`.
+
+The normal form is defined as the result of applying a particular
+set of conversion rules (beta-, delta-, iota- and zeta-reduction and eta-expansion)
+repeatedly until it's no longer possible to apply any of them.
+
+Sometimes the result of a reduction tactic will be a simple value, for example reducing
+`2*3+4` with `cbv beta delta iota` to `10`, which requires applying several
+reduction rules repeatedly.  In other cases, it may yield an expression containing
+variables, axioms or opaque contants that can't be reduced.
+
+The useful conversion rules are shown below.  All of them except for eta-expansion
+can be applied with conversion tactics such as :tacn:`cbv`:
+
+   .. list-table::
+      :header-rows: 1
+
+      * - Conversion name
+        - Description
+
+      * - beta-reduction
+        - eliminates `fun`
+
+      * - delta-reduction
+        - replaces a defined variable or constant with its definition
+
+      * - zeta-reduction
+        - eliminates `let`
+
+      * - eta-expansion
+        - replaces a term `f` of type `forall a : A, B` with `fun x : A => f x`
+
+      * - match-reduction
+        - eliminates `match`
+
+      * - fix-reduction
+        - replaces a `fix` with a :term:`beta-redex`;
+          recursive calls to the symbol are replaced with the `fix` term
+
+      * - cofix-reduction
+        - replaces a `cofix` with a :term:`beta-redex`;
+          recursive calls to the symbol are replaced with the `cofix` term
+
+      * - iota-reduction
+        - match-, fix- and cofix-reduction together
+
+:ref:`applyingconversionrules`
+describes tactics that only apply conversion rules.
+(Other tactics may use conversion rules in addition
+to other changes to the proof state.)
 
 α-conversion
 ~~~~~~~~~~~~
@@ -123,7 +193,7 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`.
    .. math::
       λ x:T.~(t~x)~\not\triangleright_η~t
 
-   This is because, in general, the type of :math:`t` need not to be convertible
+   This is because, in general, the type of :math:`t` need not be convertible
    to the type of :math:`λ x:T.~(t~x)`. E.g., if we take :math:`f` such that:
 
    .. math::
@@ -142,6 +212,30 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`.
    because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be
    convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`.
 
+Examples
+~~~~~~~~
+
+   .. example:: Simple delta, fix, beta and match reductions
+
+      ``+`` is a :ref:`notation <Notations>` for ``Nat.add``, which is defined
+      with a :cmd:`Fixpoint`.
+
+      .. coqtop:: all abort
+
+         Print Nat.add.
+         Goal 1 + 1 = 2.
+         cbv delta.
+         cbv fix.
+         cbv beta.
+         cbv match.
+
+      The term can be fully reduced with `cbv`:
+
+      .. coqtop:: all abort
+
+         Goal 1 + 1 = 2.
+         cbv.
+
 .. _proof-irrelevance:
 
 Proof Irrelevance
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index fcf61a5bf4..1a729ced4e 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -42,7 +42,6 @@ Type cast
    term_cast ::= @term10 : @type
    | @term10 <: @type
    | @term10 <<: @type
-   | @term10 :>
 
 The expression :n:`@term10 : @type` is a type cast expression. It enforces
 the type of :n:`@term10` to be :n:`@type`.
@@ -53,9 +52,6 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`vm_compute`).
 :n:`@term10 <<: @type` specifies that compilation to OCaml will be used
 to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`).
 
-:n:`@term10 :>` casts to the support type in Program mode.
-See :ref:`syntactic_control`.
-
 .. _gallina-definitions:
 
 Top-level definitions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 25ac72069b..52cf565998 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1251,6 +1251,10 @@ Notations
 
    This command supports the :attr:`deprecated` attribute.
 
+   .. exn:: Notation levels must range between 0 and 6.
+
+      The level of a notation must be an integer between 0 and 6 inclusive.
+
 Abbreviations
 ~~~~~~~~~~~~~
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index bab9d35099..d4749f781a 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -609,7 +609,7 @@ Abbreviations
 
    |SSR| extends the :tacn:`set` tactic by supplying:
 
-   + an open syntax, similarly to the :tacn:`pose (ssreflect)` tactic;
+   + an open syntax, similarly to the :tacn:`pose <pose (ssreflect)>` tactic;
    + a more aggressive matching algorithm;
    + an improved interpretation of wildcards, taking advantage of the
      matching algorithm;
@@ -899,7 +899,7 @@ context of a goal thanks to the ``in`` tactical.
 
 .. tacv:: set @ident := @term in {+ @ident}
 
-   This variant of :tacn:`set (ssreflect)` introduces a defined constant
+   This variant of :tacn:`set <set (ssreflect)>` introduces a defined constant
    called :token:`ident` in the context, and folds it in
    the context entries mentioned on the right hand side of ``in``.
    The body of :token:`ident` is the first subterm matching these context
@@ -1202,7 +1202,7 @@ The move tactic.
          Goal not False.
          move.
 
-   More precisely, the :tacn:`move` tactic inspects the goal and does nothing
+   More precisely, the :tacn:`move <move (ssreflect)>` tactic inspects the goal and does nothing
    (:tacn:`idtac`) if an introduction step is possible, i.e. if the goal is a
    product or a ``let … in``, and performs :tacn:`hnf` otherwise.
 
@@ -1301,7 +1301,7 @@ The apply tactic
    this use of the :tacn:`refine` tactic implies that the tactic tries to match
    the goal up to expansion of constants and evaluation of subterms.
 
-:tacn:`apply (ssreflect)` has a special behavior on goals containing
+:tacn:`apply <apply (ssreflect)>` has a special behavior on goals containing
 existential metavariables of sort :g:`Prop`.
 
 .. example::
@@ -2461,7 +2461,7 @@ The have tactic.
    redex, and introduces the lemma under a fresh name, automatically
    chosen.
 
-Like in the case of the :n:`pose (ssreflect)` tactic (see section :ref:`definitions_ssr`), the types of
+Like in the case of the :n:`pose <pose (ssreflect)>` tactic (see section :ref:`definitions_ssr`), the types of
 the holes are abstracted in term.
 
 .. example::
@@ -3775,7 +3775,7 @@ involves the following steps:
    ``forall n, F1 n = F2 n`` for ``eq_map``).
 
 3. If so :tacn:`under` puts these n goals in head normal form (using
-   the defective form of the tactic :tacn:`move`), then executes
+   the defective form of the tactic :tacn:`move <move (ssreflect)>`), then executes
    the corresponding intro pattern :n:`@i_pattern__i` in each goal.
 
 4. Then :tacn:`under` checks that the first n subgoals
@@ -5665,6 +5665,7 @@ Tactics
 respectively.
 
 .. tacn:: move
+   :name: move (ssreflect)
 
    :tacn:`idtac` or :tacn:`hnf` (see  :ref:`bookkeeping_ssr`)
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index fad02b2645..7bc009fcfe 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1148,7 +1148,7 @@ Managing the local context
       or at the bottom of the local context. All hypotheses on which the new
       hypothesis depends are moved too so as to respect the order of
       dependencies between hypotheses. It is equivalent to :n:`intro {? @ident__1 }`
-      followed by the appropriate call to :tacn:`move … after …`,
+      followed by the appropriate call to :tacn:`move`,
       :tacn:`move … before …`, :tacn:`move … at top`,
       or :tacn:`move … at bottom`.
 
@@ -1235,7 +1235,6 @@ Managing the local context
       hypotheses that depend on it.
 
 .. tacn:: move @ident__1 after @ident__2
-   :name: move … after …
 
    This moves the hypothesis named :n:`@ident__1` in the local context after
    the hypothesis named :n:`@ident__2`, where “after” is in reference to the
@@ -1256,7 +1255,7 @@ Managing the local context
       :name: move … before …
 
       This moves :n:`@ident__1` towards and just before the hypothesis
-      named :n:`@ident__2`.  As for :tacn:`move … after …`, dependencies
+      named :n:`@ident__2`.  As for :tacn:`move`, dependencies
       over :n:`@ident__1` (when :n:`@ident__1` comes before :n:`@ident__2` in
       the order of dependencies) or in the type of :n:`@ident__1`
       (when :n:`@ident__1` comes after :n:`@ident__2` in the order of
@@ -2502,7 +2501,7 @@ and an explanation of the underlying technique.
    :name: inversion ... using ...
 
    .. todo using … instead of ... in the name above gives a Sphinx error, even though
-      this works just find for :tacn:`move … after …`
+      this works just find for :tacn:`move`
 
    Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the
    local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this
diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst
index 32d3e87e68..dd1d6051b5 100644
--- a/doc/sphinx/refman-preamble.rst
+++ b/doc/sphinx/refman-preamble.rst
@@ -15,7 +15,7 @@
 .. |c_i| replace:: `c`\ :math:`_{i}`
 .. |c_n| replace:: `c`\ :math:`_{n}`
 .. |Cic| replace:: CIC
-.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}`
+.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{βδιζ}`
 .. |Latex| replace:: :smallcaps:`LaTeX`
 .. |Ltac| replace:: `L`:sub:`tac`
 .. |p_1| replace:: `p`\ :math:`_{1}`
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
index 522b9900a5..51e26a9082 100644
--- a/doc/tools/coqrst/coqdoc/main.py
+++ b/doc/tools/coqrst/coqdoc/main.py
@@ -28,7 +28,7 @@ from bs4 import BeautifulSoup
 from bs4.element import NavigableString
 
 COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals',
-                  '-s', '--html', '--stdout', '--utf8']
+                  '-s', '--html', '--stdout', '--utf8', '--parse-comments']
 
 COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"]
 COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS)
@@ -68,8 +68,19 @@ def lex(source):
         if isinstance(elem, NavigableString):
             yield [], elem
         elif elem.name == "span":
-            cls = "coqdoc-{}".format(elem['title'])
-            yield [cls], elem.string
+            if elem.string:
+                cls = "coqdoc-{}".format(elem.get("title", "comment"))
+                yield [cls], elem.string
+            else:
+                # handle multi-line comments
+                children = list(elem.children)
+                mlc = children[0].startswith("(*") and children[-1].endswith ("*)")
+                for elem2 in children:
+                    if isinstance(elem2, NavigableString):
+                        cls = ["coqdoc-comment"] if mlc else []
+                        yield cls, elem2
+                    elif elem2.name == 'br':
+                        pass
         elif elem.name == 'br':
             pass
         else:
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 1428dae7ef..468b6b648d 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -938,10 +938,11 @@ class CoqtopBlocksTransform(Transform):
 
     @staticmethod
     def split_lines(source):
-        r"""Split Coq input in chunks
+        r"""Split Coq input into chunks, which may include single- or
+        multi-line comments.  Nested comments are not supported.
 
         A chunk is a minimal sequence of consecutive lines of the input that
-        ends with a '.'
+        ends with a '.' or '*)'
 
         >>> split_lines('A.\nB.''')
         ['A.', 'B.']
@@ -962,8 +963,14 @@ class CoqtopBlocksTransform(Transform):
 
         >>> split_lines('SearchHead le.\nSearchHead (@eq bool).')
         ['SearchHead le.', 'SearchHead (@eq bool).']
+
+        >>> split_lines("(* *) x. (* *)\ny.\n")
+        ['(* *) x. (* *)', 'y.']
+
+        >>> split_lines("(* *) x (* \n *)\ny.\n")
+        ['(* *) x (* \n *)', 'y.']
         """
-        return re.split(r"(?<=(?<!\.)\.)\n", source.strip())
+        return re.split(r"(?:(?<=(?<!\.)\.)|(?<=\*\)))\n", source.strip())
 
     @staticmethod
     def parse_options(node):
@@ -1039,7 +1046,11 @@ class CoqtopBlocksTransform(Transform):
         if options['warn']:
             repl.sendone('Set Warnings "default".')
         for sentence in self.split_lines(node.rawsource):
-            pairs.append((sentence, repl.sendone(sentence)))
+            comment = re.compile(r"\s*\(\*.*?\*\)\s*", re.DOTALL)
+            wo_comments = re.sub(comment, "", sentence)
+            has_tac = wo_comments != "" and not wo_comments.isspace()
+            output = repl.sendone(sentence) if has_tac else ""
+            pairs.append((sentence, output))
         if options['abort']:
             repl.sendone('Abort All.')
         if options['fail']:
@@ -1052,9 +1063,10 @@ class CoqtopBlocksTransform(Transform):
             # Use Coqdoc to highlight input
             in_chunks = highlight_using_coqdoc(sentence)
             dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(options['input']))
-            # Parse ANSI sequences to highlight output
-            out_chunks = AnsiColorsParser().colorize_str(output)
-            dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output))
+            if output:
+                # Parse ANSI sequences to highlight output
+                out_chunks = AnsiColorsParser().colorize_str(output)
+                dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output))
         node.clear()
         node.rawsource = self.make_rawsource(pairs, options['input'], options['output'])
         node['classes'].extend(self.block_classes(options['input'] or options['output']))
@@ -1180,8 +1192,7 @@ class StdGlossaryIndex(Index):
             if type == 'term':
                 entries = content[itemname[0].lower()]
                 entries.append([itemname, 0, docname, anchor, '', '', ''])
-        content = sorted(content.items())
-        return content, False
+        return content.items(), False
 
 def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
     """A grammar production not included in a ``prodn`` directive.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index fd1c3c0260..5c211d82e9 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -365,7 +365,6 @@ term100: [
 | REPLACE term99 ":" term200
 | WITH term99 ":" type
 | MOVETO term_cast term99 ":" type
-| MOVETO term_cast term99 ":>"
 ]
 
 constr: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 0c8980b1bd..fe166524bf 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1,6 +1,15 @@
 (* Coq grammar generated from .mlg files.  Do not edit by hand.  Not compiled into Coq *)
 DOC_GRAMMAR
 
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "BackTo" natural "."
+| test_show_goal "Show" "Goal" natural "at" natural "."
+| "Show" "Proof" "Diffs" OPT "removed" "."
+| Pvernac.Vernac_.main_entry
+]
+
 Constr.ident: [
 | Prim.ident
 ]
@@ -75,7 +84,6 @@ term100: [
 | term99 "<:" term200
 | term99 "<<:" term200
 | term99 ":" term200
-| term99 ":>"
 | term99
 ]
 
@@ -478,15 +486,6 @@ strategy_level: [
 | "transparent"
 ]
 
-vernac_toplevel: [
-| "Drop" "."
-| "Quit" "."
-| "BackTo" natural "."
-| test_show_goal "Show" "Goal" natural "at" natural "."
-| "Show" "Proof" "Diffs" OPT "removed" "."
-| Pvernac.Vernac_.main_entry
-]
-
 opt_hintbases: [
 |
 | ":" LIST1 IDENT
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 40bb980e90..2b09263cc4 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -553,7 +553,6 @@ term_cast: [
 | term10 ":" type
 | term10 "<:" type
 | term10 "<<:" type
-| term10 ":>"
 ]
 
 term_match: [