Merge remote-tracking branch 'origin/master' into stm+doc_hook

57 files changed, 3287 insertions, 861 deletions

diff --git a/doc/changelog/00-title.rst b/doc/changelog/00-title.rst
new file mode 100644
index 0000000000..628d9c8578
--- /dev/null
+++ b/doc/changelog/00-title.rst
@@ -0,0 +1,2 @@
+Unreleased changes
+------------------
diff --git a/doc/changelog/01-kernel/00000-title.rst b/doc/changelog/01-kernel/00000-title.rst
new file mode 100644
index 0000000000..f680628a05
--- /dev/null
+++ b/doc/changelog/01-kernel/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Kernel**
+
diff --git a/doc/changelog/02-specification-language/00000-title.rst b/doc/changelog/02-specification-language/00000-title.rst
new file mode 100644
index 0000000000..99bd2c5b44
--- /dev/null
+++ b/doc/changelog/02-specification-language/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Specification language, type inference**
+
diff --git a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
new file mode 100644
index 0000000000..0a902079b9
--- /dev/null
+++ b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
@@ -0,0 +1,4 @@
+- Record fields can be annotated to prevent them from being used as canonical projections;
+  see :ref:`canonicalstructures` for details
+  (`#10076 <https://github.com/coq/coq/pull/10076>`_,
+  by Vincent Laporte).
diff --git a/doc/changelog/03-notations/00000-title.rst b/doc/changelog/03-notations/00000-title.rst
new file mode 100644
index 0000000000..abc532df11
--- /dev/null
+++ b/doc/changelog/03-notations/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Notations**
+
diff --git a/doc/changelog/04-tactics/00000-title.rst b/doc/changelog/04-tactics/00000-title.rst
new file mode 100644
index 0000000000..3c7802d632
--- /dev/null
+++ b/doc/changelog/04-tactics/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Tactics**
+
diff --git a/doc/changelog/05-tactic-language/00000-title.rst b/doc/changelog/05-tactic-language/00000-title.rst
new file mode 100644
index 0000000000..b34d190298
--- /dev/null
+++ b/doc/changelog/05-tactic-language/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Tactic language**
+
diff --git a/doc/changelog/06-ssreflect/00000-title.rst b/doc/changelog/06-ssreflect/00000-title.rst
new file mode 100644
index 0000000000..2e724627ec
--- /dev/null
+++ b/doc/changelog/06-ssreflect/00000-title.rst
@@ -0,0 +1,3 @@
+
+**SSReflect**
+
diff --git a/doc/changelog/07-commands-and-options/00000-title.rst b/doc/changelog/07-commands-and-options/00000-title.rst
new file mode 100644
index 0000000000..1a0272983e
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Commands and options**
+
diff --git a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst
new file mode 100644
index 0000000000..78874cadb1
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst
@@ -0,0 +1,6 @@
+- Deprecated flag `Refine Instance Mode` has been removed.
+  (`#09530 <https://github.com/coq/coq/pull/09530>`_, fixes
+  `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890
+  <https://github.com/coq/coq/issues/3890>`_ and `#4638
+  <https://github.com/coq/coq/issues/4638>`_
+  by Maxime Dénès, review by Gaëtan Gilbert).
diff --git a/doc/changelog/08-tools/00000-title.rst b/doc/changelog/08-tools/00000-title.rst
new file mode 100644
index 0000000000..bf462744fb
--- /dev/null
+++ b/doc/changelog/08-tools/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Tools**
+
diff --git a/doc/changelog/09-coqide/00000-title.rst b/doc/changelog/09-coqide/00000-title.rst
new file mode 100644
index 0000000000..0fc27cf380
--- /dev/null
+++ b/doc/changelog/09-coqide/00000-title.rst
@@ -0,0 +1,3 @@
+
+**CoqIDE**
+
diff --git a/doc/changelog/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst
new file mode 100644
index 0000000000..d517a0e709
--- /dev/null
+++ b/doc/changelog/10-standard-library/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Standard library**
+
diff --git a/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst
new file mode 100644
index 0000000000..6b301f59d3
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Infrastructure and dependencies**
+
diff --git a/doc/changelog/12-misc/00000-title.rst b/doc/changelog/12-misc/00000-title.rst
new file mode 100644
index 0000000000..5e709e2b27
--- /dev/null
+++ b/doc/changelog/12-misc/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Miscellaneous**
+
diff --git a/doc/changelog/README.md b/doc/changelog/README.md
new file mode 100644
index 0000000000..2891eb207e
--- /dev/null
+++ b/doc/changelog/README.md
@@ -0,0 +1,41 @@
+# Unreleased changelog #
+
+## When to add an entry? ##
+
+All new features, user-visible changes to features, user-visible or
+otherwise important infrastructure changes, and important bug fixes
+should get a changelog entry.
+
+Compatibility-breaking changes should always get a changelog entry,
+which should explain what compatibility-breakage is to expect.
+
+Pull requests changing the ML API in significant ways should add an
+entry in [`dev/doc/changes.md`](../../dev/doc/changes.md).
+
+## How to add an entry? ##
+
+You should create a file in one of the sub-directories. The name of
+the file should be `NNNNN-identifier.rst` where `NNNNN` is the number
+of the pull request on five digits and `identifier` is whatever you
+want.
+
+This file should use the same format as the reference manual (as it
+will be copied in there). You may reference the documentation you just
+added with `:ref:`, `:tacn:`, `:cmd:`, `:opt:`, `:token:`, etc. See
+the [documentation of the Sphinx format](../sphinx/README.rst) of the
+manual for details.
+
+The entry should be written using the following structure:
+
+``` rst
+- Description of the changes, with possible link to
+  :ref:`relevant-section` of the updated documentation
+  (`#PRNUM <https://github.com/coq/coq/pull/PRNUM>`_,
+  [fixes `#ISSUE1 <https://github.com/coq/coq/issues/ISSUE1>`_
+  [ and `#ISSUE2 <https://github.com/coq/coq/issues/ISSUE2>`_],]
+  by Full Name[, with help / review of Full Name]).
+```
+
+The description should be kept rather short and the only additional
+required meta-information are the link to the pull request and the
+full name of the author.
diff --git a/doc/dune b/doc/dune
index bd40104725..3a8efbb36d 100644
--- a/doc/dune
+++ b/doc/dune
@@ -11,6 +11,7 @@
   (package coq)
   (source_tree sphinx)
   (source_tree tools)
+  unreleased.rst
   (env_var SPHINXWARNOPT))
  (action
   (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html)))
@@ -19,6 +20,11 @@
  (name refman-html)
  (deps sphinx_build))
 
+(rule
+ (targets unreleased.rst)
+ (deps (source_tree changelog))
+ (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst"))))
+
 ; The install target still needs more work.
 ; (install
 ;  (section doc)
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 23f8fbe888..e9b91d5a7e 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,25 +1,16 @@
-(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
-let edeclare ?hook ~ontop ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
-  let sigma = Evd.minimize_universes sigma in
-  let body = EConstr.to_constr sigma body in
-  let tyopt = Option.map (EConstr.to_constr sigma) tyopt in
-  let uvars_fold uvars c =
-    Univ.LSet.union uvars (Vars.universes_of_constr c) in
-  let uvars = List.fold_left uvars_fold Univ.LSet.empty
-     (Option.List.cons tyopt [body]) in
-  let sigma = Evd.restrict_universe_context sigma uvars in
-  let univs = Evd.check_univ_decl ~poly sigma udecl in
+let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
+  let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
+      ~opaque ~poly sigma udecl ~types:tyopt ~body in
   let uctx = Evd.evar_universe_context sigma in
   let ubinders = Evd.universe_binders sigma in
-  let ce = Declare.definition_entry ?types:tyopt ~univs body in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ~ontop ident k ce ubinders imps ?hook_data
+  DeclareDef.declare_definition ident k ce ubinders imps ?hook_data
 
 let packed_declare_definition ~poly ident value_with_constraints =
   let body, ctx = value_with_constraints in
   let sigma = Evd.from_ctx ctx in
   let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in
   let udecl = UState.default_univ_decl in
-  ignore (edeclare ~ontop:None ident k ~opaque:false sigma udecl body None [])
+  ignore (edeclare ident k ~opaque:false sigma udecl body None [])
 
 (* But this definition cannot be undone by Reset ident *)
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 881f7a310d..b20669c7f1 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat
 ``{*, …}``, ``{+, …}``
   an optional or mandatory repeatable block, with repetitions separated by commas
 
-``%|``, ``%{``, …
-  an escaped character (rendered without the leading ``%``)
+``{| … | … | … }``
+  an alternative, indicating than one of multiple constructs can be used
+
+``%{``, ``%}``, ``%|``
+  an escaped character (rendered without the leading ``%``).  In most cases, escaping is not necessary.  In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``.  But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``.  (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.)
 
 ..
    FIXME document the new subscript support
@@ -148,7 +151,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
     Example::
 
         .. prodn:: term += let: @pattern := @term in @term
-        .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+        .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
 
 ``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values.
     Example::
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 78803a927f..2093765608 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat
 ``{*, …}``, ``{+, …}``
   an optional or mandatory repeatable block, with repetitions separated by commas
 
-``%|``, ``%{``, …
-  an escaped character (rendered without the leading ``%``)
+``{| … | … | … }``
+  an alternative, indicating than one of multiple constructs can be used
+
+``%{``, ``%}``, ``%|``
+  an escaped character (rendered without the leading ``%``).  In most cases, escaping is not necessary.  In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``.  But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``.  (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.)
 
 ..
    FIXME document the new subscript support
diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty
index 75eac1f724..3548b8754c 100644
--- a/doc/sphinx/_static/coqnotations.sty
+++ b/doc/sphinx/_static/coqnotations.sty
@@ -18,6 +18,9 @@
 \newlength{\nscriptsize}
 \setlength{\nscriptsize}{0.8em}
 
+\newlength{\nboxsep}
+\setlength{\nboxsep}{2pt}
+
 \newcommand*{\scriptsmallsquarebox}[1]{%
   % Force width
   \makebox[\nscriptsize]{%
@@ -31,7 +34,8 @@
 \newcommand*{\nsup}[1]{^{\nscript{0.15}{#1}}}
 \newcommand*{\nsub}[1]{_{\nscript{0.35}{#1}}}
 \newcommand*{\nnotation}[1]{#1}
-\newcommand*{\nrepeat}[1]{\text{\adjustbox{cfbox=nbordercolor 0.5pt 2pt,bgcolor=nbgcolor}{#1\hspace{.5\nscriptsize}}}}
+\newcommand*{\nbox}[1]{\adjustbox{cfbox=nbordercolor 0.5pt \nboxsep,bgcolor=nbgcolor}{#1}}
+\newcommand*{\nrepeat}[1]{\text{\nbox{#1\hspace{.5\nscriptsize}}}}
 \newcommand*{\nwrapper}[1]{\ensuremath{\displaystyle#1}} % https://tex.stackexchange.com/questions/310877/
 \newcommand*{\nhole}[1]{\textit{\color{nholecolor}#1}}
 
@@ -42,9 +46,32 @@
 }
 % </magic>
 
+% https://tex.stackexchange.com/questions/490262/
+\def\naltsep{}
+\newsavebox{\nsavedalt}
+\newlength{\naltvruleht}
+\newlength{\naltvruledp}
+\def\naltvrule{\smash{\vrule height\naltvruleht depth\naltvruledp}}
+\newcommand{\nalternative}[2]{%
+  % First measure the contents of the box without the bar
+  \bgroup%
+  \def\naltsep{}%
+  \savebox{\nsavedalt}{#1}%
+  \setlength{\naltvruleht}{\ht\nsavedalt}%
+  \setlength{\naltvruledp}{\dp\nsavedalt}%
+  \addtolength{\naltvruleht}{#2}%
+  \addtolength{\naltvruledp}{#2}%
+  % Then redraw it with the bar
+  \def\naltsep{\naltvrule}%
+  #1\egroup}
+
 \newcssclass{notation-sup}{\nsup{#1}}
 \newcssclass{notation-sub}{\nsub{#1}}
 \newcssclass{notation}{\nnotation{#1}}
 \newcssclass{repeat}{\nrepeat{#1}}
 \newcssclass{repeat-wrapper}{\nwrapper{#1}}
 \newcssclass{hole}{\nhole{#1}}
+\newcssclass{alternative}{\nalternative{\nbox{#1}}{0pt}}
+\newcssclass{alternative-block}{#1}
+\newcssclass{repeated-alternative}{\nalternative{#1}{\nboxsep}}
+\newcssclass{alternative-separator}{\quad\naltsep{}\quad}
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index dcb47d1786..8322ab0137 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -45,15 +45,46 @@
     width: 2.2em;
 }
 
-.notation .repeat {
+.notation .repeat, .notation .alternative {
     background: #EAEAEA;
     border: 1px solid #AAA;
     display: inline-block;
-    padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */
-    padding-left: 0.2em;
+    padding: 0 0.2em 0 0.3em;
     margin: 0.25em 0;
 }
 
+.notation .repeated-alternative {
+    display: inline-table;
+}
+
+.notation .alternative {
+    display: inline-table;
+    padding: 0 0.2em;
+}
+
+.notation .alternative-block {
+    display: table-cell;
+    padding: 0 0.5em;
+}
+
+.notation .alternative-separator {
+    border-left: 1px solid black; /* Display a thin bar */
+    display: table-cell;
+    width: 0;
+}
+
+.alternative-block:first-child {
+  padding-left: 0;
+}
+
+.alternative-block:last-child {
+  padding-right: 0;
+}
+
+.notation .repeat {
+    padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */
+}
+
 .notation .repeat-wrapper {
     display: inline-block;
     position: relative;
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index dd21ea09bd..b593b0cef1 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -209,7 +209,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``.
                         LE_class : LE.class T;
                         extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
 
-    Structure type := _Pack { obj : Type; class_of : class obj }.
+    Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }.
 
     Arguments Mixin {e le} _.
 
@@ -219,6 +219,9 @@ The mixin component of the ``LEQ`` class contains all the extra content we
 are adding to ``EQ`` and ``LE``. In particular it contains the requirement
 that the two relations we are combining are compatible.
 
+The `class_of` projection of the `type` structure is annotated as *not canonical*;
+it plays no role in the search for instances.
+
 Unfortunately there is still an obstacle to developing the algebraic
 theory of this new class.
 
@@ -313,9 +316,7 @@ constructor ``*``. It also tests that they work as expected.
 Unfortunately, these declarations are very verbose. In the following
 subsection we show how to make them more compact.
 
-.. FIXME shouldn't warn
-
-.. coqtop:: all warn
+.. coqtop:: all
 
   Module Add_instance_attempt.
 
@@ -420,9 +421,7 @@ the reader can refer to :cite:`CSwcu`.
 
 The declaration of canonical instances can now be way more compact:
 
-.. FIXME should not warn
-
-.. coqtop:: all warn
+.. coqtop:: all
 
   Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
   
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index e93b01f14d..8a895eb515 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -99,7 +99,7 @@ Extraction Options
 Setting the target language
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Extraction Language ( OCaml | Haskell | Scheme )
+.. cmd:: Extraction Language {| OCaml | Haskell | Scheme }
    :name: Extraction Language
 
    The ability to fix target language is the first and more important
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index b474c51f17..847abb33fc 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -170,12 +170,12 @@ compatibility constraints.
 Adding new relations and morphisms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd::  Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident
+.. cmd::  Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident
 
    This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`,
    :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`.
 
-   The :token:`ident` gives a unique name to the morphism and it is used
+   The final :token:`ident` gives a unique name to the morphism and it is used
    by the command to generate fresh names for automatically provided
    lemmas used internally.
 
@@ -219,15 +219,16 @@ replace terms with related ones only in contexts that are syntactic
 compositions of parametric morphism instances declared with the
 following command.
 
-.. cmd:: Add Parametric Morphism (x1 : T1) ... (xk : Tk) : (f t1 ... tn) with signature sig as @ident
+.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident
 
-   This command declares ``f`` as a parametric morphism of signature ``sig``. The
-   identifier :token:`ident` gives a unique name to the morphism and it is used as
-   the base name of the typeclass instance definition and as the name of
-   the lemma that proves the well-definedness of the morphism. The
-   parameters of the morphism as well as the signature may refer to the
-   context of variables. The command asks the user to prove interactively
-   that ``f`` respects the relations identified from the signature.
+   This command declares a parametric morphism :n:`@ident {+ @term__1}` of
+   signature :n:`@term__2`.  The final identifier :token:`ident` gives a unique
+   name to the morphism and it is used as the base name of the typeclass
+   instance definition and as the name of the lemma that proves the
+   well-definedness of the morphism. The parameters of the morphism as well as
+   the signature may refer to the context of variables. The command asks the
+   user to prove interactively that the function denoted by the first
+   :token:`ident` respects the relations identified from the signature.
 
 .. example::
 
@@ -577,7 +578,7 @@ Deprecated syntax and backward incompatibilities
    Notice that the syntax is not completely backward compatible since the
    identifier was not required.
 
-.. cmd:: Add Morphism f : @ident
+.. cmd:: Add Morphism @ident : @ident
    :name: Add Morphism
 
    This command is restricted to the declaration of morphisms
@@ -809,7 +810,7 @@ Usage
 ~~~~~
 
 
-.. tacn:: rewrite_strat @s [in @ident]
+.. tacn:: rewrite_strat @s {? in @ident }
    :name: rewrite_strat
 
    Rewrite using the strategy s in hypothesis ident or the conclusion.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index b410833d25..22ddcae584 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -283,7 +283,7 @@ optional identifier is used when multiple functions have unsolved
 obligations (e.g. when defining mutually recursive blocks). The
 optional tactic is replaced by the default one if not specified.
 
-.. cmd:: {? Local|Global} Obligation Tactic := @tactic
+.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic
    :name: Obligation Tactic
 
    Sets the default obligation solving tactic applied to all obligations
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index c0c8c2d79c..8935ba27e3 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -10,9 +10,9 @@ SProp (proof irrelevant propositions)
 This section describes the extension of |Coq| with definitionally
 proof irrelevant propositions (types in the sort :math:`\SProp`, also
 known as strict propositions). To use :math:`\SProp` you must pass
-``-allow-sprop`` to the |Coq| program or use :opt:`Allow StrictProp`.
+``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`.
 
-.. opt:: Allow StrictProp
+.. flag:: Allow StrictProp
    :name: Allow StrictProp
 
    Allows using :math:`\SProp` when set and forbids it when unset. The
@@ -201,10 +201,10 @@ This means that some errors will be delayed until ``Qed``:
 
    Abort.
 
-.. opt:: Elaboration StrictProp Cumulativity
+.. flag:: Elaboration StrictProp Cumulativity
    :name: Elaboration StrictProp Cumulativity
 
-   Unset this option (it's on by default) to be strict with regard to
+   Unset this flag (it is on by default) to be strict with regard to
    :math:`\SProp` cumulativity during elaboration.
 
 The implementation of proof irrelevance uses inferred "relevance"
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index a5e9023732..65934efaa6 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -311,24 +311,24 @@ Summary of the commands
 
          This command has no effect when used on a typeclass.
 
-.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
+.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} }
 
    This command is used to declare a typeclass instance named
-   :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and
-   fields ``b1`` to ``bi``, where each field must be a declared field of
-   the class.  Missing fields must be filled in interactive proof mode.
+   :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and
+   fields defined by :token:`field_def`, where each field must be a declared field of
+   the class.
 
    An arbitrary context of :token:`binders` can be put after the name of the
    instance and before the colon to declare a parameterized instance. An
    optional priority can be declared, 0 being the highest priority as for
-   :tacn:`auto` hints. If the priority is not specified, it defaults to the number
+   :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number
    of non-dependent binders of the instance.
 
-   .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term
+   .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @term__0 {+ @term} {? | @num } := @term
 
       This syntax is used for declaration of singleton class instances or
-      for directly giving an explicit term of type :n:`forall @binders, @class
-      @term__1 … @term__n`.  One need not even mention the unique field name for
+      for directly giving an explicit term of type :n:`forall @binders, @term__0
+      {+ @term}`.  One need not even mention the unique field name for
       singleton classes.
 
    .. cmdv:: Global Instance
@@ -356,11 +356,11 @@ Summary of the commands
 Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
 few other commands related to typeclasses.
 
-.. cmd:: Existing Instance {+ @ident} [| priority]
+.. cmd:: Existing Instance {+ @ident} {? | @num}
 
    This command adds an arbitrary list of constants whose type ends with
    an applied typeclass to the instance database with an optional
-   priority.  It can be used for redeclaring instances at the end of
+   priority :token:`num`.  It can be used for redeclaring instances at the end of
    sections, or declaring structure projections as instances. This is
    equivalent to ``Hint Resolve ident : typeclass_instances``, except it
    registers instances for :cmd:`Print Instances`.
@@ -405,8 +405,10 @@ few other commands related to typeclasses.
      resolution with the local hypotheses use full conversion during
      unification.
 
+   + When considering local hypotheses, we use the union of all the modes
+     declared in the given databases.
 
-   .. cmdv:: typeclasses eauto @num
+   .. tacv:: typeclasses eauto @num
 
       .. warning::
          The semantics for the limit :n:`@num`
@@ -415,7 +417,7 @@ few other commands related to typeclasses.
          counted, which might result in larger limits being necessary when
          searching with ``typeclasses eauto`` than with :tacn:`auto`.
 
-   .. cmdv:: typeclasses eauto with {+ @ident}
+   .. tacv:: typeclasses eauto with {+ @ident}
 
       This variant runs resolution with the given hint databases. It treats
       typeclass subgoals the same as other subgoals (no shelving of
@@ -561,23 +563,10 @@ Settings
    of goals.  Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this
    option to 0 turns that option off.
 
-.. flag:: Refine Instance Mode
-
-   .. deprecated:: 8.10
-
-   This flag allows to switch the behavior of instance declarations made through
-   the Instance command.
-
-   + When it is off (the default), they fail with an error instead.
-
-   + When it is on, instances that have unsolved holes in
-     their proof-term silently open the proof mode with the remaining
-     obligations to prove.
-
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num
+.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num
    :name: Typeclasses eauto
 
    This command allows more global customization of the typeclass
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index 0467852b19..85b02013d8 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -551,3 +551,20 @@ the Calculus of Inductive Constructions}},
   biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11},
   bibsource = {dblp computer science bibliography, http://dblp.org}
 }
+
+@inproceedings{MilnerPrincipalTypeSchemes,
+ author = {Damas, Luis and Milner, Robin},
+ title = {Principal Type-schemes for Functional Programs},
+ booktitle = {Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ series = {POPL '82},
+ year = {1982},
+ isbn = {0-89791-065-6},
+ location = {Albuquerque, New Mexico},
+ pages = {207--212},
+ numpages = {6},
+ url = {http://doi.acm.org/10.1145/582153.582176},
+ doi = {10.1145/582153.582176},
+ acmid = {582176},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 57b9e45342..cc2c43e7dd 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -2,6 +2,600 @@
 Recent changes
 --------------
 
+.. ifconfig:: not coq_config.is_a_released_version
+
+   .. include:: ../unreleased.rst
+
+Version 8.10
+------------
+
+Summary of changes
+~~~~~~~~~~~~~~~~~~
+
+|Coq| version 8.10 contains two major new features: support for a native
+fixed-precision integer type and a new sort :math:`\SProp` of strict
+propositions. It is also the result of refinements and stabilization of
+previous features, deprecations or removals of deprecated features,
+cleanups of the internals of the system and API, and many documentation improvements.
+This release includes many user-visible changes, including deprecations that are
+documented in the next subsection, and new features that are documented in the
+reference manual. Here are the most important user-visible changes:
+
+- Kernel:
+
+  - A notion of primitive object was added to the calculus. Its first
+    instance is primitive cyclic unsigned integers, axiomatized in
+    module :g:`UInt63`. See Section :ref:`primitive-integers`.
+    The `Coq.Numbers.Cyclic.Int31` library is deprecated
+    (`#6914 <https://github.com/coq/coq/pull/6914>`_, by Maxime Dénès,
+    Benjamin Grégoire and Vincent Laporte,
+    with help and reviews from many others).
+
+  - The :math:`\SProp` sort of definitionally proof-irrelevant propositions was
+    introduced. :math:`\SProp` allows to mark proof
+    terms as irrelevant for conversion, and is treated like :math:`\Prop`
+    during extraction. It is enabled using the `-allow-sprop`
+    command-line flag or the :flag:`Allow StrictProp` flag.
+    See Chapter :ref:`sprop`
+    (`#8817 <https://github.com/coq/coq/pull/8817>`_, by Gaëtan Gilbert).
+
+  - The unfolding heuristic in termination checking was made more
+    complete, allowing more constants to be unfolded to discover valid
+    recursive calls.  Performance regression may occur in Fixpoint
+    declarations without an explicit ``{struct}`` annotation, since
+    guessing the decreasing argument can now be more expensive
+    (`#9602 <https://github.com/coq/coq/pull/9602>`_, by Enrico Tassi).
+
+- Universes:
+
+  - Added :cmd:`Print Universes Subgraph` variant of :cmd:`Print Universes`.
+    Try for instance
+    :g:`Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1).`
+    (`#8451 <https://github.com/coq/coq/pull/8451>`_, by Gaëtan Gilbert).
+
+  - Added private universes for opaque polymorphic constants, see the
+    documentation for the :flag:`Private Polymorphic Universes` flag,
+    and unset it to get the previous behaviour
+    (`#8850 <https://github.com/coq/coq/pull/8850>`_, by Gaëtan Gilbert).
+
+- Notations:
+
+  - New command :cmd:`String Notation` to register string syntax for custom
+    inductive types
+    (`#8965 <https://github.com/coq/coq/pull/8965>`_, by Jason Gross).
+
+  - Experimental: :ref:`Numeral Notations <numeral-notations>` now parse decimal
+    constants such as ``1.02e+01`` or ``10.2``. Parsers added for :g:`Q` and :g:`R`.
+    In the rare case when such numeral notations were used
+    in a development along with :g:`Q` or :g:`R`, they may have to be removed or
+    disambiguated through explicit scope annotations
+    (`#8764 <https://github.com/coq/coq/pull/8764>`_, by Pierre Roux).
+
+- Ltac backtraces can be turned on using the :flag:`Ltac Backtrace`
+  flag, which is off by default
+  (`#9142 <https://github.com/coq/coq/pull/9142>`_,
+  fixes `#7769 <https://github.com/coq/coq/issues/7769>`_
+  and `#7385 <https://github.com/coq/coq/issues/7385>`_,
+  by Pierre-Marie Pédrot).
+
+- The tactics :tacn:`lia`, :tacn:`nia`, :tacn:`lra`, :tacn:`nra` are now using a novel
+  Simplex-based proof engine. In case of regression, unset :flag:`Simplex`
+  to get the venerable Fourier-based engine
+  (`#8457 <https://github.com/coq/coq/pull/8457>`_, by Fréderic Besson).
+
+- SSReflect:
+
+  - New intro patterns:
+
+    - temporary introduction: `=> +`
+    - block introduction: `=> [^ prefix ] [^~ suffix ]`
+    - fast introduction: `=> >`
+    - tactics as views: `=> /ltac:mytac`
+    - replace hypothesis: `=> {}H`
+
+      See Section :ref:`introduction_ssr`
+      (`#6705 <https://github.com/coq/coq/pull/6705>`_, by Enrico Tassi,
+      with help from Maxime Dénès,
+      ideas coming from various users).
+
+  - New tactic :tacn:`under` to rewrite under binders, given an
+    extensionality lemma:
+
+    - interactive mode: :n:`under @term`, associated terminator: :tacn:`over`
+    - one-liner mode: `under @term do [@tactic | ...]`
+
+    It can take occurrence switches, contextual patterns, and intro patterns:
+    :g:`under {2}[in RHS]eq_big => [i|i ?] do ...`
+    (`#9651 <https://github.com/coq/coq/pull/9651>`_,
+    by Erik Martin-Dorel and Enrico Tassi).
+
+- :cmd:`Combined Scheme` now works when inductive schemes are generated in sort
+  :math:`\Type`. It used to be limited to sort `Prop`
+  (`#7634 <https://github.com/coq/coq/pull/7634>`_, by Théo Winterhalter).
+
+- A new registration mechanism for reference from ML code to Coq
+  constructs has been added
+  (`#186 <https://github.com/coq/coq/pull/186>`_,
+  by Emilio Jesús Gallego Arias, Maxime Dénès and Vincent Laporte).
+
+- CoqIDE:
+
+  - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2
+    (`#9279 <https://github.com/coq/coq/pull/9279>`_,
+    by Hugo Herbelin, with help from Jacques Garrigue,
+    Emilio Jesús Gallego Arias, Michael Sogetrop and Vincent Laporte).
+
+  - Smart input for Unicode characters. For example, typing
+    ``\alpha`` then ``Shift+Space`` will insert the greek letter alpha.
+    A larger number of default bindings are provided, following the latex
+    naming convention. Bindings can be customized, either globally, or on a
+    per-project basis. See Section :ref:`coqide-unicode` for details
+    (`#8560 <https://github.com/coq/coq/pull/8560>`_, by Arthur Charguéraud).
+
+- Infrastructure and dependencies:
+
+  - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the
+    `INSTALL` file for more information on dependencies
+    (`#7522 <https://github.com/coq/coq/pull/7522>`_, by Emilio Jesús Gallego Arías).
+
+  - Coq 8.10 doesn't need Camlp5 to build anymore. It now includes a
+    fork of the core parsing library that Coq uses, which is a small
+    subset of the whole Camlp5 distribution. In particular, this subset
+    doesn't depend on the OCaml AST, allowing easier compilation and
+    testing on experimental OCaml versions. Coq also ships a new parser
+    `coqpp` that plugin authors must switch to
+    (`#7902 <https://github.com/coq/coq/pull/7902>`_,
+    `#7979 <https://github.com/coq/coq/pull/7979>`_,
+    `#8161 <https://github.com/coq/coq/pull/8161>`_,
+    `#8667 <https://github.com/coq/coq/pull/8667>`_,
+    and `#8945 <https://github.com/coq/coq/pull/8945>`_,
+    by Pierre-Marie Pédrot and Emilio Jesús Gallego Arias).
+
+    The Coq developers would like to thank Daniel de Rauglaudre for many
+    years of continued support.
+
+  - Coq now supports building with Dune, in addition to the traditional
+    Makefile which is scheduled for deprecation
+    (`#6857 <https://github.com/coq/coq/pull/6857>`_,
+    by Emilio Jesús Gallego Arias, with help from Rudi Grinberg).
+
+    Experimental support for building Coq projects has been integrated
+    in Dune at the same time, providing an `improved experience
+    <https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/>`_
+    for plugin developers. We thank the Dune team for their work
+    supporting Coq.
+
+Version 8.10 also comes with a bunch of smaller-scale changes and
+improvements regarding the different components of the system, including
+many additions to the standard library (see the next subsection for details).
+
+On the implementation side, the ``dev/doc/changes.md`` file documents
+the numerous changes to the implementation and improvements of
+interfaces. The file provides guidelines on porting a plugin to the new
+version and a plugin development tutorial originally made by Yves Bertot
+is now in `doc/plugin_tutorial`. The ``dev/doc/critical-bugs`` file
+documents the known critical bugs of |Coq| and affected releases.
+
+The efficiency of the whole system has seen improvements thanks to
+contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès.
+
+Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael
+Soegtrop, Théo Zimmermann worked on maintaining and improving the
+continuous integration system and package building infrastructure.
+Coq is now continuously tested against OCaml trunk, in addition to the
+oldest supported and latest OCaml releases.
+
+Coq's documentation for the development branch is now deployed
+continously at https://coq.github.io/doc/master/api (documentation of
+the ML API), https://coq.github.io/doc/master/refman (reference
+manual), and https://coq.github.io/doc/master/stdlib (documentation of
+the standard library). Similar links exist for the `v8.10` branch.
+
+The OPAM repository for |Coq| packages has been maintained by Guillaume
+Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2)
+with contributions from many users. A list of packages is available at
+https://coq.inria.fr/opam/www/.
+
+The 61 contributors to this version are David A. Dalrymple, Tanaka
+Akira, Benjamin Barenblat, Yves Bertot, Frédéric Besson, Lasse
+Blaauwbroek, Martin Bodin, Joachim Breitner, Tej Chajed, Frédéric
+Chapoton, Arthur Charguéraud, Cyril Cohen, Lukasz Czajka, Christian
+Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Gaëtan Gilbert, Matěj
+Grabovský, Simon Gregersen, Jason Gross, Samuel Gruetter, Hugo Herbelin,
+Jasper Hugunin, Mirai Ikebuchi, Emilio Jesus Gallego Arias, Chantal
+Keller, Matej Košík, Vincent Laporte, Olivier Laurent, Larry Darryl Lee
+Jr, Pierre Letouzey, Nick Lewycky, Yao Li, Yishuai Li, Xia Li-yao, Assia
+Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, Guillaume
+Melquiond, Kayla Ngan, Sam Pablo Kuper, Karl Palmskog, Clément
+Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Ryan
+Scott, Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau,
+Enrico Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo
+Winterhalter, Beta Ziliani and Théo Zimmermann.
+
+Many power users helped to improve the design of the new features via
+the issue and pull request system, the |Coq| development mailing list,
+the coq-club@inria.fr mailing list or the new Discourse forum. It would
+be impossible to mention exhaustively the names of everybody who to some
+extent influenced the development.
+
+Version 8.10 is the fifth release of |Coq| developed on a time-based
+development cycle. Its development spanned 6 months from the release of
+|Coq| 8.9. Vincent Laporte is the release manager and maintainer of this
+release. This release is the result of ~2500 commits and ~650 PRs merged,
+closing 150+ issues.
+
+| Santiago de Chile, April 2019,
+| Matthieu Sozeau for the |Coq| development team
+|
+
+Other changes in 8.10+beta1
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+- Command-line tools and options:
+
+  - The use of `coqtop` as a compiler has been deprecated, in favor of
+    `coqc`. Consequently option `-compile` will stop to be accepted in
+    the next release. `coqtop` is now reserved to interactive
+    use
+    (`#9095 <https://github.com/coq/coq/pull/9095>`_,
+    by Emilio Jesús Gallego Arias).
+
+  - New option ``-topfile filename``, which will set the current module name
+    (*à la* ``-top``) based on the filename passed, taking into account the
+    proper ``-R``/``-Q`` options. For example, given ``-R Foo foolib`` using
+    ``-topfile foolib/bar.v`` will set the module name to ``Foo.Bar``.
+    CoqIDE now properly sets the module name for a given file based on
+    its path
+    (`#8991 <https://github.com/coq/coq/pull/8991>`_,
+    closes `#8989 <https://github.com/coq/coq/issues/8989>`_,
+    by Gaëtan Gilbert).
+
+  - Experimental: Coq flags and options can now be set on the
+    command-line, e.g. ``-set "Universe Polymorphism=true"``
+    (`#9876 <https://github.com/coq/coq/pull/9876>`_, by Gaëtan Gilbert).
+
+  - The `-native-compiler` flag of `coqc` and `coqtop` now takes an
+    argument which can have three values:
+
+    - `no` disables native_compute
+    - `yes` enables native_compute and precompiles `.v` files to
+      native code
+    - `ondemand` enables native_compute but compiles code only when
+      `native_compute` is called
+
+    The default value is `ondemand`. Note that this flag now has
+    priority over the configure flag of the same name.
+
+    A new `-bytecode-compiler` flag for `coqc` and `coqtop` controls
+    whether conversion can use the VM. The default value is `yes`.
+
+    (`#8870 <https://github.com/coq/coq/pull/8870>`_, by Maxime Dénès)
+
+  - The pretty timing diff scripts (flag `TIMING=1` to a
+    `coq_makefile`\-made `Makefile`, also
+    `tools/make-both-single-timing-files.py`,
+    `tools/make-both-time-files.py`, and `tools/make-one-time-file.py`)
+    now correctly support non-UTF-8 characters in the output of
+    `coqc` / `make` as well as printing to stdout, on both python2 and
+    python3
+    (`#9872 <https://github.com/coq/coq/pull/9872>`_,
+    closes `#9767 <https://github.com/coq/coq/issues/9767>`_
+    and `#9705 <https://github.com/coq/coq/issues/9705>`_,
+    by Jason Gross)
+
+  - coq_makefile's install target now errors if any file to install is missing
+    (`#9906 <https://github.com/coq/coq/pull/9906>`_, by Gaëtan Gilbert).
+
+  - Preferences from ``coqide.keys`` are no longer overridden by
+    modifiers preferences in ``coqiderc``
+    (`#10014 <https://github.com/coq/coq/pull/10014>`_, by Hugo Herbelin).
+
+- Specification language, type inference:
+
+  - Fixing a missing check in interpreting instances of existential
+    variables that are bound to local definitions. Might exceptionally
+    induce an overhead if the cost of checking the conversion of the
+    corresponding definitions is additionally high
+    (`#8217 <https://github.com/coq/coq/pull/8217>`_,
+    closes `#8215 <https://github.com/coq/coq/issues/8215>`_,
+    by Hugo Herbelin).
+
+  - A few improvements in inference of the return clause of `match` that
+    can exceptionally introduce incompatibilities. This can be
+    solved by writing an explicit `return` clause, sometimes even simply
+    an explicit `return _` clause
+    (`#262 <https://github.com/coq/coq/pull/262>`_, by Hugo Herbelin).
+
+  - Using non-projection values with the projection syntax is not
+    allowed. For instance :g:`0.(S)` is not a valid way to write :g:`S 0`.
+    Projections from non-primitive (emulated) records are allowed with
+    warning "nonprimitive-projection-syntax"
+    (`#8829 <https://github.com/coq/coq/pull/8829>`_, by Gaëtan Gilbert).
+
+  - An option and attributes to control the automatic decision to declare
+    an inductive type as template polymorphic were added.  Warning
+    "auto-template" (off by default) can trigger when an inductive is
+    automatically declared template polymorphic without the attribute.
+
+    Inductive types declared by Funind will never be template polymorphic.
+
+    (`#8488 <https://github.com/coq/coq/pull/8488>`_, by Gaëtan Gilbert)
+
+- Notations:
+
+  - New command :cmd:`Declare Scope` to explicitly declare a scope name
+    before any use of it. Implicit declaration of a scope at the time of
+    :cmd:`Bind Scope`, :cmd:`Delimit Scope`, :cmd:`Undelimit Scope`,
+    or :cmd:`Notation` is deprecated
+    (`#7135 <https://github.com/coq/coq/pull/7135>`_, by Hugo Herbelin).
+
+  - Various bugs have been fixed (e.g. `#9214
+    <https://github.com/coq/coq/pull/9214>`_ on removing spurious
+    parentheses on abbreviations shortening a strict prefix of an
+    application, by Hugo Herbelin).
+
+  - :cmd:`Numeral Notation` now support inductive types in the input to
+    printing functions (e.g., numeral notations can be defined for terms
+    containing things like :g:`@cons nat O O`), and parsing functions now
+    fully normalize terms including parameters of constructors (so that,
+    e.g., a numeral notation whose parsing function outputs a proof of
+    :g:`Nat.gcd x y = 1` will no longer fail to parse due to containing the
+    constant :g:`Nat.gcd` in the parameter-argument of :g:`eq_refl`)
+    (`#9874 <https://github.com/coq/coq/pull/9840>`_,
+    closes `#9840 <https://github.com/coq/coq/issues/9840>`_
+    and `#9844 <https://github.com/coq/coq/issues/9844>`_,
+    by Jason Gross).
+
+  - Deprecated compatibility notations have actually been
+    removed. Uses of these notations are generally easy to fix thanks
+    to the hint contained in the deprecation warning emitted by Coq
+    8.8 and 8.9.  For projects that require more than a handful of
+    such fixes, there is `a script
+    <https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py>`_
+    that will do it automatically, using the output of ``coqc``
+    (`#8638 <https://github.com/coq/coq/pull/8638>`_, by Jason Gross).
+
+  - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar`
+    (`#10061 <https://github.com/coq/coq/pull/10061>`_,
+    fixes `#9681 <http://github.com/coq/coq/pull/9681>`_,
+    by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin).
+
+- The `quote plugin
+  <https://coq.inria.fr/distrib/V8.9.0/refman/proof-engine/detailed-tactic-examples.html#quote>`_
+  was removed. If some users are interested in maintaining this plugin
+  externally, the Coq development team can provide assistance for
+  extracting the plugin and setting up a new repository
+  (`#7894 <https://github.com/coq/coq/pull/7894>`_, by Maxime Dénès).
+
+- Ltac:
+
+  - Tactic names are no longer allowed to clash, even if they are not defined in
+    the same section. For example, the following is no longer accepted:
+    :g:`Ltac foo := idtac. Section S. Ltac foo := fail. End S.`
+    (`#8555 <https://github.com/coq/coq/pull/8555>`_, by Maxime Dénès).
+
+  - Names of existential variables occurring in Ltac functions
+    (e.g. :g:`?[n]` or :g:`?n` in terms - not in patterns) are now interpreted
+    the same way as other variable names occurring in Ltac functions
+    (`#7309 <https://github.com/coq/coq/pull/7309>`_, by Hugo Herbelin).
+
+- Tactics:
+
+  - Removed the deprecated `romega` tactic
+    (`#8419 <https://github.com/coq/coq/pull/8419>`_,
+    by Maxime Dénès and Vincent Laporte).
+
+  - Hint declaration and removal should now specify a database (e.g. `Hint Resolve
+    foo : database`). When the database name is omitted, the hint is added to the
+    `core` database (as previously), but a deprecation warning is emitted
+    (`#8987 <https://github.com/coq/coq/pull/8987>`_, by Maxime Dénès).
+
+  - There are now tactics in `PreOmega.v` called
+    `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and
+    `Z.to_euclidean_division_equations` (which combines the `div_mod`
+    and `quot_rem` variants) which allow :tacn:`lia`, :tacn:`nia`, etc to
+    support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively),
+    by posing the specifying equation for `Z.div` and `Z.modulo` before
+    replacing them with atoms
+    (`#8062 <https://github.com/coq/coq/pull/8062>`_, by Jason Gross).
+
+  - The syntax of the :tacn:`autoapply` tactic was fixed to conform with preexisting
+    documentation: it now takes a `with` clause instead of a `using` clause
+    (`#9524 <https://github.com/coq/coq/pull/9524>`_,
+    closes `#7632 <https://github.com/coq/coq/issues/7632>`_,
+    by Théo Zimmermann).
+
+  - Modes are now taken into account by :tacn:`typeclasses eauto` for
+    local hypotheses
+    (`#9996 <https://github.com/coq/coq/pull/9996>`_,
+    fixes `#5752 <https://github.com/coq/coq/issues/5752>`_,
+    by Maxime Dénès, review by Pierre-Marie Pédrot).
+
+  - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a
+    documented replacement of :tacn:`convert_concl_no_check`
+    (`#10012 <https://github.com/coq/coq/pull/10012>`_,
+    `#10017 <https://github.com/coq/coq/pull/10017>`_,
+    `#10053 <https://github.com/coq/coq/pull/10053>`_, and
+    `#10059 <https://github.com/coq/coq/pull/10059>`_,
+    by Hugo Herbelin and Paolo G. Giarrusso).
+
+  - The simplified value returned by :tacn:`field_simplify` is not
+    always a fraction anymore.  When the denominator is :g:`1`, it
+    returns :g:`x` while previously it was returning :g:`x/1`.  This
+    change could break codes that were post-processing application of
+    :tacn:`field_simplify` to get rid of these :g:`x/1`
+    (`#9854 <https://github.com/coq/coq/pull/9854>`_,
+    by Laurent Théry,
+    with help from Michael Soegtrop, Maxime Dénès, and Vincent Laporte).
+
+- SSReflect:
+
+  - Clear discipline made consistent across the entire proof language.
+    Whenever a clear switch `{x..}` comes immediately before an existing proof
+    context entry (used as a view, as a rewrite rule or as name for a new
+    context entry) then such entry is cleared too.
+
+    E.g. The following sentences are elaborated as follows (when H is an existing
+    proof context entry):
+
+    - `=> {x..} H`       ->  `=> {x..H} H`
+    - `=> {x..} /H`      ->  `=> /v {x..H}`
+    - `rewrite {x..} H`  ->  `rewrite E {x..H}`
+
+    (`#9341 <https://github.com/coq/coq/pull/9341>`_, by Enrico Tassi).
+
+  - `inE` now expands `y \in r x` when `r` is a `simpl_rel`.
+    New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion
+    class, simplified `predType` interface: `pred_class` and `mkPredType`
+    deprecated, `{pred T}` and `PredType` should be used instead.
+    `if c return t then ...` now expects `c` to be a variable bound in `t`.
+    New `nonPropType` interface matching types that do _not_ have sort `Prop`.
+    New `relpre R f` definition for the preimage of a relation R under f
+    (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier).
+
+- Vernacular commands:
+
+  - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`.
+    Names may not be repeated, and may not overlap with section variable names
+    (`#8820 <https://github.com/coq/coq/pull/8820>`_,
+    closes `#8791 <https://github.com/coq/coq/issues/8791>`_,
+    by Jasper Hugunin).
+
+  - Removed the deprecated `Implicit Tactic` family of commands
+    (`#8779 <https://github.com/coq/coq/pull/8779>`_, by Pierre-Marie Pédrot).
+
+  - The `Automatic Introduction` option has been removed and is now the
+    default
+    (`#9001 <https://github.com/coq/coq/pull/9001>`_,
+    by Emilio Jesús Gallego Arias).
+
+  - `Arguments` now accepts names for arguments provided with `extra_scopes`
+    (`#9117 <https://github.com/coq/coq/pull/9117>`_, by Maxime Dénès).
+
+  - The naming scheme for anonymous binders in a `Theorem` has changed to
+    avoid conflicts with explicitly named binders
+    (`#9160 <https://github.com/coq/coq/pull/9160>`_,
+    closes `#8819 <https://github.com/coq/coq/issues/8819>`_,
+    by Jasper Hugunin).
+
+  - Computation of implicit arguments now properly handles local definitions in the
+    binders for an `Instance`, and can be mixed with implicit binders `{x : T}`
+    (`#9307 <https://github.com/coq/coq/pull/9307>`_,
+    closes `#9300 <https://github.com/coq/coq/issues/9300>`_,
+    by Jasper Hugunin).
+
+  - :cmd:`Declare Instance` now requires an instance name.
+
+    The flag `Refine Instance Mode` has been turned off by default, meaning that
+    :cmd:`Instance` no longer opens a proof when a body is provided. The flag
+    has been deprecated and will be removed in the next version.
+
+    (`#9270 <https://github.com/coq/coq/pull/9270>`_,
+    and `#9825 <https://github.com/coq/coq/pull/9825>`_,
+    by Maxime Dénès)
+
+  - Command :cmd:`Instance`, when no body is provided, now always opens
+    a proof. This is a breaking change, as instance of :n:`Instance
+    @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will
+    have to be changed into :n:`Instance @ident__1 : @ident__2 := %{%}.`
+    or :n:`Instance @ident__1 : @ident__2. Proof. Qed.`
+    (`#9274 <https://github.com/coq/coq/pull/9274>`_, by Maxime Dénès).
+
+  - The flag :flag:`Program Mode` now means that the `Program` attribute is enabled
+    for all commands that support it. In particular, it does not have any effect
+    on tactics anymore. May cause some incompatibilities
+    (`#9410 <https://github.com/coq/coq/pull/9410>`_, by Maxime Dénès).
+
+  - The algorithm computing implicit arguments now behaves uniformly for primitive
+    projection and application nodes
+    (`#9509 <https://github.com/coq/coq/pull/9509>`_,
+    closes `#9508 <https://github.com/coq/coq/issues/9508>`_,
+    by Pierre-Marie Pédrot).
+
+  - :cmd:`Hypotheses` and :cmd:`Variables` can now take implicit
+    binders inside sections
+    (`#9364 <https://github.com/coq/coq/pull/9364>`_,
+    closes `#9363 <https://github.com/coq/coq/issues/9363>`_,
+    by Jasper Hugunin).
+
+  - Removed deprecated option `Automatic Coercions Import`
+    (`#8094 <https://github.com/coq/coq/pull/8094>`_, by Maxime Dénès).
+
+  - The ``Show Script`` command has been deprecated
+    (`#9829 <https://github.com/coq/coq/pull/9829>`_, by Vincent Laporte).
+
+  - :cmd:`Coercion` does not warn ambiguous paths which are obviously
+    convertible with existing ones
+    (`#9743 <https://github.com/coq/coq/pull/9743>`_,
+    closes `#3219 <https://github.com/coq/coq/issues/3219>`_,
+    by Kazuhiko Sakaguchi).
+
+  - A new flag :flag:`Fast Name Printing` has been introduced. It changes the
+    algorithm used for allocating bound variable names for a faster but less
+    clever one
+    (`#9078 <https://github.com/coq/coq/pull/9078>`_, by Pierre-Marie Pédrot).
+
+  - Option ``Typeclasses Axioms Are Instances`` (compatibility option
+    introduced in the previous version) is deprecated. Use :cmd:`Declare
+    Instance` for axioms which should be instances
+    (`#8920 <https://github.com/coq/coq/pull/8920>`_, by Gaëtan Gilbert).
+
+  - Removed option `Printing Primitive Projection Compatibility`
+    (`#9306 <https://github.com/coq/coq/pull/9306>`_, by Gaëtan Gilbert).
+
+- Standard Library:
+
+  - Added `Bvector.BVeq` that decides whether two `Bvector`\s are equal.
+    Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`
+    (`#8171 <https://github.com/coq/coq/pull/8171>`_, by Yishuai Li).
+
+  - Added `ByteVector` type that can convert to and from `string`
+    (`#8365 <https://github.com/coq/coq/pull/8365>`_, by Yishuai Li).
+
+  - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about
+    the upper bound of number represented by a vector.
+    Allowed implicit vector length argument in `Ndigits.Bv2N`
+    (`#8815 <https://github.com/coq/coq/pull/8815>`_, by Yishuai Li).
+
+  - The prelude used to be automatically Exported and is now only
+    Imported. This should be relevant only when importing files which
+    don't use `-noinit` into files which do
+    (`#9013 <https://github.com/coq/coq/pull/9013>`_, by Gaëtan Gilert).
+
+  - Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an
+    ordered type, using lexical order
+    (`#7221 <https://github.com/coq/coq/pull/7221>`_, by Li Yao).
+
+  - Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`
+    (`#9425 <https://github.com/coq/coq/pull/9425>`_, by Andres Erbsen).
+
+  - Moved the `auto` hints of the `FSet` library into a new
+    `fset` database
+    (`#9725 <https://github.com/coq/coq/pull/9725>`_, by Frédéric Besson).
+
+  - Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull`
+    (`#9984 <https://github.com/coq/coq/pull/9984>`_,
+    by Jean-Christophe Léchenet and Oliver Nash).
+
+- Some error messages that show problems with a pair of non-matching
+  values will now highlight the differences
+  (`#8669 <https://github.com/coq/coq/pull/8669>`_, by Jim Fehrle).
+
+- Changelog has been moved from a specific file `CHANGES.md` to the
+  reference manual; former Credits chapter of the reference manual has
+  been split in two parts: a History chapter which was enriched with
+  additional historical information about Coq versions 1 to 5, and a
+  Changes chapter which was enriched with the content formerly in
+  `CHANGES.md` and `COMPATIBILITY`
+  (`#9133 <https://github.com/coq/coq/pull/9133>`_,
+  `#9668 <https://github.com/coq/coq/pull/9668>`_,
+  `#9939 <https://github.com/coq/coq/pull/9939>`_,
+  `#9964 <https://github.com/coq/coq/pull/9964>`_,
+  and `#10085 <https://github.com/coq/coq/pull/10085>`_,
+  by Théo Zimmermann,
+  with help and ideas from Emilio Jesús Gallego Arias, Gaëtan
+  Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi).
+
 Version 8.9
 -----------
 
@@ -12,7 +606,7 @@ Summary of changes
 of features and deprecations or removals of deprecated features,
 cleanups of the internals of the system and API along with a few new
 features. This release includes many user-visible changes, including
-deprecations that are documented in ``CHANGES.md`` and new features that
+deprecations that are documented in the next subsection and new features that
 are documented in the reference manual. Here are the most important
 changes:
 
@@ -26,7 +620,7 @@ changes:
     manual).
 
   - Deprecated notations of the standard library will be removed in the
-    next version of |Coq|, see the ``CHANGES.md`` file for a script to
+    next version of |Coq|, see the next subsection for a script to
     ease porting, by Jason Gross and Jean-Christophe Léchenet.
 
   - Added the :cmd:`Numeral Notation` command for registering decimal
@@ -79,7 +673,7 @@ changes:
 - Library: additions and changes in the ``VectorDef``, ``Ascii``, and
   ``String`` libraries. Syntax notations are now available only when using
   ``Import`` of libraries and not merely ``Require``, by various
-  contributors (source of incompatibility, see ``CHANGES.md`` for details).
+  contributors (source of incompatibility, see the next subsection for details).
 
 - Toplevels: ``coqtop`` and ``coqide`` can now display diffs between proof
   steps in color, using the :opt:`Diffs` option, by Jim Fehrle.
@@ -96,7 +690,7 @@ changes:
 
 Version 8.9 also comes with a bunch of smaller-scale changes and
 improvements regarding the different components of the system.  Most
-important ones are documented in the ``CHANGES.md`` file.
+important ones are documented in the next subsection file.
 
 On the implementation side, the ``dev/doc/changes.md`` file documents
 the numerous changes to the implementation and improvements of
@@ -152,8 +746,8 @@ engineer working with Maxime Dénès in the |Coq| consortium.
 | Matthieu Sozeau for the |Coq| development team
 |
 
-Details of changes
-~~~~~~~~~~~~~~~~~~
+Details of changes in 8.9+beta1
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Kernel
 
@@ -167,16 +761,12 @@ Notations
 - Deprecated compatibility notations will actually be removed in the
   next version of Coq.  Uses of these notations are generally easy to
   fix thanks to the hint contained in the deprecation warnings. For
-  projects that require more than a handful of such fixes, there is [a
-  script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py)
-  that will do it automatically, using the output of coqc. The script
+  projects that require more than a handful of such fixes, there is `a
+  script
+  <https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py>`_
+  that will do it automatically, using the output of ``coqc``. The script
   contains documentation on its usage in a comment at the top.
 
-- When several notations are available for the same expression,
-  priority is given to latest notations defined in the scopes being
-  opened, in order, rather than to the latest notations defined
-  independently of whether they are in an opened scope or not.
-
 Tactics
 
 - Added toplevel goal selector `!` which expects a single focused goal.
@@ -260,7 +850,7 @@ Standard Library
   `Require Import Coq.Compat.Coq88` will make these notations
   available.  Users wishing to port their developments automatically
   may download `fix.py` from
-  <https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169>
+  https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169
   and run a command like `while true; do make -Okj 2>&1 |
   /path/to/fix.py; done` and get a cup of coffee.  (This command must
   be manually interrupted once the build finishes all the way though.
@@ -284,8 +874,8 @@ Tools
   If you would like to maintain this tool externally, please contact us.
 
 - Removed the Emacs modes distributed with Coq. You are advised to
-  use [Proof-General](https://proofgeneral.github.io/) (and optionally
-  [Company-Coq](https://github.com/cpitclaudel/company-coq)) instead.
+  use `Proof-General <https://proofgeneral.github.io/>`_ (and optionally
+  `Company-Coq <https://github.com/cpitclaudel/company-coq>`_) instead.
   If your use case is not covered by these alternative Emacs modes,
   please open an issue. We can help set up external maintenance as part
   of Proof-General, or independently as part of coq-community.
@@ -428,7 +1018,7 @@ version.
 
 Version 8.8 also comes with a bunch of smaller-scale changes and
 improvements regarding the different components of the system.
-Most important ones are documented in the ``CHANGES.md`` file.
+Most important ones are documented in the next subsection file.
 
 The efficiency of the whole system has seen improvements thanks to
 contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, Maxime Dénès and
@@ -788,7 +1378,7 @@ of integers and real constants are now represented using ``IZR`` (work by
 Guillaume Melquiond).
 
 Standard library additions and improvements by Jason Gross, Pierre Letouzey and
-others, documented in the ``CHANGES.md`` file.
+others, documented in the next subsection file.
 
 The mathematical proof language/declarative mode plugin was removed from the
 archive.
@@ -3349,7 +3939,7 @@ Vernacular commands
   Equality Schemes", this replaces deprecated option "Equality Scheme").
 - Made support for automatic generation of case analysis schemes available
   to user (governed by option "Set Case Analysis Schemes").
-- New command :n:`{? Global } Generalizable [All|No] [Variable|Variables] {* @ident}` to
+- New command :n:`{? Global } Generalizable {| All | No } {| Variable | Variables } {* @ident}` to
   declare which identifiers are generalizable in `` `{} `` and `` `() `` binders.
 - New command "Print Opaque Dependencies" to display opaque constants in
   addition to all variables, parameters or axioms a theorem or
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 48ad60c6dd..ec3343dac6 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -47,12 +47,13 @@ with open("refman-preamble.rst") as s:
 # -- General configuration ------------------------------------------------
 
 # If your documentation needs a minimal Sphinx version, state it here.
-#needs_sphinx = '1.0'
+needs_sphinx = '1.7.8'
 
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
 extensions = [
+    'sphinx.ext.ifconfig',
     'sphinx.ext.mathjax',
     'sphinx.ext.todo',
     'sphinxcontrib.bibtex',
@@ -100,6 +101,7 @@ def copy_formatspecific_files(app):
 
 def setup(app):
     app.connect('builder-inited', copy_formatspecific_files)
+    app.add_config_value('coq_config', coq_config, 'env')
 
 # The master toctree document.
 # We create this file in `copy_master_doc` above.
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index a91c6a9c5f..0a20d1c47b 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -42,6 +42,7 @@ Contents
    proof-engine/proof-handling
    proof-engine/tactics
    proof-engine/ltac
+   proof-engine/ltac2
    proof-engine/detailed-tactic-examples
    proof-engine/ssreflect-proof-language
 
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index 708820fff7..5562736997 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -41,6 +41,7 @@ The proof engine
    proof-engine/proof-handling
    proof-engine/tactics
    proof-engine/ltac
+   proof-engine/ltac2
    proof-engine/detailed-tactic-examples
    proof-engine/ssreflect-proof-language
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 695dea222f..5e214f6f7f 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor
 
   .. productionlist::
     record_term : {| [`field_def` ; … ; `field_def`] |}
-    field_def : name [binders] := `record_term`
+    field_def : `ident` [`binders`] := `term`
 
 Alternatively, the following syntax allows creating objects by using named fields, as
 shown in this grammar. The fields do not have to be in any particular order, nor do they have
@@ -831,16 +831,16 @@ Sections create local contexts which can be shared across multiple definitions.
 
       Links :token:`type` to each :token:`ident`.
 
-   .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
 
       Declare one or more variables with various types.
 
-   .. cmdv:: Variables {+ ( {+ @ident } : @type) }
-             Hypothesis {+ ( {+ @ident } : @type) }
-             Hypotheses {+ ( {+ @ident } : @type) }
+   .. cmdv:: Variables {+ ( {+ @ident } : @type) }
+             Hypothesis {+ ( {+ @ident } : @type) }
+             Hypotheses {+ ( {+ @ident } : @type) }
       :name: Variables; Hypothesis; Hypotheses
 
-      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
+      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
 
 .. cmd:: Let @ident := @term
 
@@ -931,7 +931,7 @@ In the syntax of module application, the ! prefix indicates that any
    :token:`module_binding`. The output module type
    is verified against each :token:`module_type`.
 
-.. cmdv:: Module [ Import | Export ]
+.. cmdv:: Module {| Import | Export }
 
    Behaves like :cmd:`Module`, but automatically imports or exports the module.
 
@@ -1648,7 +1648,7 @@ Declaring Implicit Arguments
 
 
 
-.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident }
+.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } }
    :name: Arguments (implicits)
 
    This command is used to set implicit arguments *a posteriori*,
@@ -1665,20 +1665,20 @@ Declaring Implicit Arguments
 
    This command clears implicit arguments.
 
-.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident }
+.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } }
 
    This command is used to recompute the implicit arguments of
    :token:`qualid` after ending of the current section if any, enforcing the
    implicit arguments known from inside the section to be the ones
    declared by the command.
 
-.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident }
+.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } }
 
    When in a module, tell not to activate the
    implicit arguments of :token:`qualid` declared by this command to contexts that
    require the module.
 
-.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } }
+.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } }
 
    For names of constants, inductive types,
    constructors, lemmas which can only be applied to a fixed number of
@@ -2048,6 +2048,21 @@ in :ref:`canonicalstructures`; here only a simple example is given.
       If a same field occurs in several canonical structures, then
       only the structure declared first as canonical is considered.
 
+   .. note::
+      To prevent a field from being involved in the inference of canonical instances,
+      its declaration can be annotated with the :g:`#[canonical(false)]` attribute.
+
+      .. example::
+
+         For instance, when declaring the :g:`Setoid` structure above, the
+         :g:`Prf_equiv` field declaration could be written as follows.
+
+         .. coqdoc::
+
+            #[canonical(false)] Prf_equiv : equivalence Carrier Equal
+
+      See :ref:`canonicalstructures` for a more realistic example.
+
    .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term
 
       This is equivalent to a regular definition of :token:`ident` followed by the
@@ -2067,6 +2082,10 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
          Print Canonical Projections.
 
+      .. note::
+
+         The last line would not show up if the corresponding projection (namely
+         :g:`Prf_equiv`) were annotated as not canonical, as described above.
 
 Implicit types of variables
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2148,7 +2167,7 @@ that specify which variables should be generalizable.
 
    Disable implicit generalization  entirely. This is the default behavior.
 
-.. cmd:: Generalizable (Variable | Variables) {+ @ident }
+.. cmd:: Generalizable {| Variable | Variables } {+ @ident }
 
    Allow generalization of the given identifiers only. Calling this command multiple times
    adds to the allowed identifiers.
@@ -2244,6 +2263,7 @@ Printing universes
       unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
 
 .. cmdv:: Print Universes Subgraph(@names)
+   :name: Print Universes Subgraph
 
    Prints the graph restricted to the requested names (adjusting
    constraints to preserve the implied transitive constraints between
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 5a1af9f9fa..8acbcbec8f 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -616,34 +616,34 @@ has type :token:`type`.
 
       Adds several parameters with specification :token:`type`.
 
-   .. cmdv:: Parameter {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Parameter {+ ( {+ @ident } : @type ) }
 
       Adds blocks of parameters with different specifications.
 
-   .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) }
       :name: Local Parameter
 
       Such parameters are never made accessible through their unqualified name by
       :cmd:`Import` and its variants. You have to explicitly give their fully
       qualified name to refer to them.
 
-   .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) }
-             {? Local } Axiom {+ ( {+ @ident } : @type ) }
-             {? Local } Axioms {+ ( {+ @ident } : @type ) }
-             {? Local } Conjecture {+ ( {+ @ident } : @type ) }
-             {? Local } Conjectures {+ ( {+ @ident } : @type ) }
+   .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) }
+             {? Local } Axiom {+ ( {+ @ident } : @type ) }
+             {? Local } Axioms {+ ( {+ @ident } : @type ) }
+             {? Local } Conjecture {+ ( {+ @ident } : @type ) }
+             {? Local } Conjectures {+ ( {+ @ident } : @type ) }
       :name: Parameters; Axiom; Axioms; Conjecture; Conjectures
 
-      These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
+      These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
 
-   .. cmdv:: Variable  {+ ( {+ @ident } : @type ) }
-             Variables {+ ( {+ @ident } : @type ) }
-             Hypothesis {+ ( {+ @ident } : @type ) }
-             Hypotheses {+ ( {+ @ident } : @type ) }
+   .. cmdv:: Variable  {+ ( {+ @ident } : @type ) }
+             Variables {+ ( {+ @ident } : @type ) }
+             Hypothesis {+ ( {+ @ident } : @type ) }
+             Hypotheses {+ ( {+ @ident } : @type ) }
       :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section)
 
       Outside of any section, these variants are synonyms of
-      :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
+      :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
       For their meaning inside a section, see :cmd:`Variable` in
       :ref:`section-mechanism`.
 
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index 97d86943fb..efb5df720a 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -181,7 +181,14 @@ presented as a notebook.
 The first section is for selecting the text font used for scripts,
 goal and message windows.
 
-The second section is devoted to file management: you may configure
+The second and third sections are for controlling colors and style.
+
+The fourth section is for customizing the editor. It includes in
+particular the ability to activate an Emacs mode named
+micro-Proof-General (use the Help menu to know more about the
+available bindings).
+
+The next section is devoted to file management: you may configure
 automatic saving of files, by periodically saving the contents into
 files named `#f#` for each opened file `f`. You may also activate the
 *revert* feature: in case a opened file is modified on the disk by a
@@ -252,6 +259,8 @@ use antialiased fonts or not, by setting the environment variable
 `GDK_USE_XFT` to 1 or 0 respectively.
 
 
+.. _coqide-unicode:
+
 Bindings for input of Unicode symbols
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 35231610fe..554f6bf230 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -909,13 +909,15 @@ Command line options
   :--coqlib url: Set base URL for the Coq standard library (default is
     `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url
     Coq``.
-  :-R dir coqdir: Map physical directory dir to |Coq| logical
+  :-R dir coqdir: Recursively map physical directory dir to |Coq| logical
     directory  ``coqdir`` (similarly to |Coq| option ``-R``).
+  :-Q dir coqdir: Map physical directory dir to |Coq| logical
+    directory  ``coqdir`` (similarly to |Coq| option ``-Q``).
 
     .. note::
 
-       option ``-R`` only has
-       effect on the files *following* it on the command line, so you will
+       options ``-R`` and ``-Q`` only have
+       effect on the files *following* them on the command line, so you will
        probably need to put this option first.
 
 
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index b629d15b11..0ace9ef5b9 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -396,381 +396,3 @@ the optional tactic of the ``Hint Rewrite`` command.
    .. coqtop:: none
 
       Qed.
-
-Using the tactic language
--------------------------
-
-
-About the cardinality of the set of natural numbers
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The first example which shows how to use pattern matching over the
-proof context is a proof of the fact that natural numbers have more
-than two elements. This can be done as follows:
-
-.. coqtop:: in reset
-
-   Lemma card_nat :
-     ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z.
-   Proof.
-
-.. coqtop:: in
-
-   red; intros (x, (y, Hy)).
-
-.. coqtop:: in
-
-   elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
-
-   match goal with
-       | _ : ?a = ?b, _ : ?a = ?c |- _ =>
-           cut (b = c); [ discriminate | transitivity a; auto ]
-   end.
-
-.. coqtop:: in
-
-   Qed.
-
-We can notice that all the (very similar) cases coming from the three
-eliminations (with three distinct natural numbers) are successfully
-solved by a match goal structure and, in particular, with only one
-pattern (use of non-linear matching).
-
-
-Permutations of lists
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-A more complex example is the problem of permutations of
-lists. The aim is to show that a list is a permutation of
-another list.
-
-.. coqtop:: in reset
-
-   Section Sort.
-
-.. coqtop:: in
-
-   Variable A : Set.
-
-.. coqtop:: in
-
-   Inductive perm : list A -> list A -> Prop :=
-       | perm_refl : forall l, perm l l
-       | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1)
-       | perm_append : forall a l, perm (a :: l) (l ++ a :: nil)
-       | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2.
-
-.. coqtop:: in
-
-   End Sort.
-
-First, we define the permutation predicate as shown above.
-
-.. coqtop:: none
-
-   Require Import List.
-
-
-.. coqtop:: in
-
-   Ltac perm_aux n :=
-   match goal with
-       | |- (perm _ ?l ?l) => apply perm_refl
-       | |- (perm _ (?a :: ?l1) (?a :: ?l2)) =>
-           let newn := eval compute in (length l1) in
-               (apply perm_cons; perm_aux newn)
-       | |- (perm ?A (?a :: ?l1) ?l2) =>
-           match eval compute in n with
-               | 1 => fail
-               | _ =>
-                   let l1' := constr:(l1 ++ a :: nil) in
-                       (apply (perm_trans A (a :: l1) l1' l2);
-                       [ apply perm_append | compute; perm_aux (pred n) ])
-           end
-   end.
-
-Next we define an auxiliary tactic ``perm_aux`` which takes an argument
-used to control the recursion depth. This tactic behaves as follows. If
-the lists are identical (i.e. convertible), it concludes. Otherwise, if
-the lists have identical heads, it proceeds to look at their tails.
-Finally, if the lists have different heads, it rotates the first list by
-putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the
-number of performed rotations using the argument ``n``. We do this by
-decrementing ``n`` each time we perform a rotation. It works because
-for a list of length ``n`` we can make exactly ``n - 1`` rotations
-to generate at most ``n`` distinct lists. Notice that we use the natural
-numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know
-that it is possible to use the usual natural numbers, but they are only
-used as arguments for primitive tactics and they cannot be handled, so,
-in particular, we cannot make computations with them. Thus the natural
-choice is to use Coq data structures so that Coq makes the computations
-(reductions) by ``eval compute in`` and we can get the terms back by match.
-
-.. coqtop:: in
-
-   Ltac solve_perm :=
-   match goal with
-       | |- (perm _ ?l1 ?l2) =>
-           match eval compute in (length l1 = length l2) with
-               | (?n = ?n) => perm_aux n
-           end
-   end.
-
-The main tactic is ``solve_perm``. It computes the lengths of the two lists
-and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they
-aren't, the lists cannot be permutations of each other). Using this tactic we
-can now prove lemmas as follows:
-
-.. coqtop:: in
-
-   Lemma solve_perm_ex1 :
-     perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
-   Proof. solve_perm. Qed.
-
-.. coqtop:: in
-
-   Lemma solve_perm_ex2 :
-     perm nat
-       (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
-         (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
-   Proof. solve_perm. Qed.
-
-Deciding intuitionistic propositional logic
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Pattern matching on goals allows a powerful backtracking when returning tactic
-values. An interesting application is the problem of deciding intuitionistic
-propositional logic. Considering the contraction-free sequent calculi LJT* of
-Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the
-tactic language as shown below.
-
-.. coqtop:: in reset
-
-   Ltac basic :=
-   match goal with
-       | |- True => trivial
-       | _ : False |- _ => contradiction
-       | _ : ?A |- ?A => assumption
-   end.
-
-.. coqtop:: in
-
-   Ltac simplify :=
-   repeat (intros;
-       match goal with
-           | H : ~ _ |- _ => red in H
-           | H : _ /\ _ |- _ =>
-               elim H; do 2 intro; clear H
-           | H : _ \/ _ |- _ =>
-               elim H; intro; clear H
-           | H : ?A /\ ?B -> ?C |- _ =>
-               cut (A -> B -> C);
-                   [ intro | intros; apply H; split; assumption ]
-           | H: ?A \/ ?B -> ?C |- _ =>
-               cut (B -> C);
-                   [ cut (A -> C);
-                       [ intros; clear H
-                       | intro; apply H; left; assumption ]
-                   | intro; apply H; right; assumption ]
-           | H0 : ?A -> ?B, H1 : ?A |- _ =>
-               cut B; [ intro; clear H0 | apply H0; assumption ]
-           | |- _ /\ _ => split
-           | |- ~ _ => red
-       end).
-
-.. coqtop:: in
-
-   Ltac my_tauto :=
-     simplify; basic ||
-     match goal with
-         | H : (?A -> ?B) -> ?C |- _ =>
-             cut (B -> C);
-                 [ intro; cut (A -> B);
-                     [ intro; cut C;
-                         [ intro; clear H | apply H; assumption ]
-                     | clear H ]
-                 | intro; apply H; intro; assumption ]; my_tauto
-         | H : ~ ?A -> ?B |- _ =>
-             cut (False -> B);
-                 [ intro; cut (A -> False);
-                     [ intro; cut B;
-                         [ intro; clear H | apply H; assumption ]
-                     | clear H ]
-                 | intro; apply H; red; intro; assumption ]; my_tauto
-         | |- _ \/ _ => (left; my_tauto) || (right; my_tauto)
-     end.
-
-The tactic ``basic`` tries to reason using simple rules involving truth, falsity
-and available assumptions. The tactic ``simplify`` applies all the reversible
-rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main
-tactic to be called) simplifies with ``simplify``, tries to conclude with
-``basic`` and tries several paths using the backtracking rules (one of the
-four Dyckhoff’s rules for the left implication to get rid of the contraction
-and the right ``or``).
-
-Having defined ``my_tauto``, we can prove tautologies like these:
-
-.. coqtop:: in
-
-   Lemma my_tauto_ex1 :
-     forall A B : Prop, A /\ B -> A \/ B.
-   Proof. my_tauto. Qed.
-
-.. coqtop:: in
-
-   Lemma my_tauto_ex2 :
-     forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
-   Proof. my_tauto. Qed.
-
-
-Deciding type isomorphisms
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-A more tricky problem is to decide equalities between types modulo
-isomorphisms. Here, we choose to use the isomorphisms of the simply
-typed λ-calculus with Cartesian product and unit type (see, for
-example, :cite:`RC95`). The axioms of this λ-calculus are given below.
-
-.. coqtop:: in reset
-
-   Open Scope type_scope.
-
-.. coqtop:: in
-
-   Section Iso_axioms.
-
-.. coqtop:: in
-
-   Variables A B C : Set.
-
-.. coqtop:: in
-
-   Axiom Com : A * B = B * A.
-
-   Axiom Ass : A * (B * C) = A * B * C.
-
-   Axiom Cur : (A * B -> C) = (A -> B -> C).
-
-   Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
-
-   Axiom P_unit : A * unit = A.
-
-   Axiom AR_unit : (A -> unit) = unit.
-
-   Axiom AL_unit : (unit -> A) = A.
-
-.. coqtop:: in
-
-   Lemma Cons : B = C -> A * B = A * C.
-
-   Proof.
-
-   intro Heq; rewrite Heq; reflexivity.
-
-   Qed.
-
-.. coqtop:: in
-
-   End Iso_axioms.
-
-.. coqtop:: in
-
-   Ltac simplify_type ty :=
-   match ty with
-       | ?A * ?B * ?C =>
-           rewrite <- (Ass A B C); try simplify_type_eq
-       | ?A * ?B -> ?C =>
-           rewrite (Cur A B C); try simplify_type_eq
-       | ?A -> ?B * ?C =>
-           rewrite (Dis A B C); try simplify_type_eq
-       | ?A * unit =>
-           rewrite (P_unit A); try simplify_type_eq
-       | unit * ?B =>
-           rewrite (Com unit B); try simplify_type_eq
-       | ?A -> unit =>
-           rewrite (AR_unit A); try simplify_type_eq
-       | unit -> ?B =>
-           rewrite (AL_unit B); try simplify_type_eq
-       | ?A * ?B =>
-           (simplify_type A; try simplify_type_eq) ||
-           (simplify_type B; try simplify_type_eq)
-       | ?A -> ?B =>
-           (simplify_type A; try simplify_type_eq) ||
-           (simplify_type B; try simplify_type_eq)
-   end
-   with simplify_type_eq :=
-   match goal with
-       | |- ?A = ?B => try simplify_type A; try simplify_type B
-   end.
-
-.. coqtop:: in
-
-   Ltac len trm :=
-   match trm with
-       | _ * ?B => let succ := len B in constr:(S succ)
-       | _ => constr:(1)
-   end.
-
-.. coqtop:: in
-
-   Ltac assoc := repeat rewrite <- Ass.
-
-.. coqtop:: in
-
-   Ltac solve_type_eq n :=
-   match goal with
-       | |- ?A = ?A => reflexivity
-       | |- ?A * ?B = ?A * ?C =>
-           apply Cons; let newn := len B in solve_type_eq newn
-       | |- ?A * ?B = ?C =>
-           match eval compute in n with
-               | 1 => fail
-               | _ =>
-                   pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n)
-           end
-   end.
-
-.. coqtop:: in
-
-   Ltac compare_structure :=
-   match goal with
-       | |- ?A = ?B =>
-           let l1 := len A
-           with l2 := len B in
-               match eval compute in (l1 = l2) with
-                   | ?n = ?n => solve_type_eq n
-               end
-   end.
-
-.. coqtop:: in
-
-   Ltac solve_iso := simplify_type_eq; compare_structure.
-
-The tactic to judge equalities modulo this axiomatization is shown above.
-The algorithm is quite simple. First types are simplified using axioms that
-can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``).
-The normal forms are sequences of Cartesian products without Cartesian product
-in the left component. These normal forms are then compared modulo permutation
-of the components by the tactic ``compare_structure``. If they have the same
-lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal.
-The main tactic that puts all these components together is called ``solve_iso``.
-
-Here are examples of what can be solved by ``solve_iso``.
-
-.. coqtop:: in
-
-   Lemma solve_iso_ex1 :
-     forall A B : Set, A * unit * B = B * (unit * A).
-   Proof.
-     intros; solve_iso.
-   Qed.
-
-.. coqtop:: in
-
-   Lemma solve_iso_ex2 :
-     forall A B C : Set,
-       (A * unit -> B * (C * unit)) =
-       (A * unit -> (C -> unit) * C) * (unit -> A -> B).
-   Proof.
-     intros; solve_iso.
-   Qed.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 0322b43694..bbd7e0ba3d 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1,14 +1,27 @@
 .. _ltac:
 
-The tactic language
-===================
+Ltac
+====
 
-This chapter gives a compact documentation of |Ltac|, the tactic language
-available in |Coq|. We start by giving the syntax, and next, we present the
-informal semantics. If you want to know more regarding this language and
-especially about its foundations, you can refer to :cite:`Del00`. Chapter
-:ref:`detailedexamplesoftactics` is devoted to giving small but nontrivial
-use examples of this language.
+This chapter documents the tactic language |Ltac|.
+
+We start by giving the syntax, and next, we present the informal
+semantics. To learn more about the language and
+especially about its foundations, please refer to :cite:`Del00`.
+
+.. example:: Basic tactic macros
+
+   Here are some examples of simple tactic macros that the
+   language lets you write.
+
+   .. coqdoc::
+
+      Ltac reduce_and_try_to_solve := simpl; intros; auto.
+
+      Ltac destruct_bool_and_rewrite b H1 H2 :=
+        destruct b; [ rewrite H1; eauto | rewrite H2; eauto ].
+
+   See Section :ref:`ltac-examples` for more advanced examples.
 
 .. _ltac-syntax:
 
@@ -347,7 +360,7 @@ Detecting progress
 
 We can check if a tactic made progress with:
 
-.. tacn:: progress expr
+.. tacn:: progress @expr
    :name: progress
 
    :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v``
@@ -542,7 +555,7 @@ Identity
 The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but
 it appears in the proof script.
 
-.. tacn:: idtac {* message_token}
+.. tacn:: idtac {* @message_token}
    :name: idtac
 
    This prints the given tokens. Strings and integers are printed
@@ -671,7 +684,7 @@ Timing a tactic that evaluates to a term
 Tactic expressions that produce terms can be timed with the experimental
 tactic
 
-.. tacn:: time_constr expr
+.. tacn:: time_constr @expr
    :name: time_constr
 
    which evaluates :n:`@expr ()` and displays the time the tactic expression
@@ -867,7 +880,7 @@ We can perform pattern matching on goals using the following expression:
 
 .. we should provide the full grammar here
 
-.. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end
    :name: match goal
 
    If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is
@@ -905,7 +918,7 @@ We can perform pattern matching on goals using the following expression:
       first), but it possible to reverse this order (oldest first)
       with the :n:`match reverse goal with` variant.
 
-   .. tacv:: multimatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+   .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end
 
       Using :n:`multimatch` instead of :n:`match` will allow subsequent tactics
       to backtrack into a right-hand side tactic which has backtracking points
@@ -916,7 +929,7 @@ We can perform pattern matching on goals using the following expression:
       The syntax :n:`match [reverse] goal …` is, in fact, a shorthand for
       :n:`once multimatch [reverse] goal …`.
 
-   .. tacv:: lazymatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+   .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end
 
       Using lazymatch instead of match will perform the same pattern matching
       procedure but will commit to the first matching branch with the first
@@ -1122,33 +1135,33 @@ Defining |Ltac| functions
 
 Basically, |Ltac| toplevel definitions are made as follows:
 
-.. cmd:: Ltac @ident {* @ident} := @expr
+.. cmd:: {? Local} Ltac @ident {* @ident} := @expr
+   :name: Ltac
 
    This defines a new |Ltac| function that can be used in any tactic
    script or new |Ltac| toplevel definition.
 
+   If preceded by the keyword ``Local``, the tactic definition will not be
+   exported outside the current module.
+
    .. note::
 
       The preceding definition can equivalently be written:
 
       :n:`Ltac @ident := fun {+ @ident} => @expr`
 
-   Recursive and mutual recursive function definitions are also possible
-   with the syntax:
-
    .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @expr
 
-      It is also possible to *redefine* an existing user-defined tactic using the syntax:
+      This syntax allows recursive and mutual recursive function definitions.
 
    .. cmdv:: Ltac @qualid {* @ident} ::= @expr
 
+      This syntax *redefines* an existing user-defined tactic.
+
       A previous definition of qualid must exist in the environment. The new
       definition will always be used instead of the old one and it goes across
       module boundaries.
 
-   If preceded by the keyword Local the tactic definition will not be
-   exported outside the current module.
-
 Printing |Ltac| tactics
 ~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1160,6 +1173,399 @@ Printing |Ltac| tactics
 
    This command displays a list of all user-defined tactics, with their arguments.
 
+
+.. _ltac-examples:
+
+Examples of using |Ltac|
+-------------------------
+
+Proof that the natural numbers have at least two elements
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. example:: Proof that the natural numbers have at least two elements
+
+   The first example shows how to use pattern matching over the proof
+   context to prove that natural numbers have at least two
+   elements. This can be done as follows:
+
+   .. coqtop:: reset all
+
+      Lemma card_nat :
+        ~ exists x y : nat, forall z:nat, x = z \/ y = z.
+      Proof.
+      intros (x & y & Hz).
+      destruct (Hz 0), (Hz 1), (Hz 2).
+
+   At this point, the :tacn:`congruence` tactic would finish the job:
+
+   .. coqtop:: all abort
+
+      all: congruence.
+
+   But for the purpose of the example, let's craft our own custom
+   tactic to solve this:
+
+   .. coqtop:: none
+
+      Lemma card_nat :
+        ~ exists x y : nat, forall z:nat, x = z \/ y = z.
+      Proof.
+      intros (x & y & Hz).
+      destruct (Hz 0), (Hz 1), (Hz 2).
+
+   .. coqtop:: all abort
+
+      all: match goal with
+           | _ : ?a = ?b, _ : ?a = ?c |- _ => assert (b = c) by now transitivity a
+           end.
+      all: discriminate.
+
+   Notice that all the (very similar) cases coming from the three
+   eliminations (with three distinct natural numbers) are successfully
+   solved by a ``match goal`` structure and, in particular, with only one
+   pattern (use of non-linear matching).
+
+
+Proving that a list is a permutation of a second list
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. example:: Proving that a list is a permutation of a second list
+
+   Let's first define the permutation predicate:
+
+   .. coqtop:: in reset
+
+      Section Sort.
+
+        Variable A : Set.
+
+        Inductive perm : list A -> list A -> Prop :=
+        | perm_refl : forall l, perm l l
+        | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1)
+        | perm_append : forall a l, perm (a :: l) (l ++ a :: nil)
+        | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2.
+
+      End Sort.
+
+   .. coqtop:: none
+
+      Require Import List.
+
+
+   Next we define an auxiliary tactic :g:`perm_aux` which takes an
+   argument used to control the recursion depth. This tactic works as
+   follows: If the lists are identical (i.e. convertible), it
+   completes the proof. Otherwise, if the lists have identical heads,
+   it looks at their tails.  Finally, if the lists have different
+   heads, it rotates the first list by putting its head at the end.
+
+   Every time we perform a rotation, we decrement :g:`n`. When :g:`n`
+   drops down to :g:`1`, we stop performing rotations and we fail.
+   The idea is to give the length of the list as the initial value of
+   :g:`n`. This way of counting the number of rotations will avoid
+   going back to a head that had been considered before.
+
+   From Section :ref:`ltac-syntax` we know that Ltac has a primitive
+   notion of integers, but they are only used as arguments for
+   primitive tactics and we cannot make computations with them. Thus,
+   instead, we use Coq's natural number type :g:`nat`.
+
+   .. coqtop:: in
+
+      Ltac perm_aux n :=
+        match goal with
+        | |- (perm _ ?l ?l) => apply perm_refl
+        | |- (perm _ (?a :: ?l1) (?a :: ?l2)) =>
+           let newn := eval compute in (length l1) in
+               (apply perm_cons; perm_aux newn)
+        | |- (perm ?A (?a :: ?l1) ?l2) =>
+           match eval compute in n with
+           | 1 => fail
+           | _ =>
+               let l1' := constr:(l1 ++ a :: nil) in
+               (apply (perm_trans A (a :: l1) l1' l2);
+               [ apply perm_append | compute; perm_aux (pred n) ])
+           end
+        end.
+
+
+   The main tactic is :g:`solve_perm`. It computes the lengths of the
+   two lists and uses them as arguments to call :g:`perm_aux` if the
+   lengths are equal. (If they aren't, the lists cannot be
+   permutations of each other.)
+
+   .. coqtop:: in
+
+      Ltac solve_perm :=
+        match goal with
+        | |- (perm _ ?l1 ?l2) =>
+           match eval compute in (length l1 = length l2) with
+           | (?n = ?n) => perm_aux n
+           end
+        end.
+
+   And now, here is how we can use the tactic :g:`solve_perm`:
+
+   .. coqtop:: out
+
+      Goal perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
+
+   .. coqtop:: all abort
+
+      solve_perm.
+
+   .. coqtop:: out
+
+      Goal perm nat
+             (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
+             (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
+
+   .. coqtop:: all abort
+
+      solve_perm.
+
+
+Deciding intuitionistic propositional logic
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Pattern matching on goals allows powerful backtracking when returning tactic
+values. An interesting application is the problem of deciding intuitionistic
+propositional logic. Considering the contraction-free sequent calculi LJT* of
+Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the
+tactic language as shown below.
+
+.. coqtop:: in reset
+
+   Ltac basic :=
+   match goal with
+       | |- True => trivial
+       | _ : False |- _ => contradiction
+       | _ : ?A |- ?A => assumption
+   end.
+
+.. coqtop:: in
+
+   Ltac simplify :=
+   repeat (intros;
+       match goal with
+           | H : ~ _ |- _ => red in H
+           | H : _ /\ _ |- _ =>
+               elim H; do 2 intro; clear H
+           | H : _ \/ _ |- _ =>
+               elim H; intro; clear H
+           | H : ?A /\ ?B -> ?C |- _ =>
+               cut (A -> B -> C);
+                   [ intro | intros; apply H; split; assumption ]
+           | H: ?A \/ ?B -> ?C |- _ =>
+               cut (B -> C);
+                   [ cut (A -> C);
+                       [ intros; clear H
+                       | intro; apply H; left; assumption ]
+                   | intro; apply H; right; assumption ]
+           | H0 : ?A -> ?B, H1 : ?A |- _ =>
+               cut B; [ intro; clear H0 | apply H0; assumption ]
+           | |- _ /\ _ => split
+           | |- ~ _ => red
+       end).
+
+.. coqtop:: in
+
+   Ltac my_tauto :=
+     simplify; basic ||
+     match goal with
+         | H : (?A -> ?B) -> ?C |- _ =>
+             cut (B -> C);
+                 [ intro; cut (A -> B);
+                     [ intro; cut C;
+                         [ intro; clear H | apply H; assumption ]
+                     | clear H ]
+                 | intro; apply H; intro; assumption ]; my_tauto
+         | H : ~ ?A -> ?B |- _ =>
+             cut (False -> B);
+                 [ intro; cut (A -> False);
+                     [ intro; cut B;
+                         [ intro; clear H | apply H; assumption ]
+                     | clear H ]
+                 | intro; apply H; red; intro; assumption ]; my_tauto
+         | |- _ \/ _ => (left; my_tauto) || (right; my_tauto)
+     end.
+
+The tactic ``basic`` tries to reason using simple rules involving truth, falsity
+and available assumptions. The tactic ``simplify`` applies all the reversible
+rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main
+tactic to be called) simplifies with ``simplify``, tries to conclude with
+``basic`` and tries several paths using the backtracking rules (one of the
+four Dyckhoff’s rules for the left implication to get rid of the contraction
+and the right ``or``).
+
+Having defined ``my_tauto``, we can prove tautologies like these:
+
+.. coqtop:: in
+
+   Lemma my_tauto_ex1 :
+     forall A B : Prop, A /\ B -> A \/ B.
+   Proof. my_tauto. Qed.
+
+.. coqtop:: in
+
+   Lemma my_tauto_ex2 :
+     forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
+   Proof. my_tauto. Qed.
+
+
+Deciding type isomorphisms
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A trickier problem is to decide equalities between types modulo
+isomorphisms. Here, we choose to use the isomorphisms of the simply
+typed λ-calculus with Cartesian product and unit type (see, for
+example, :cite:`RC95`). The axioms of this λ-calculus are given below.
+
+.. coqtop:: in reset
+
+   Open Scope type_scope.
+
+.. coqtop:: in
+
+   Section Iso_axioms.
+
+.. coqtop:: in
+
+   Variables A B C : Set.
+
+.. coqtop:: in
+
+   Axiom Com : A * B = B * A.
+
+   Axiom Ass : A * (B * C) = A * B * C.
+
+   Axiom Cur : (A * B -> C) = (A -> B -> C).
+
+   Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
+
+   Axiom P_unit : A * unit = A.
+
+   Axiom AR_unit : (A -> unit) = unit.
+
+   Axiom AL_unit : (unit -> A) = A.
+
+.. coqtop:: in
+
+   Lemma Cons : B = C -> A * B = A * C.
+
+   Proof.
+
+   intro Heq; rewrite Heq; reflexivity.
+
+   Qed.
+
+.. coqtop:: in
+
+   End Iso_axioms.
+
+.. coqtop:: in
+
+   Ltac simplify_type ty :=
+   match ty with
+       | ?A * ?B * ?C =>
+           rewrite <- (Ass A B C); try simplify_type_eq
+       | ?A * ?B -> ?C =>
+           rewrite (Cur A B C); try simplify_type_eq
+       | ?A -> ?B * ?C =>
+           rewrite (Dis A B C); try simplify_type_eq
+       | ?A * unit =>
+           rewrite (P_unit A); try simplify_type_eq
+       | unit * ?B =>
+           rewrite (Com unit B); try simplify_type_eq
+       | ?A -> unit =>
+           rewrite (AR_unit A); try simplify_type_eq
+       | unit -> ?B =>
+           rewrite (AL_unit B); try simplify_type_eq
+       | ?A * ?B =>
+           (simplify_type A; try simplify_type_eq) ||
+           (simplify_type B; try simplify_type_eq)
+       | ?A -> ?B =>
+           (simplify_type A; try simplify_type_eq) ||
+           (simplify_type B; try simplify_type_eq)
+   end
+   with simplify_type_eq :=
+   match goal with
+       | |- ?A = ?B => try simplify_type A; try simplify_type B
+   end.
+
+.. coqtop:: in
+
+   Ltac len trm :=
+   match trm with
+       | _ * ?B => let succ := len B in constr:(S succ)
+       | _ => constr:(1)
+   end.
+
+.. coqtop:: in
+
+   Ltac assoc := repeat rewrite <- Ass.
+
+.. coqtop:: in
+
+   Ltac solve_type_eq n :=
+   match goal with
+       | |- ?A = ?A => reflexivity
+       | |- ?A * ?B = ?A * ?C =>
+           apply Cons; let newn := len B in solve_type_eq newn
+       | |- ?A * ?B = ?C =>
+           match eval compute in n with
+               | 1 => fail
+               | _ =>
+                   pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n)
+           end
+   end.
+
+.. coqtop:: in
+
+   Ltac compare_structure :=
+   match goal with
+       | |- ?A = ?B =>
+           let l1 := len A
+           with l2 := len B in
+               match eval compute in (l1 = l2) with
+                   | ?n = ?n => solve_type_eq n
+               end
+   end.
+
+.. coqtop:: in
+
+   Ltac solve_iso := simplify_type_eq; compare_structure.
+
+The tactic to judge equalities modulo this axiomatization is shown above.
+The algorithm is quite simple. First types are simplified using axioms that
+can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``).
+The normal forms are sequences of Cartesian products without a Cartesian product
+in the left component. These normal forms are then compared modulo permutation
+of the components by the tactic ``compare_structure``. If they have the same
+length, the tactic ``solve_type_eq`` attempts to prove that the types are equal.
+The main tactic that puts all these components together is ``solve_iso``.
+
+Here are examples of what can be solved by ``solve_iso``.
+
+.. coqtop:: in
+
+   Lemma solve_iso_ex1 :
+     forall A B : Set, A * unit * B = B * (unit * A).
+   Proof.
+     intros; solve_iso.
+   Qed.
+
+.. coqtop:: in
+
+   Lemma solve_iso_ex2 :
+     forall A B C : Set,
+       (A * unit -> B * (C * unit)) =
+       (A * unit -> (C -> unit) * C) * (unit -> A -> B).
+   Proof.
+     intros; solve_iso.
+   Qed.
+
+
 Debugging |Ltac| tactics
 ------------------------
 
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
new file mode 100644
index 0000000000..aa603fc966
--- /dev/null
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -0,0 +1,992 @@
+.. _ltac2:
+
+.. coqtop:: none
+
+   From Ltac2 Require Import Ltac2.
+
+Ltac2
+=====
+
+The Ltac tactic language is probably one of the ingredients of the success of
+Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac:
+
+- has often unclear semantics
+- is very non-uniform due to organic growth
+- lacks expressivity (data structures, combinators, types, ...)
+- is slow
+- is error-prone and fragile
+- has an intricate implementation
+
+Following the need of users that start developing huge projects relying
+critically on Ltac, we believe that we should offer a proper modern language
+that features at least the following:
+
+- at least informal, predictable semantics
+- a typing system
+- standard programming facilities (i.e. datatypes)
+
+This new language, called Ltac2, is described in this chapter. It is still
+experimental but we encourage nonetheless users to start testing it,
+especially wherever an advanced tactic language is needed. The previous
+implementation of Ltac, described in the previous chapter, will be referred to
+as Ltac1.
+
+.. _ltac2_design:
+
+General design
+--------------
+
+There are various alternatives to Ltac1, such that Mtac or Rtac for instance.
+While those alternatives can be quite distinct from Ltac1, we designed
+Ltac2 to be closest as reasonably possible to Ltac1, while fixing the
+aforementioned defects.
+
+In particular, Ltac2 is:
+
+- a member of the ML family of languages, i.e.
+
+  * a call-by-value functional language
+  * with effects
+  * together with Hindley-Milner type system
+
+- a language featuring meta-programming facilities for the manipulation of
+  Coq-side terms
+- a language featuring notation facilities to help writing palatable scripts
+
+We describe more in details each point in the remainder of this document.
+
+ML component
+------------
+
+Overview
+~~~~~~~~
+
+Ltac2 is a member of the ML family of languages, in the sense that it is an
+effectful call-by-value functional language, with static typing à la
+Hindley-Milner (see :cite:`MilnerPrincipalTypeSchemes`). It is commonly accepted
+that ML constitutes a sweet spot in PL design, as it is relatively expressive
+while not being either too lax (unlike dynamic typing) nor too strict
+(unlike, say, dependent types).
+
+The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it
+naturally fits in the ML lineage, just as the historical ML was designed as
+the tactic language for the LCF prover. It can also be seen as a general-purpose
+language, by simply forgetting about the Coq-specific features.
+
+Sticking to a standard ML type system can be considered somewhat weak for a
+meta-language designed to manipulate Coq terms. In particular, there is no
+way to statically guarantee that a Coq term resulting from an Ltac2
+computation will be well-typed. This is actually a design choice, motivated
+by retro-compatibility with Ltac1. Instead, well-typedness is deferred to
+dynamic checks, allowing many primitive functions to fail whenever they are
+provided with an ill-typed term.
+
+The language is naturally effectful as it manipulates the global state of the
+proof engine. This allows to think of proof-modifying primitives as effects
+in a straightforward way. Semantically, proof manipulation lives in a monad,
+which allows to ensure that Ltac2 satisfies the same equations as a generic ML
+with unspecified effects would do, e.g. function reduction is substitution
+by a value.
+
+Type Syntax
+~~~~~~~~~~~
+
+At the level of terms, we simply elaborate on Ltac1 syntax, which is quite
+close to e.g. the one of OCaml. Types follow the simply-typed syntax of OCaml.
+
+The non-terminal :production:`lident` designates identifiers starting with a
+lowercase.
+
+.. productionlist:: coq
+   ltac2_type             : ( `ltac2_type`, ... , `ltac2_type` ) `ltac2_typeconst`
+                    : ( `ltac2_type` * ... * `ltac2_type` )
+                    : `ltac2_type` -> `ltac2_type`
+                    : `ltac2_typevar`
+   ltac2_typeconst        : ( `modpath` . )* `lident`
+   ltac2_typevar          : '`lident`
+   ltac2_typeparams       : ( `ltac2_typevar`, ... , `ltac2_typevar` )
+
+The set of base types can be extended thanks to the usual ML type
+declarations such as algebraic datatypes and records.
+
+Built-in types include:
+
+- ``int``, machine integers (size not specified, in practice inherited from OCaml)
+- ``string``, mutable strings
+- ``'a array``, mutable arrays
+- ``exn``, exceptions
+- ``constr``, kernel-side terms
+- ``pattern``, term patterns
+- ``ident``, well-formed identifiers
+
+Type declarations
+~~~~~~~~~~~~~~~~~
+
+One can define new types by the following commands.
+
+.. cmd:: Ltac2 Type @ltac2_typeparams @lident
+   :name: Ltac2 Type
+
+   This command defines an abstract type. It has no use for the end user and
+   is dedicated to types representing data coming from the OCaml world.
+
+.. cmdv:: Ltac2 Type {? rec} @ltac2_typeparams @lident := @ltac2_typedef
+
+   This command defines a type with a manifest. There are four possible
+   kinds of such definitions: alias, variant, record and open variant types.
+
+   .. productionlist:: coq
+      ltac2_typedef    : `ltac2_type`
+                       : [ `ltac2_constructordef` | ... | `ltac2_constructordef` ]
+                       : { `ltac2_fielddef` ; ... ; `ltac2_fielddef` }
+                       : [ .. ]
+      ltac2_constructordef   : `uident` [ ( `ltac2_type` , ... , `ltac2_type` ) ]
+      ltac2_fielddef         : [ mutable ] `ident` : `ltac2_type`
+
+   Aliases are just a name for a given type expression and are transparently
+   unfoldable to it. They cannot be recursive. The non-terminal
+   :production:`uident` designates identifiers starting with an uppercase.
+
+   Variants are sum types defined by constructors and eliminated by
+   pattern-matching. They can be recursive, but the `rec` flag must be
+   explicitly set. Pattern-maching must be exhaustive.
+
+   Records are product types with named fields and eliminated by projection.
+   Likewise they can be recursive if the `rec` flag is set.
+
+   .. cmdv:: Ltac2 Type @ltac2_typeparams @ltac2_qualid := [ @ltac2_constructordef ]
+
+      Open variants are a special kind of variant types whose constructors are not
+      statically defined, but can instead be extended dynamically. A typical example
+      is the standard `exn` type. Pattern-matching must always include a catch-all
+      clause. They can be extended by this command.
+
+Term Syntax
+~~~~~~~~~~~
+
+The syntax of the functional fragment is very close to the one of Ltac1, except
+that it adds a true pattern-matching feature, as well as a few standard
+constructions from ML.
+
+.. productionlist:: coq
+   ltac2_var        : `lident`
+   ltac2_qualid     : ( `modpath` . )* `lident`
+   ltac2_constructor: `uident`
+   ltac2_term       : `ltac2_qualid`
+                    : `ltac2_constructor`
+                    : `ltac2_term` `ltac2_term` ... `ltac2_term`
+                    : fun `ltac2_var` => `ltac2_term`
+                    : let `ltac2_var` := `ltac2_term` in `ltac2_term`
+                    : let rec `ltac2_var` := `ltac2_term` in `ltac2_term`
+                    : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end
+                    : `int`
+                    : `string`
+                    : `ltac2_term` ; `ltac2_term`
+                    : [| `ltac2_term` ; ... ; `ltac2_term` |]
+                    : ( `ltac2_term` , ... , `ltac2_term` )
+                    : { `ltac2_field` `ltac2_field` ... `ltac2_field` }
+                    : `ltac2_term` . ( `ltac2_qualid` )
+                    : `ltac2_term` . ( `ltac2_qualid` ) := `ltac2_term`
+                    : [; `ltac2_term` ; ... ; `ltac2_term` ]
+                    : `ltac2_term` :: `ltac2_term`
+                    : ...
+   ltac2_branch     : `ltac2_pattern` => `ltac2_term`
+   ltac2_pattern    : `ltac2_var`
+                    : _
+                    : ( `ltac2_pattern` , ... , `ltac2_pattern` )
+                    : `ltac2_constructor` `ltac2_pattern` ... `ltac2_pattern`
+                    : [ ]
+                    : `ltac2_pattern` :: `ltac2_pattern`
+   ltac2_field      : `ltac2_qualid` := `ltac2_term`
+
+In practice, there is some additional syntactic sugar that allows e.g. to
+bind a variable and match on it at the same time, in the usual ML style.
+
+There is a dedicated syntax for list and array literals.
+
+.. note::
+
+   For now, deep pattern matching is not implemented.
+
+Ltac Definitions
+~~~~~~~~~~~~~~~~
+
+.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term
+   :name: Ltac2
+
+   This command defines a new global Ltac2 value.
+
+   For semantic reasons, the body of the Ltac2 definition must be a syntactical
+   value, i.e. a function, a constant or a pure constructor recursively applied to
+   values.
+
+   If ``rec`` is set, the tactic is expanded into a recursive binding.
+
+   If ``mutable`` is set, the definition can be redefined at a later stage (see below).
+
+.. cmd:: Ltac2 Set @qualid := @ltac2_term
+   :name: Ltac2 Set
+
+   This command redefines a previous ``mutable`` definition.
+   Mutable definitions act like dynamic binding, i.e. at runtime, the last defined
+   value for this entry is chosen. This is useful for global flags and the like.
+
+Reduction
+~~~~~~~~~
+
+We use the usual ML call-by-value reduction, with an otherwise unspecified
+evaluation order. This is a design choice making it compatible with OCaml,
+if ever we implement native compilation. The expected equations are as follows::
+
+  (fun x => t) V ≡ t{x := V} (βv)
+
+  let x := V in t ≡ t{x := V} (let)
+
+  match C V₀ ... Vₙ with ... | C x₀ ... xₙ  => t | ... end ≡ t {xᵢ := Vᵢ} (ι)
+
+  (t any term, V values, C constructor)
+
+Note that call-by-value reduction is already a departure from Ltac1 which uses
+heuristics to decide when evaluating an expression. For instance, the following
+expressions do not evaluate the same way in Ltac1.
+
+:n:`foo (idtac; let x := 0 in bar)`
+
+:n:`foo (let x := 0 in bar)`
+
+Instead of relying on the :n:`idtac` idiom, we would now require an explicit thunk
+not to compute the argument, and :n:`foo` would have e.g. type
+:n:`(unit -> unit) -> unit`.
+
+:n:`foo (fun () => let x := 0 in bar)`
+
+Typing
+~~~~~~
+
+Typing is strict and follows Hindley-Milner system. Unlike Ltac1, there
+are no type casts at runtime, and one has to resort to conversion
+functions. See notations though to make things more palatable.
+
+In this setting, all usual argument-free tactics have type :n:`unit -> unit`, but
+one can return as well a value of type :n:`t` thanks to terms of type :n:`unit -> t`,
+or take additional arguments.
+
+Effects
+~~~~~~~
+
+Effects in Ltac2 are straightforward, except that instead of using the
+standard IO monad as the ambient effectful world, Ltac2 is going to use the
+tactic monad.
+
+Note that the order of evaluation of application is *not* specified and is
+implementation-dependent, as in OCaml.
+
+We recall that the `Proofview.tactic` monad is essentially a IO monad together
+with backtracking state representing the proof state.
+
+Intuitively a thunk of type :n:`unit -> 'a` can do the following:
+
+- It can perform non-backtracking IO like printing and setting mutable variables
+- It can fail in a non-recoverable way
+- It can use first-class backtrack. The proper way to figure that is that we
+  morally have the following isomorphism:
+  :n:`(unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a)))`
+  i.e. thunks can produce a lazy list of results where each
+  tail is waiting for a continuation exception.
+- It can access a backtracking proof state, made out amongst other things of
+  the current evar assignation and the list of goals under focus.
+
+We describe more thoroughly the various effects existing in Ltac2 hereafter.
+
+Standard IO
++++++++++++
+
+The Ltac2 language features non-backtracking IO, notably mutable data and
+printing operations.
+
+Mutable fields of records can be modified using the set syntax. Likewise,
+built-in types like `string` and `array` feature imperative assignment. See
+modules `String` and `Array` respectively.
+
+A few printing primitives are provided in the `Message` module, allowing to
+display information to the user.
+
+Fatal errors
+++++++++++++
+
+The Ltac2 language provides non-backtracking exceptions, also known as *panics*,
+through the following primitive in module `Control`.::
+
+  val throw : exn -> 'a
+
+Unlike backtracking exceptions from the next section, this kind of error
+is never caught by backtracking primitives, that is, throwing an exception
+destroys the stack. This is materialized by the following equation, where `E`
+is an evaluation context.::
+
+  E[throw e] ≡ throw e
+
+  (e value)
+
+There is currently no way to catch such an exception and it is a design choice.
+There might be at some future point a way to catch it in a brutal way,
+destroying all backtrack and return values.
+
+Backtrack
++++++++++
+
+In Ltac2, we have the following backtracking primitives, defined in the
+`Control` module.::
+
+  Ltac2 Type 'a result := [ Val ('a) | Err (exn) ].
+
+  val zero : exn -> 'a
+  val plus : (unit -> 'a) -> (exn -> 'a) -> 'a
+  val case : (unit -> 'a) -> ('a * (exn -> 'a)) result
+
+If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is
+list concatenation, while `case` is pattern-matching.
+
+The backtracking is first-class, i.e. one can write
+:n:`plus (fun () => "x") (fun _ => "y") : string` producing a backtracking string.
+
+These operations are expected to satisfy a few equations, most notably that they
+form a monoid compatible with sequentialization.::
+
+  plus t zero ≡ t ()
+  plus (fun () => zero e) f ≡ f e
+  plus (plus t f) g ≡ plus t (fun e => plus (f e) g)
+
+  case (fun () => zero e) ≡ Err e
+  case (fun () => plus (fun () => t) f) ≡ Val (t,f)
+
+  let x := zero e in u ≡ zero e
+  let x := plus t f in u ≡ plus (fun () => let x := t in u) (fun e => let x := f e in u)
+
+  (t, u, f, g, e values)
+
+Goals
++++++
+
+A goal is given by the data of its conclusion and hypotheses, i.e. it can be
+represented as `[Γ ⊢ A]`.
+
+The tactic monad naturally operates over the whole proofview, which may
+represent several goals, including none. Thus, there is no such thing as
+*the current goal*. Goals are naturally ordered, though.
+
+It is natural to do the same in Ltac2, but we must provide a way to get access
+to a given goal. This is the role of the `enter` primitive, that applies a
+tactic to each currently focused goal in turn.::
+
+  val enter : (unit -> unit) -> unit
+
+It is guaranteed that when evaluating `enter f`, `f` is called with exactly one
+goal under focus. Note that `f` may be called several times, or never, depending
+on the number of goals under focus before the call to `enter`.
+
+Accessing the goal data is then implicit in the Ltac2 primitives, and may panic
+if the invariants are not respected. The two essential functions for observing
+goals are given below.::
+
+  val hyp : ident -> constr
+  val goal : unit -> constr
+
+The two above functions panic if there is not exactly one goal under focus.
+In addition, `hyp` may also fail if there is no hypothesis with the
+corresponding name.
+
+Meta-programming
+----------------
+
+Overview
+~~~~~~~~
+
+One of the major implementation issues of Ltac1 is the fact that it is
+never clear whether an object refers to the object world or the meta-world.
+This is an incredible source of slowness, as the interpretation must be
+aware of bound variables and must use heuristics to decide whether a variable
+is a proper one or referring to something in the Ltac context.
+
+Likewise, in Ltac1, constr parsing is implicit, so that ``foo 0`` is
+not ``foo`` applied to the Ltac integer expression ``0`` (Ltac does have a
+notion of integers, though it is not first-class), but rather the Coq term
+:g:`Datatypes.O`.
+
+The implicit parsing is confusing to users and often gives unexpected results.
+Ltac2 makes these explicit using quoting and unquoting notation, although there
+are notations to do it in a short and elegant way so as not to be too cumbersome
+to the user.
+
+Generic Syntax for Quotations
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+In general, quotations can be introduced in terms using the following syntax, where
+:production:`quotentry` is some parsing entry.
+
+.. prodn::
+   ltac2_term += @ident : ( @quotentry )
+
+Built-in quotations
++++++++++++++++++++
+
+The current implementation recognizes the following built-in quotations:
+
+- ``ident``, which parses identifiers (type ``Init.ident``).
+- ``constr``, which parses Coq terms and produces an-evar free term at runtime
+  (type ``Init.constr``).
+- ``open_constr``, which parses Coq terms and produces a term potentially with
+  holes at runtime (type ``Init.constr`` as well).
+- ``pattern``, which parses Coq patterns and produces a pattern used for term
+  matching (type ``Init.pattern``).
+- ``reference``, which parses either a :n:`@qualid` or :n:`& @ident`. Qualified names
+  are globalized at internalization into the corresponding global reference,
+  while ``&id`` is turned into ``Std.VarRef id``. This produces at runtime a
+  ``Std.reference``.
+
+The following syntactic sugar is provided for two common cases.
+
+- ``@id`` is the same as ``ident:(id)``
+- ``'t`` is the same as ``open_constr:(t)``
+
+Strict vs. non-strict mode
+++++++++++++++++++++++++++
+
+Depending on the context, quotations producing terms (i.e. ``constr`` or
+``open_constr``) are not internalized in the same way. There are two possible
+modes, respectively called the *strict* and the *non-strict* mode.
+
+- In strict mode, all simple identifiers appearing in a term quotation are
+  required to be resolvable statically. That is, they must be the short name of
+  a declaration which is defined globally, excluding section variables and
+  hypotheses. If this doesn't hold, internalization will fail. To work around
+  this error, one has to specifically use the ``&`` notation.
+- In non-strict mode, any simple identifier appearing in a term quotation which
+  is not bound in the global context is turned into a dynamic reference to a
+  hypothesis. That is to say, internalization will succeed, but the evaluation
+  of the term at runtime will fail if there is no such variable in the dynamic
+  context.
+
+Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict
+mode is only set when evaluating Ltac2 snippets in interactive proof mode. The
+rationale is that it is cumbersome to explicitly add ``&`` interactively, while it
+is expected that global tactics enforce more invariants on their code.
+
+Term Antiquotations
+~~~~~~~~~~~~~~~~~~~
+
+Syntax
+++++++
+
+One can also insert Ltac2 code into Coq terms, similarly to what is possible in
+Ltac1.
+
+.. prodn::
+   term += ltac2:( @ltac2_term )
+
+Antiquoted terms are expected to have type ``unit``, as they are only evaluated
+for their side-effects.
+
+Semantics
++++++++++
+
+Interpretation of a quoted Coq term is done in two phases, internalization and
+evaluation.
+
+- Internalization is part of the static semantics, i.e. it is done at Ltac2
+  typing time.
+- Evaluation is part of the dynamic semantics, i.e. it is done when
+  a term gets effectively computed by Ltac2.
+
+Note that typing of Coq terms is a *dynamic* process occurring at Ltac2
+evaluation time, and not at Ltac2 typing time.
+
+Static semantics
+****************
+
+During internalization, Coq variables are resolved and antiquotations are
+type-checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq
+implementation terminology. Note that although it went through the
+type-checking of **Ltac2**, the resulting term has not been fully computed and
+is potentially ill-typed as a runtime **Coq** term.
+
+.. example::
+
+   The following term is valid (with type `unit -> constr`), but will fail at runtime:
+
+   .. coqtop:: in
+
+      Ltac2 myconstr () := constr:(nat -> 0).
+
+Term antiquotations are type-checked in the enclosing Ltac2 typing context
+of the corresponding term expression.
+
+.. example::
+
+   The following will type-check, with type `constr`.
+
+   .. coqdoc::
+
+      let x := '0 in constr:(1 + ltac2:(exact x))
+
+Beware that the typing environment of antiquotations is **not**
+expanded by the Coq binders from the term.
+
+  .. example::
+
+     The following Ltac2 expression will **not** type-check::
+
+     `constr:(fun x : nat => ltac2:(exact x))`
+     `(* Error: Unbound variable 'x' *)`
+
+There is a simple reason for that, which is that the following expression would
+not make sense in general.
+
+`constr:(fun x : nat => ltac2:(clear @x; exact x))`
+
+Indeed, a hypothesis can suddenly disappear from the runtime context if some
+other tactic pulls the rug from under you.
+
+Rather, the tactic writer has to resort to the **dynamic** goal environment,
+and must write instead explicitly that she is accessing a hypothesis, typically
+as follows.
+
+`constr:(fun x : nat => ltac2:(exact (hyp @x)))`
+
+This pattern is so common that we provide dedicated Ltac2 and Coq term notations
+for it.
+
+- `&x` as an Ltac2 expression expands to `hyp @x`.
+- `&x` as a Coq constr expression expands to
+  `ltac2:(Control.refine (fun () => hyp @x))`.
+
+Dynamic semantics
+*****************
+
+During evaluation, a quoted term is fully evaluated to a kernel term, and is
+in particular type-checked in the current environment.
+
+Evaluation of a quoted term goes as follows.
+
+- The quoted term is first evaluated by the pretyper.
+- Antiquotations are then evaluated in a context where there is exactly one goal
+  under focus, with the hypotheses coming from the current environment extended
+  with the bound variables of the term, and the resulting term is fed into the
+  quoted term.
+
+Relative orders of evaluation of antiquotations and quoted term are not
+specified.
+
+For instance, in the following example, `tac` will be evaluated in a context
+with exactly one goal under focus, whose last hypothesis is `H : nat`. The
+whole expression will thus evaluate to the term :g:`fun H : nat => H`.
+
+`let tac () := hyp @H in constr:(fun H : nat => ltac2:(tac ()))`
+
+Many standard tactics perform type-checking of their argument before going
+further. It is your duty to ensure that terms are well-typed when calling
+such tactics. Failure to do so will result in non-recoverable exceptions.
+
+**Trivial Term Antiquotations**
+
+It is possible to refer to a variable of type `constr` in the Ltac2 environment
+through a specific syntax consistent with the antiquotations presented in
+the notation section.
+
+.. prodn:: term += $@lident
+
+In a Coq term, writing :g:`$x` is semantically equivalent to
+:g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to
+insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term.
+
+Match over terms
+~~~~~~~~~~~~~~~~
+
+Ltac2 features a construction similar to Ltac1 :n:`match` over terms, although
+in a less hard-wired way.
+
+.. productionlist:: coq
+   ltac2_term       : match! `ltac2_term` with `constrmatching` .. `constrmatching` end
+                    : lazy_match! `ltac2_term` with `constrmatching` .. `constrmatching` end
+                    : multi_match! `ltac2_term` with `constrmatching` .. `constrmatching` end
+   constrmatching  : | `constrpattern` => `ltac2_term`
+   constrpattern   : `term`
+                   : context  [ `term` ]
+                   : context `lident` [ `term` ]
+
+This construction is not primitive and is desugared at parsing time into
+calls to term matching functions from the `Pattern` module. Internally, it is
+implemented thanks to a specific scope accepting the :n:`@constrmatching` syntax.
+
+Variables from the :n:`@constrpattern` are statically bound in the body of the branch, to
+values of type `constr` for the variables from the :n:`@constr` pattern and to a
+value of type `Pattern.context` for the variable :n:`@lident`.
+
+Note that unlike Ltac, only lowercase identifiers are valid as Ltac2
+bindings, so that there will be a syntax error if one of the bound variables
+starts with an uppercase character.
+
+The semantics of this construction is otherwise the same as the corresponding
+one from Ltac1, except that it requires the goal to be focused.
+
+Match over goals
+~~~~~~~~~~~~~~~~
+
+Similarly, there is a way to match over goals in an elegant way, which is
+just a notation desugared at parsing time.
+
+.. productionlist:: coq
+   ltac2_term             : match! [ reverse ] goal with `goalmatching` ... `goalmatching` end
+                    : lazy_match! [ reverse ] goal with `goalmatching` ... `goalmatching` end
+                    : multi_match! [ reverse ] goal with `goalmatching` ... `goalmatching` end
+   goalmatching     : | [ `hypmatching` ... `hypmatching` |- `constrpattern` ] => `ltac2_term`
+   hypmatching      : `lident` : `constrpattern`
+                    : _ : `constrpattern`
+
+Variables from :n:`@hypmatching` and :n:`@constrpattern` are bound in the body of the
+branch. Their types are:
+
+- ``constr`` for pattern variables appearing in a :n:`@term`
+- ``Pattern.context`` for variables binding a context
+- ``ident`` for variables binding a hypothesis name.
+
+The same identifier caveat as in the case of matching over constr applies, and
+this features has the same semantics as in Ltac1. In particular, a ``reverse``
+flag can be specified to match hypotheses from the more recently introduced to
+the least recently introduced one.
+
+Notations
+---------
+
+Notations are the crux of the usability of Ltac1. We should be able to recover
+a feeling similar to the old implementation by using and abusing notations.
+
+Scopes
+~~~~~~
+
+A scope is a name given to a grammar entry used to produce some Ltac2 expression
+at parsing time. Scopes are described using a form of S-expression.
+
+.. prodn::
+   ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) }
+
+A few scopes contain antiquotation features. For sake of uniformity, all
+antiquotations are introduced by the syntax :n:`$@lident`.
+
+The following scopes are built-in.
+
+- :n:`constr`:
+
+  + parses :n:`c = @term` and produces :n:`constr:(c)`
+
+- :n:`ident`:
+
+  + parses :n:`id = @ident` and produces :n:`ident:(id)`
+  + parses :n:`$(x = @ident)` and produces the variable :n:`x`
+
+- :n:`list0(@ltac2_scope)`:
+
+  + if :n:`@ltac2_scope` parses :production:`entry`, parses :n:`(@entry__0, ..., @entry__n)` and produces
+    :n:`[@entry__0; ...; @entry__n]`.
+
+- :n:`list0(@ltac2_scope, sep = @string__sep)`:
+
+  + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`(@entry__0 @string__sep ... @string__sep @entry__n)`
+    and produces :n:`[@entry__0; ...; @entry__n]`.
+
+- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @entry}` instead
+  of :n:`{* @entry}`.
+
+- :n:`opt(@ltac2_scope)`
+
+  + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`{? @entry}` and produces either :n:`None` or
+    :n:`Some x` where :n:`x` is the parsed expression.
+
+- :n:`self`:
+
+  + parses a Ltac2 expression at the current level and return it as is.
+
+- :n:`next`:
+
+  + parses a Ltac2 expression at the next level and return it as is.
+
+- :n:`tactic(n = @integer)`:
+
+  + parses a Ltac2 expression at the provided level :n:`n` and return it as is.
+
+- :n:`thunk(@ltac2_scope)`:
+
+  + parses the same as :n:`scope`, and if :n:`e` is the parsed expression, returns
+    :n:`fun () => e`.
+
+- :n:`STRING`:
+
+  + parses the corresponding string as an identifier and returns :n:`()`.
+
+- :n:`keyword(s = @string)`:
+
+  + parses the string :n:`s` as a keyword and returns `()`.
+
+- :n:`terminal(s = @string)`:
+
+  + parses the string :n:`s` as a keyword, if it is already a
+    keyword, otherwise as an :n:`@ident`. Returns `()`.
+
+- :n:`seq(@ltac2_scope__1, ..., @ltac2_scope__2)`:
+
+  + parses :n:`scope__1`, ..., :n:`scope__n` in this order, and produces a tuple made
+    out of the parsed values in the same order. As an optimization, all
+    subscopes of the form :n:`STRING` are left out of the returned tuple, instead
+    of returning a useless unit value. It is forbidden for the various
+    subscopes to refer to the global entry using self or next.
+
+A few other specific scopes exist to handle Ltac1-like syntax, but their use is
+discouraged and they are thus not documented.
+
+For now there is no way to declare new scopes from Ltac2 side, but this is
+planned.
+
+Notations
+~~~~~~~~~
+
+The Ltac2 parser can be extended by syntactic notations.
+
+.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term
+   :name: Ltac2 Notation
+
+   A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded
+   to the provided body where every token from the notation is let-bound to the
+   corresponding generated expression.
+
+   .. example::
+
+      Assume we perform:
+
+      .. coqdoc::
+
+         Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids.
+
+      Then the following expression
+
+      `let y := @X in foo (nat -> nat) x $y`
+
+      will expand at parsing time to
+
+      `let y := @X in`
+      `let c := fun () => constr:(nat -> nat) with ids := [@x; y] in Bar.f c ids`
+
+      Beware that the order of evaluation of multiple let-bindings is not specified,
+      so that you may have to resort to thunking to ensure that side-effects are
+      performed at the right time.
+
+Abbreviations
+~~~~~~~~~~~~~
+
+.. cmdv:: Ltac2 Notation @lident := @ltac2_term
+
+  This command introduces a special kind of notations, called abbreviations,
+  that is designed so that it does not add any parsing rules. It is similar in
+  spirit to Coq abbreviations, insofar as its main purpose is to give an
+  absolute name to a piece of pure syntax, which can be transparently referred
+  by this name as if it were a proper definition.
+
+  The abbreviation can then be manipulated just as a normal Ltac2 definition,
+  except that it is expanded at internalization time into the given expression.
+  Furthermore, in order to make this kind of construction useful in practice in
+  an effectful language such as Ltac2, any syntactic argument to an abbreviation
+  is thunked on-the-fly during its expansion.
+
+For instance, suppose that we define the following.
+
+:n:`Ltac2 Notation foo := fun x => x ().`
+
+Then we have the following expansion at internalization time.
+
+:n:`foo 0 ↦ (fun x => x ()) (fun _ => 0)`
+
+Note that abbreviations are not typechecked at all, and may result in typing
+errors after expansion.
+
+Evaluation
+----------
+
+Ltac2 features a toplevel loop that can be used to evaluate expressions.
+
+.. cmd:: Ltac2 Eval @ltac2_term
+   :name: Ltac2 Eval
+
+   This command evaluates the term in the current proof if there is one, or in the
+   global environment otherwise, and displays the resulting value to the user
+   together with its type. This command is pure in the sense that it does not
+   modify the state of the proof, and in particular all side-effects are discarded.
+
+Debug
+-----
+
+.. flag:: Ltac2 Backtrace
+
+   When this flag is set, toplevel failures will be printed with a backtrace.
+
+Compatibility layer with Ltac1
+------------------------------
+
+Ltac1 from Ltac2
+~~~~~~~~~~~~~~~~
+
+Simple API
+++++++++++
+
+One can call Ltac1 code from Ltac2 by using the :n:`ltac1` quotation. It parses
+a Ltac1 expression, and semantics of this quotation is the evaluation of the
+corresponding code for its side effects. In particular, it cannot return values,
+and the quotation has type :n:`unit`.
+
+Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited
+to the use of standalone function calls.
+
+Low-level API
++++++++++++++
+
+There exists a lower-level FFI into Ltac1 that is not recommended for daily use,
+which is available in the `Ltac2.Ltac1` module. This API allows to directly
+manipulate dynamically-typed Ltac1 values, either through the function calls,
+or using the `ltac1val` quotation. The latter parses the same as `ltac1`, but
+has type `Ltac2.Ltac1.t` instead of `unit`, and dynamically behaves as an Ltac1
+thunk, i.e. `ltac1val:(foo)` corresponds to the tactic closure that Ltac1
+would generate from `idtac; foo`.
+
+Due to intricate dynamic semantics, understanding when Ltac1 value quotations
+focus is very hard. This is why some functions return a continuation-passing
+style value, as it can dispatch dynamically between focused and unfocused
+behaviour.
+
+Ltac2 from Ltac1
+~~~~~~~~~~~~~~~~
+
+Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation
+instead.
+
+Note that the tactic expression is evaluated eagerly, if one wants to use it as
+an argument to a Ltac1 function, she has to resort to the good old
+:n:`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately
+and won't print anything.
+
+.. coqtop:: in
+
+   From Ltac2 Require Import Ltac2.
+   Set Default Proof Mode "Classic".
+
+.. coqtop:: all
+
+   Ltac mytac tac := idtac "wow"; tac.
+
+   Goal True.
+   Proof.
+   Fail mytac ltac2:(fail).
+
+Transition from Ltac1
+---------------------
+
+Owing to the use of a lot of notations, the transition should not be too
+difficult. In particular, it should be possible to do it incrementally. That
+said, we do *not* guarantee you it is going to be a blissful walk either.
+Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq
+will help you.
+
+We list the major changes and the transition strategies hereafter.
+
+Syntax changes
+~~~~~~~~~~~~~~
+
+Due to conflicts, a few syntactic rules have changed.
+
+- The dispatch tactical :n:`tac; [foo|bar]` is now written :n:`tac > [foo|bar]`.
+- Levels of a few operators have been revised. Some tacticals now parse as if
+  they were a normal function, i.e. one has to put parentheses around the
+  argument when it is complex, e.g an abstraction. List of affected tacticals:
+  :n:`try`, :n:`repeat`, :n:`do`, :n:`once`, :n:`progress`, :n:`time`, :n:`abstract`.
+- :n:`idtac` is no more. Either use :n:`()` if you expect nothing to happen,
+  :n:`(fun () => ())` if you want a thunk (see next section), or use printing
+  primitives from the :n:`Message` module if you want to display something.
+
+Tactic delay
+~~~~~~~~~~~~
+
+Tactics are not magically delayed anymore, neither as functions nor as
+arguments. It is your responsibility to thunk them beforehand and apply them
+at the call site.
+
+A typical example of a delayed function:
+
+:n:`Ltac foo := blah.`
+
+becomes
+
+:n:`Ltac2 foo () := blah.`
+
+All subsequent calls to `foo` must be applied to perform the same effect as
+before.
+
+Likewise, for arguments:
+
+:n:`Ltac bar tac := tac; tac; tac.`
+
+becomes
+
+:n:`Ltac2 bar tac := tac (); tac (); tac ().`
+
+We recommend the use of syntactic notations to ease the transition. For
+instance, the first example can alternatively be written as:
+
+:n:`Ltac2 foo0 () := blah.`
+:n:`Ltac2 Notation foo := foo0 ().`
+
+This allows to keep the subsequent calls to the tactic as-is, as the
+expression `foo` will be implicitly expanded everywhere into `foo0 ()`. Such
+a trick also works for arguments, as arguments of syntactic notations are
+implicitly thunked. The second example could thus be written as follows.
+
+:n:`Ltac2 bar0 tac := tac (); tac (); tac ().`
+:n:`Ltac2 Notation bar := bar0.`
+
+Variable binding
+~~~~~~~~~~~~~~~~
+
+Ltac1 relies on complex dynamic trickery to be able to tell apart bound
+variables from terms, hypotheses, etc. There is no such thing in Ltac2,
+as variables are recognized statically and other constructions do not live in
+the same syntactic world. Due to the abuse of quotations, it can sometimes be
+complicated to know what a mere identifier represents in a tactic expression. We
+recommend tracking the context and letting the compiler print typing errors to
+understand what is going on.
+
+We list below the typical changes one has to perform depending on the static
+errors produced by the typechecker.
+
+In Ltac expressions
++++++++++++++++++++
+
+.. exn:: Unbound {| value | constructor } X
+
+   * if `X` is meant to be a term from the current stactic environment, replace
+     the problematic use by `'X`.
+   * if `X` is meant to be a hypothesis from the goal context, replace the
+     problematic use by `&X`.
+
+In quotations
++++++++++++++
+
+.. exn:: The reference X was not found in the current environment
+
+   * if `X` is meant to be a tactic expression bound by a Ltac2 let or function,
+     replace the problematic use by `$X`.
+   * if `X` is meant to be a hypothesis from the goal context, replace the
+     problematic use by `&X`.
+
+Exception catching
+~~~~~~~~~~~~~~~~~~
+
+Ltac2 features a proper exception-catching mechanism. For this reason, the
+Ltac1 mechanism relying on `fail` taking integers, and tacticals decreasing it,
+has been removed. Now exceptions are preserved by all tacticals, and it is
+your duty to catch them and reraise them depending on your use.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 16b158c397..4a2f9c0db3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -322,7 +322,7 @@ Navigation in the proof tree
 .. index:: {
            }
 
-.. cmd:: %{ %| %}
+.. cmd:: {| %{ | %} }
 
    The command ``{`` (without a terminating period) focuses on the first
    goal, much like :cmd:`Focus` does, however, the subproof can only be
@@ -430,7 +430,7 @@ not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further
 nesting levels provided they are delimited by these. Bullets are made of
 repeated ``-``, ``+`` or ``*`` symbols:
 
-.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * }
+.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } }
 
 Note again that when a focused goal is proved a message is displayed
 together with a suggestion about the right bullet or ``}`` to unfocus it
@@ -492,7 +492,7 @@ The following example script illustrates all these features:
 
 Set Bullet Behavior
 ```````````````````
-.. opt:: Bullet Behavior  %( "None" %| "Strict Subproofs" %)
+.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" }
    :name: Bullet Behavior
 
    This option controls the bullet behavior and can take two possible values:
@@ -544,9 +544,9 @@ Requesting information
 
       ``<Your Tactic Text here>``.
 
-     .. deprecated:: 8.10
+      .. deprecated:: 8.10
 
-        Please use a text editor.
+         Please use a text editor.
 
    .. cmdv:: Show Proof
       :name: Show Proof
@@ -680,7 +680,7 @@ This image shows an error message with diff highlighting in CoqIDE:
 How to enable diffs
 ```````````````````
 
-.. opt:: Diffs %( "on" %| "off" %| "removed" %)
+.. opt:: Diffs {| "on" | "off" | "removed" }
    :name: Diffs
 
    The “on” setting highlights added tokens in green, while the “removed” setting
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 4e40df6f94..75e019592f 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -617,7 +617,7 @@ Abbreviations
      selected occurrences of a term.
 
 .. prodn::
-   occ_switch ::= { {? + %| - } {* @num } }
+   occ_switch ::= { {? {| + | - } } {* @num } }
 
 where:
 
@@ -2273,7 +2273,7 @@ to the others.
 Iteration
 ~~~~~~~~~
 
-.. tacn:: do {? @num } ( @tactic | [ {+| @tactic } ] )
+.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] }
    :name: do (ssreflect)
 
    This tactical offers an accurate control on the repetition of tactics.
@@ -2300,7 +2300,7 @@ tactic should be repeated on the current subgoal.
 There are four kinds of multipliers:
 
 .. prodn::
-   mult ::= @num ! %| ! %| @num ? %| ?
+   mult ::= {| @num ! | ! | @num ? | ? }
 
 Their meaning is:
 
@@ -2571,7 +2571,7 @@ destruction of existential assumptions like in the tactic:
 An alternative use of the ``have`` tactic is to provide the explicit proof
 term for the intermediate lemma, using tactics of the form:
 
-.. tacv:: have {? @ident } := term
+.. tacv:: have {? @ident } := @term
 
    This tactic creates a new assumption of type the type of :token:`term`.
    If the
@@ -5444,7 +5444,7 @@ equivalences are indeed taken into account, otherwise only single
 |SSR| searching tool
 --------------------
 
-.. cmd:: Search {? @pattern }  {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } }
+.. cmd:: Search {? @pattern }  {* {? - } {| @string | @pattern } {? % @ident} } {? in {+ {? - } @qualid } }
    :name: Search (ssreflect)
 
    This is the |SSR| extension of the Search command. :token:`qualid` is the
@@ -5686,7 +5686,7 @@ respectively.
 
    local cofix definition
 
-.. tacn:: set @ident {? : @term } := {? @occ_switch } %( @term %| ( @c_pattern) %)
+.. tacn:: set @ident {? : @term } := {? @occ_switch } {| @term | ( @c_pattern) }
 
    abbreviation (see :ref:`abbreviations_ssr`)
 
@@ -5714,26 +5714,26 @@ introduction see :ref:`introduction_ssr`
 
 localization see :ref:`localization_ssr`
 
-.. prodn:: tactic += do {? @mult } %( @tactic %| [ {+| @tactic } ] %)
+.. prodn:: tactic += do {? @mult } {| @tactic | [ {+| @tactic } ] }
 
 iteration  see :ref:`iteration_ssr`
 
-.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } %( @tactic %| [ {+| @tactic } ] %)
+.. prodn:: tactic += @tactic ; {| first | last } {? @num } {| @tactic | [ {+| @tactic } ] }
 
 selector  see :ref:`selectors_ssr`
 
-.. prodn:: tactic += @tactic ; %( first %| last %) {? @num }
+.. prodn:: tactic += @tactic ; {| first | last } {? @num }
 
 rotation see :ref:`selectors_ssr`
 
-.. prodn:: tactic += by %( @tactic %| [ {*| @tactic } ] %)
+.. prodn:: tactic += by {| @tactic | [ {*| @tactic } ] }
 
 closing see :ref:`terminators_ssr`
 
 Commands
 ~~~~~~~~
 
-.. cmd:: Hint View for %( move %| apply %) / @ident {? | @num }
+.. cmd:: Hint View for {| move | apply } / @ident {? | @num }
 
    view hint declaration (see :ref:`declaring_new_hints_ssr`)
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 8d9e99b9d5..4e47621938 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1749,7 +1749,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``,
       and ``in`` clauses.
 
-.. tacn:: case term
+.. tacn:: case @term
    :name: case
 
    The tactic :n:`case` is a more basic tactic to perform case analysis without
@@ -1982,7 +1982,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    :n:`induction @ident; induction @ident` (or
    :n:`induction @ident ; destruct @ident` depending on the exact needs).
 
-.. tacv:: double induction num1 num2
+.. tacv:: double induction @num__1 @num__2
 
    This tactic is deprecated and should be replaced by
    :n:`induction num1; induction num3` where :n:`num3` is the result
@@ -2271,11 +2271,11 @@ and an explanation of the underlying technique.
          :undocumented:
 
    .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern}
-             injection @num as {+ simple_intropattern}
-             injection as {+ simple_intropattern}
-             einjection @term {? with @bindings_list} as {+ simple_intropattern}
-             einjection @num as {+ simple_intropattern}
-             einjection as {+ simple_intropattern}
+             injection @num as {+ @simple_intropattern}
+             injection as {+ @simple_intropattern}
+             einjection @term {? with @bindings_list} as {+ @simple_intropattern}
+             einjection @num as {+ @simple_intropattern}
+             einjection as {+ @simple_intropattern}
 
       These variants apply :n:`intros {+ @simple_intropattern}` after the call to
       :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in
@@ -2637,7 +2637,7 @@ and an explanation of the underlying technique.
    is correct at some time of the interactive development of a proof, use
    the command ``Guarded`` (see Section :ref:`requestinginformation`).
 
-.. tacv:: fix @ident @num with {+ (ident {+ @binder} [{struct @ident}] : @type)}
+.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)}
 
    This starts a proof by mutual induction. The statements to be simultaneously
    proved are respectively :g:`forall binder ... binder, type`.
@@ -3561,7 +3561,7 @@ Automation
 .. tacn:: autorewrite with {+ @ident}
    :name: autorewrite
 
-   This tactic [4]_ carries out rewritings according to the rewriting rule
+   This tactic carries out rewritings according to the rewriting rule
    bases :n:`{+ @ident}`.
 
    Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until
@@ -3777,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       discrimination network to relax or constrain it in the case of discriminated
       databases.
 
-   .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident
-             Hint Constants %( Transparent %| Opaque %) : @ident
+   .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident
+             Hint Constants {| Transparent | Opaque } : @ident
       :name: Hint Variables; Hint Constants
 
       This sets the transparency flag used during unification of
@@ -3850,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       semantics of :n:`Hint Cut @regexp` is to set the cut expression
       to :n:`c | regexp`, the initial cut expression being `emp`.
 
-   .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident
+   .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident
       :name: Hint Mode
 
       This sets an optional mode of use of the identifier :n:`@qualid`. When
@@ -3863,9 +3863,9 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       terms and input heads *must not* contain existential variables or be
       existential variables respectively, while outputs can be any term. Multiple
       modes can be declared for a single identifier, in that case only one mode
-      needs to match the arguments for the hints to be applied.The head of a term
+      needs to match the arguments for the hints to be applied. The head of a term
       is understood here as the applicative head, or the match or projection
-      scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is
+      scrutinee’s head, recursively, casts being ignored. :cmd:`Hint Mode` is
       especially useful for typeclasses, when one does not want to support default
       instances and avoid ambiguity in general. Setting a parameter of a class as an
       input forces proof-search to be driven by that index of the class, with ``!``
@@ -3874,8 +3874,14 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
 
    .. note::
 
-      One can use an ``Extern`` hint with no pattern to do pattern matching on
-      hypotheses using ``match goal with`` inside the tactic.
+      + One can use a :cmd:`Hint Extern` with no pattern to do
+        pattern matching on hypotheses using ``match goal with``
+        inside the tactic.
+
+      + If you want to add hints such as :cmd:`Hint Transparent`,
+        :cmd:`Hint Cut`, or :cmd:`Hint Mode`, for typeclass
+        resolution, do not forget to put them in the
+        ``typeclass_instances`` hint database.
 
 
 Hint databases defined in the Coq standard library
@@ -4010,7 +4016,7 @@ We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior
 option which accepts three flags allowing for a fine-grained handling of
 non-imported hints.
 
-.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %)
+.. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" }
    :name: Loose Hint Behavior
 
    This option accepts three values, which control the behavior of hints w.r.t.
@@ -4042,7 +4048,7 @@ Setting implicit automation tactics
    .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`.
 
 
-   .. cmdv:: Proof with tactic using {+ @ident}
+   .. cmdv:: Proof with @tactic using {+ @ident}
 
       Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
@@ -4394,6 +4400,11 @@ Equality
    This tactic applies to a goal that has the form :g:`t=u` and transforms it
    into the two subgoals :n:`t=@term` and :n:`@term=u`.
 
+   .. tacv:: etransitivity
+
+      This tactic behaves like :tacn:`transitivity`, using a fresh evar instead of
+      a concrete :token:`term`.
+
 
 Equality and inductive sets
 ---------------------------
@@ -4655,9 +4666,12 @@ Non-logical tactics
 
 .. example::
 
-   .. coqtop:: all reset
+   .. coqtop:: none reset
 
       Parameter P : nat -> Prop.
+
+   .. coqtop:: all abort
+
       Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
       repeat split.
       all: cycle 2.
@@ -4673,9 +4687,8 @@ Non-logical tactics
 
 .. example::
 
-   .. coqtop:: reset all
+   .. coqtop:: all abort
 
-      Parameter P : nat -> Prop.
       Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
       repeat split.
       all: swap 1 3.
@@ -4688,9 +4701,8 @@ Non-logical tactics
 
    .. example::
 
-      .. coqtop:: all reset
+      .. coqtop:: all abort
 
-         Parameter P : nat -> Prop.
          Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
          repeat split.
          all: revgoals.
@@ -4711,7 +4723,7 @@ Non-logical tactics
 
       .. example::
 
-         .. coqtop:: all reset
+         .. coqtop:: all abort
 
             Goal exists n, n=0.
             refine (ex_intro _ _ _).
@@ -4740,39 +4752,6 @@ Non-logical tactics
    The ``give_up`` tactic can be used while editing a proof, to choose to
    write the proof script in a non-sequential order.
 
-Simple tactic macros
--------------------------
-
-A simple example has more value than a long explanation:
-
-.. example::
-
-   .. coqtop:: reset all
-
-      Ltac Solve := simpl; intros; auto.
-
-      Ltac ElimBoolRewrite b H1 H2 :=
-      elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ].
-
-The tactics macros are synchronous with the Coq section mechanism: a
-tactic definition is deleted from the current environment when you
-close the section (see also :ref:`section-mechanism`) where it was
-defined. If you want that a tactic macro defined in a module is usable in the
-modules that require it, you should put it outside of any section.
-
-:ref:`ltac` gives examples of more complex
-user-defined tactics.
-
-.. [1] Actually, only the second subgoal will be generated since the
-  other one can be automatically checked.
-.. [2] This corresponds to the cut rule of sequent calculus.
-.. [3] Reminder: opaque constants will not be expanded by δ reductions.
-.. [4] The behavior of this tactic has changed a lot compared to the
-  versions available in the previous distributions (V6). This may cause
-  significant changes in your theories to obtain the same result. As a
-  drawback of the re-engineering of the code, this tactic has also been
-  completely revised to get a very compact and readable version.
-
 Delaying solving unification constraints
 ----------------------------------------
 
@@ -4811,3 +4790,108 @@ references to automatically generated names.
    :name: Mangle Names Prefix
 
    Specifies the prefix to use when generating names.
+
+Performance-oriented tactic variants
+------------------------------------
+
+.. tacn:: change_no_check @term
+   :name: change_no_check
+
+   For advanced usage. Similar to :n:`change @term`, but as an optimization,
+   it skips checking that :n:`@term` is convertible to the goal.
+
+   Recall that the Coq kernel typechecks proofs again when they are concluded to
+   ensure safety. Hence, using :tacn:`change` checks convertibility twice
+   overall, while :tacn:`change_no_check` can produce ill-typed terms,
+   but checks convertibility only once.
+   Hence, :tacn:`change_no_check` can be useful to speed up certain proof
+   scripts, especially if one knows by construction that the argument is
+   indeed convertible to the goal.
+
+   In the following example, :tacn:`change_no_check` replaces :g:`False` by
+   :g:`True`, but :g:`Qed` then rejects the proof, ensuring consistency.
+
+   .. example::
+
+      .. coqtop:: all abort
+
+         Goal False.
+           change_no_check True.
+           exact I.
+         Fail Qed.
+
+   :tacn:`change_no_check` supports all of `change`'s variants.
+
+   .. tacv:: change_no_check @term with @term’
+      :undocumented:
+
+   .. tacv:: change_no_check @term at {+ @num} with @term’
+      :undocumented:
+
+   .. tacv:: change_no_check @term {? {? at {+ @num}} with @term} in @ident
+
+      .. example::
+
+         .. coqtop:: all abort
+
+            Goal True -> False.
+              intro H.
+              change_no_check False in H.
+              exact H.
+            Fail Qed.
+
+   .. tacv:: convert_concl_no_check @term
+      :name: convert_concl_no_check
+
+      Deprecated old name for :tacn:`change_no_check`. Does not support any of its
+      variants.
+
+.. tacn:: exact_no_check @term
+   :name: exact_no_check
+
+   For advanced usage. Similar to :n:`exact @term`, but as an optimization,
+   it skips checking that :n:`@term` has the goal's type, relying on the kernel
+   check instead. See :tacn:`change_no_check` for more explanations.
+
+   .. example::
+
+      .. coqtop:: all abort
+
+         Goal False.
+           exact_no_check I.
+         Fail Qed.
+
+   .. tacv:: vm_cast_no_check @term
+      :name: vm_cast_no_check
+
+      For advanced usage. Similar to :n:`exact_no_check @term`, but additionally
+      instructs the kernel to use :tacn:`vm_compute` to compare the
+      goal's type with the :n:`@term`'s type.
+
+      .. example::
+
+        .. coqtop:: all abort
+
+            Goal False.
+              vm_cast_no_check I.
+            Fail Qed.
+
+   .. tacv:: native_cast_no_check @term
+      :name: native_cast_no_check
+
+      for advanced usage. similar to :n:`exact_no_check @term`, but additionally
+      instructs the kernel to use :tacn:`native_compute` to compare the goal's
+      type with the :n:`@term`'s type.
+
+      .. example::
+
+        .. coqtop:: all abort
+
+            Goal False.
+              native_cast_no_check I.
+            Fail Qed.
+
+.. [1] Actually, only the second subgoal will be generated since the
+  other one can be automatically checked.
+.. [2] This corresponds to the cut rule of sequent calculus.
+.. [3] Reminder: opaque constants will not be expanded by δ reductions.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index e207a072cc..26dc4e02cf 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -91,13 +91,13 @@ and tables:
 Flags, options and tables are identified by a series of identifiers, each with an initial
 capital letter.
 
-.. cmd::  {? Local | Global | Export } Set @flag
+.. cmd::  {? {| Local | Global | Export } } Set @flag
    :name: Set
 
    Sets :token:`flag` on. Scoping qualifiers are
    described :ref:`here <set_unset_scope_qualifiers>`.
 
-.. cmd:: {? Local | Global | Export } Unset @flag
+.. cmd:: {? {| Local | Global | Export } } Unset @flag
    :name: Unset
 
    Sets :token:`flag` off. Scoping qualifiers are
@@ -108,13 +108,13 @@ capital letter.
    Prints the current value of :token:`flag`.
 
 
-.. cmd:: {? Local | Global | Export } Set @option ( @num | @string )
+.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string }
    :name: Set @option
 
    Sets :token:`option` to the specified value.  Scoping qualifiers are
    described :ref:`here <set_unset_scope_qualifiers>`.
 
-.. cmd:: {? Local | Global | Export } Unset @option
+.. cmd:: {? {| Local | Global | Export } } Unset @option
    :name: Unset @option
 
    Sets :token:`option` to its default value.  Scoping qualifiers are
@@ -129,17 +129,17 @@ capital letter.
    Prints the current value of all flags and options, and the names of all tables.
 
 
-.. cmd:: Add @table ( @string | @qualid )
+.. cmd:: Add @table {| @string | @qualid }
    :name: Add @table
 
    Adds the specified value to :token:`table`.
 
-.. cmd:: Remove @table ( @string | @qualid )
+.. cmd:: Remove @table {| @string | @qualid }
    :name: Remove @table
 
    Removes the specified value from :token:`table`.
 
-.. cmd:: Test @table for ( @string | @qualid )
+.. cmd:: Test @table for {| @string | @qualid }
    :name: Test @table for
 
    Reports whether :token:`table` contains the specified value.
@@ -162,7 +162,7 @@ capital letter.
 Scope qualifiers for :cmd:`Set` and :cmd:`Unset`
 `````````````````````````````````````````````````
 
-:n:`{? Local | Global | Export }`
+:n:`{? {| Local | Global | Export } }`
 
 Flag and option settings can be global in scope or local to nested scopes created by
 :cmd:`Module` and :cmd:`Section` commands.  There are four alternatives:
@@ -277,7 +277,7 @@ Requests to the environment
       :token:`term_pattern` (holes of the pattern are either denoted by `_` or by
       :n:`?@ident` when non linear patterns are expected).
 
-   .. cmdv:: Search { + [-]@term_pattern_string }
+   .. cmdv:: Search {+ {? -}@term_pattern_string}
 
       where
       :n:`@term_pattern_string` is a term_pattern, a string, or a string followed
@@ -289,17 +289,17 @@ Requests to the environment
       prefixed by `-`, the search excludes the objects that mention that
       term_pattern or that string.
 
-   .. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid }
+   .. cmdv:: Search {+ {? -}@term_pattern_string} inside {+ @qualid }
 
       This restricts the search to constructions defined in the modules
       named by the given :n:`qualid` sequence.
 
-   .. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid }
+   .. cmdv:: Search {+ {? -}@term_pattern_string} outside {+ @qualid }
 
       This restricts the search to constructions not defined in the modules
       named by the given :n:`qualid` sequence.
 
-   .. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string
+   .. cmdv:: @selector: Search {+ {? -}@term_pattern_string}
 
       This specifies the goal on which to search hypothesis (see
       Section :ref:`invocation-of-tactics`).
@@ -353,7 +353,7 @@ Requests to the environment
       This restricts the search to constructions defined in the modules named
       by the given :n:`qualid` sequence.
 
-   .. cmdv:: SearchHead term outside {+ @qualid }
+   .. cmdv:: SearchHead @term outside {+ @qualid }
 
       This restricts the search to constructions not defined in the modules
       named by the given :n:`qualid` sequence.
@@ -443,7 +443,7 @@ Requests to the environment
 
          SearchRewrite (_ + _ + _).
 
-   .. cmdv:: SearchRewrite term inside {+ @qualid }
+   .. cmdv:: SearchRewrite @term inside {+ @qualid }
 
       This restricts the search to constructions defined in the modules
       named by the given :n:`qualid` sequence.
@@ -622,7 +622,7 @@ file is a particular case of module called *library file*.
       but if a further module, say `A`, contains a command :cmd:`Require Export` `B`,
       then the command :cmd:`Require Import` `A` also imports the module `B.`
 
-   .. cmdv:: Require [Import | Export] {+ @qualid }
+   .. cmdv:: Require {| Import | Export } {+ @qualid }
 
       This loads the
       modules named by the :token:`qualid` sequence and their recursive
@@ -988,7 +988,7 @@ Controlling display
 
    This option controls the normal displaying.
 
-.. opt:: Warnings "{+, {? %( - %| + %) } @ident }"
+.. opt:: Warnings "{+, {? {| - | + } } @ident }"
    :name: Warnings
 
    This option configures the display of warnings. It is experimental, and
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 418922e9b3..3a12ee288a 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -336,29 +336,32 @@ Generation of induction principles with ``Functional`` ``Scheme``
 Generation of inversion principles with ``Derive`` ``Inversion``
 -----------------------------------------------------------------
 
-.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort
+.. cmd:: Derive Inversion @ident with @ident Sort @sort
+         Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort
 
    This command generates an inversion principle for the
-   :tacn:`inversion ... using ...`  tactic. Let :g:`I` be an inductive
-   predicate and :g:`x` the variables occurring in t. This command
-   generates and stocks the inversion lemma for the sort :g:`sort`
-   corresponding to the instance :g:`∀ (x:T), I t` with the name
-   :n:`@ident` in the global environment. When applied, it is
-   equivalent to having inverted the instance with the tactic
-   :g:`inversion`.
-
+   :tacn:`inversion ... using ...` tactic.  The first :token:`ident` is the name
+   of the generated principle.  The second :token:`ident` should be an inductive
+   predicate, and :token:`binders` the variables occurring in the term
+   :token:`term`. This command generates the inversion lemma for the sort
+   :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`.
+   When applied, it is equivalent to having inverted the instance with the
+   tactic :g:`inversion`.
 
-.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort @sort
+.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort
+          Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance with the
    tactic inversion replaced by the tactic `inversion_clear`.
 
-.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort @sort
+.. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort
+          Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance with
    the tactic `dependent inversion`.
 
-.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort @sort
+.. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort
+          Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort
 
    When applied, it is equivalent to having inverted the instance
    with the tactic `dependent inversion_clear`.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 3ca1dda4d6..cda228a7da 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -327,22 +327,29 @@ symbols.
 Reserving notations
 ~~~~~~~~~~~~~~~~~~~
 
-A given notation may be used in different contexts. Coq expects all
-uses of the notation to be defined at the same precedence and with the
-same associativity. To avoid giving the precedence and associativity
-every time, it is possible to declare a parsing rule in advance
-without giving its interpretation. Here is an example from the initial
-state of Coq.
+.. cmd:: Reserved Notation @string {? (@modifiers) }
 
-.. coqtop:: in
+   A given notation may be used in different contexts. Coq expects all
+   uses of the notation to be defined at the same precedence and with the
+   same associativity. To avoid giving the precedence and associativity
+   every time, this command declares a parsing rule (:token:`string`) in advance
+   without giving its interpretation. Here is an example from the initial
+   state of Coq.
+
+   .. coqtop:: in
 
-   Reserved Notation "x = y" (at level 70, no associativity).
+      Reserved Notation "x = y" (at level 70, no associativity).
 
-Reserving a notation is also useful for simultaneously defining an
-inductive type or a recursive constant and a notation for it.
+   Reserving a notation is also useful for simultaneously defining an
+   inductive type or a recursive constant and a notation for it.
 
-.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence
-          their precedence and associativity cannot be changed.
+   .. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence
+             their precedence and associativity cannot be changed.
+
+   .. cmdv:: Reserved Infix "@symbol" {* @modifiers}
+
+      This command declares an infix parsing rule without giving its
+      interpretation.
 
 Simultaneous definition of terms and notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -840,10 +847,11 @@ gives a way to let any arbitrary expression which is not handled by the
 custom entry ``expr`` be parsed or printed by the main grammar of term
 up to the insertion of a pair of curly brackets.
 
-.. cmd:: Print Grammar @ident.
+.. cmd:: Print Custom Grammar @ident.
+   :name: Print Custom Grammar
 
-   This displays the state of the grammar for terms and grammar for
-   patterns associated to the custom entry :token:`ident`.
+   This displays the state of the grammar for terms associated to
+   the custom entry :token:`ident`.
 
 Summary
 ~~~~~~~
@@ -1376,6 +1384,8 @@ Abbreviations
    denoted expression is performed at definition time. Type checking is
    done only at the time of use of the abbreviation.
 
+.. _numeral-notations:
+
 Numeral notations
 -----------------
 
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 0ade9fdbf5..4bdfac7c42 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -39,14 +39,29 @@ from sphinx.ext import mathbase
 from . import coqdoc
 from .repl import ansicolors
 from .repl.coqtop import CoqTop, CoqTopError
+from .notations.parsing import ParseError
 from .notations.sphinx import sphinxify
 from .notations.plain import stringify_with_ellipses
 
-def parse_notation(notation, source, line, rawtext=None):
+PARSE_ERROR = """Parse error in notation!
+Offending notation: {}
+Error message: {}"""
+
+def notation_to_sphinx(notation, source, line, rawtext=None):
     """Parse notation and wrap it in an inline node"""
-    node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation'])
-    node.source, node.line = source, line
-    return node
+    try:
+        node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation'])
+        node.source, node.line = source, line
+        return node
+    except ParseError as e:
+        raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e
+
+def notation_to_string(notation):
+    """Parse notation and format it as a string with ellipses."""
+    try:
+        return stringify_with_ellipses(notation)
+    except ParseError as e:
+        raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e
 
 def highlight_using_coqdoc(sentence):
     """Lex sentence using coqdoc, and yield inline nodes for each token"""
@@ -136,7 +151,7 @@ class CoqObject(ObjectDescription):
         self._render_signature(signature, signode)
         name = self._names.get(signature)
         if name is None:
-            name = self._name_from_signature(signature)
+            name = self._name_from_signature(signature) # pylint: disable=assignment-from-none
             # remove trailing ‘.’ found in commands, but not ‘...’ (ellipsis)
             if name is not None and name.endswith(".") and not name.endswith("..."):
                 name = name[:-1]
@@ -241,7 +256,7 @@ class NotationObject(DocumentableObject):
     """
     def _render_signature(self, signature, signode):
         position = self.state_machine.get_source_and_line(self.lineno)
-        tacn_node = parse_notation(signature, *position)
+        tacn_node = notation_to_sphinx(signature, *position)
         signode += addnodes.desc_name(signature, '', tacn_node)
 
 class GallinaObject(PlainObject):
@@ -346,7 +361,7 @@ class OptionObject(NotationObject):
     annotation = "Option"
 
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 
 class FlagObject(NotationObject):
@@ -365,7 +380,7 @@ class FlagObject(NotationObject):
     annotation = "Flag"
 
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 
 class TableObject(NotationObject):
@@ -383,7 +398,7 @@ class TableObject(NotationObject):
     annotation = "Table"
 
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 class ProductionObject(CoqObject):
     r"""A grammar production.
@@ -403,7 +418,7 @@ class ProductionObject(CoqObject):
     Example::
 
         .. prodn:: term += let: @pattern := @term in @term
-        .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+        .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
 
     """
     subdomain = "prodn"
@@ -432,7 +447,7 @@ class ProductionObject(CoqObject):
         lhs_node = nodes.literal(lhs_op, lhs_op)
 
         position = self.state_machine.get_source_and_line(self.lineno)
-        rhs_node = parse_notation(rhs, *position)
+        rhs_node = notation_to_sphinx(rhs, *position)
         signode += addnodes.desc_name(signature, '', lhs_node, rhs_node)
 
         return ('token', lhs) if op == '::=' else None
@@ -475,7 +490,7 @@ class ExceptionObject(NotationObject):
 
     # Generate names automatically
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 class WarningObject(NotationObject):
     """An warning raised by a Coq command or tactic..
@@ -497,7 +512,7 @@ class WarningObject(NotationObject):
 
     # Generate names automatically
     def _name_from_signature(self, signature):
-        return stringify_with_ellipses(signature)
+        return notation_to_string(signature)
 
 def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
     #pylint: disable=unused-argument, dangerous-default-value
@@ -516,7 +531,7 @@ def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
     """
     notation = utils.unescape(text, 1)
     position = inliner.reporter.get_source_and_line(lineno)
-    return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], []
+    return [nodes.literal(rawtext, '', notation_to_sphinx(notation, *position, rawtext=rawtext))], []
 
 def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]):
     #pylint: disable=dangerous-default-value
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g
index a889ebda7b..01c656eb23 100644
--- a/doc/tools/coqrst/notations/TacticNotations.g
+++ b/doc/tools/coqrst/notations/TacticNotations.g
@@ -13,21 +13,38 @@ grammar TacticNotations;
 // needs rendering (in particular whitespace (kept in output) vs. WHITESPACE
 // (discarded)).
 
+// The distinction between nopipeblock and block is needed because we only want
+// to require escaping within alternative blocks, so that e.g. `first [ x | y ]`
+// can be written without escaping the `|`.
+
 top: blocks EOF;
 blocks: block ((whitespace)? block)*;
-block: atomic | meta | hole | repeat | curlies;
-repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE;
+
+block: pipe | nopipeblock;
+nopipeblock: atomic | escaped | hole | alternative | repeat | curlies;
+
+alternative: LALT (WHITESPACE)? altblocks (WHITESPACE)? RBRACE;
+altblocks: altblock ((WHITESPACE)? altsep (WHITESPACE)? altblock)+;
+altblock: nopipeblock ((whitespace)? nopipeblock)*;
+
+repeat: LGROUP (ATOM | PIPE)? WHITESPACE blocks (WHITESPACE)? RBRACE;
 curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE;
+
+pipe: PIPE;
+altsep: PIPE;
 whitespace: WHITESPACE;
-meta: METACHAR;
+escaped: ESCAPED;
 atomic: ATOM (SUB)?;
 hole: ID (SUB)?;
 
-LGROUP: '{' [+*?];
+
+LALT: '{|';
+LGROUP: '{+' | '{*' | '{?';
 LBRACE: '{';
 RBRACE: '}';
-METACHAR: '%' [|(){}];
-ATOM: '@' | '_' | ~[@_{} ]+;
+ESCAPED: '%{' | '%}' | '%|';
+PIPE: '|';
+ATOM: '@' | '_' | ~[@_{}| ]+;
 ID: '@' ('_'? [a-zA-Z0-9])+;
 SUB: '_' '_' [a-zA-Z0-9]+;
 WHITESPACE: ' '+;
diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens
index 88b38f97a6..2670e20aa6 100644
--- a/doc/tools/coqrst/notations/TacticNotations.tokens
+++ b/doc/tools/coqrst/notations/TacticNotations.tokens
@@ -1,10 +1,14 @@
-LGROUP=1
-LBRACE=2
-RBRACE=3
-METACHAR=4
-ATOM=5
-ID=6
-SUB=7
-WHITESPACE=8
-'{'=2
-'}'=3
+LALT=1
+LGROUP=2
+LBRACE=3
+RBRACE=4
+ESCAPED=5
+PIPE=6
+ATOM=7
+ID=8
+SUB=9
+WHITESPACE=10
+'{|'=1
+'{'=3
+'}'=4
+'|'=6
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py
index 27293e7e09..e3a115e32a 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.py
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py
@@ -1,4 +1,4 @@
-# Generated from TacticNotations.g by ANTLR 4.7
+# Generated from TacticNotations.g by ANTLR 4.7.2
 from antlr4 import *
 from io import StringIO
 from typing.io import TextIO
@@ -7,28 +7,34 @@ import sys
 
 def serializedATN():
     with StringIO() as buf:
-        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\n")
-        buf.write(":\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
-        buf.write("\4\b\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3")
-        buf.write("\5\3\6\3\6\6\6 \n\6\r\6\16\6!\5\6$\n\6\3\7\3\7\5\7(\n")
-        buf.write("\7\3\7\6\7+\n\7\r\7\16\7,\3\b\3\b\3\b\6\b\62\n\b\r\b\16")
-        buf.write("\b\63\3\t\6\t\67\n\t\r\t\16\t8\2\2\n\3\3\5\4\7\5\t\6\13")
-        buf.write("\7\r\b\17\t\21\n\3\2\7\4\2,-AA\4\2*+}\177\4\2BBaa\7\2")
-        buf.write("\"\"BBaa}}\177\177\5\2\62;C\\c|\2?\2\3\3\2\2\2\2\5\3\2")
-        buf.write("\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2")
-        buf.write("\2\17\3\2\2\2\2\21\3\2\2\2\3\23\3\2\2\2\5\26\3\2\2\2\7")
-        buf.write("\30\3\2\2\2\t\32\3\2\2\2\13#\3\2\2\2\r%\3\2\2\2\17.\3")
-        buf.write("\2\2\2\21\66\3\2\2\2\23\24\7}\2\2\24\25\t\2\2\2\25\4\3")
-        buf.write("\2\2\2\26\27\7}\2\2\27\6\3\2\2\2\30\31\7\177\2\2\31\b")
-        buf.write("\3\2\2\2\32\33\7\'\2\2\33\34\t\3\2\2\34\n\3\2\2\2\35$")
-        buf.write("\t\4\2\2\36 \n\5\2\2\37\36\3\2\2\2 !\3\2\2\2!\37\3\2\2")
-        buf.write("\2!\"\3\2\2\2\"$\3\2\2\2#\35\3\2\2\2#\37\3\2\2\2$\f\3")
-        buf.write("\2\2\2%*\7B\2\2&(\7a\2\2\'&\3\2\2\2\'(\3\2\2\2()\3\2\2")
-        buf.write("\2)+\t\6\2\2*\'\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2")
-        buf.write("-\16\3\2\2\2./\7a\2\2/\61\7a\2\2\60\62\t\6\2\2\61\60\3")
-        buf.write("\2\2\2\62\63\3\2\2\2\63\61\3\2\2\2\63\64\3\2\2\2\64\20")
-        buf.write("\3\2\2\2\65\67\7\"\2\2\66\65\3\2\2\2\678\3\2\2\28\66\3")
-        buf.write("\2\2\289\3\2\2\29\22\3\2\2\2\t\2!#\',\638\2")
+        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\f")
+        buf.write("M\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
+        buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\3\2\3\2\3\2\3\3\3\3")
+        buf.write("\3\3\3\3\3\3\3\3\5\3!\n\3\3\4\3\4\3\5\3\5\3\6\3\6\3\6")
+        buf.write("\3\6\3\6\3\6\5\6-\n\6\3\7\3\7\3\b\3\b\6\b\63\n\b\r\b\16")
+        buf.write("\b\64\5\b\67\n\b\3\t\3\t\5\t;\n\t\3\t\6\t>\n\t\r\t\16")
+        buf.write("\t?\3\n\3\n\3\n\6\nE\n\n\r\n\16\nF\3\13\6\13J\n\13\r\13")
+        buf.write("\16\13K\2\2\f\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13")
+        buf.write("\25\f\3\2\5\4\2BBaa\6\2\"\"BBaa}\177\5\2\62;C\\c|\2V\2")
+        buf.write("\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3")
+        buf.write("\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2")
+        buf.write("\2\2\2\25\3\2\2\2\3\27\3\2\2\2\5 \3\2\2\2\7\"\3\2\2\2")
+        buf.write("\t$\3\2\2\2\13,\3\2\2\2\r.\3\2\2\2\17\66\3\2\2\2\218\3")
+        buf.write("\2\2\2\23A\3\2\2\2\25I\3\2\2\2\27\30\7}\2\2\30\31\7~\2")
+        buf.write("\2\31\4\3\2\2\2\32\33\7}\2\2\33!\7-\2\2\34\35\7}\2\2\35")
+        buf.write("!\7,\2\2\36\37\7}\2\2\37!\7A\2\2 \32\3\2\2\2 \34\3\2\2")
+        buf.write("\2 \36\3\2\2\2!\6\3\2\2\2\"#\7}\2\2#\b\3\2\2\2$%\7\177")
+        buf.write("\2\2%\n\3\2\2\2&\'\7\'\2\2\'-\7}\2\2()\7\'\2\2)-\7\177")
+        buf.write("\2\2*+\7\'\2\2+-\7~\2\2,&\3\2\2\2,(\3\2\2\2,*\3\2\2\2")
+        buf.write("-\f\3\2\2\2./\7~\2\2/\16\3\2\2\2\60\67\t\2\2\2\61\63\n")
+        buf.write("\3\2\2\62\61\3\2\2\2\63\64\3\2\2\2\64\62\3\2\2\2\64\65")
+        buf.write("\3\2\2\2\65\67\3\2\2\2\66\60\3\2\2\2\66\62\3\2\2\2\67")
+        buf.write("\20\3\2\2\28=\7B\2\29;\7a\2\2:9\3\2\2\2:;\3\2\2\2;<\3")
+        buf.write("\2\2\2<>\t\4\2\2=:\3\2\2\2>?\3\2\2\2?=\3\2\2\2?@\3\2\2")
+        buf.write("\2@\22\3\2\2\2AB\7a\2\2BD\7a\2\2CE\t\4\2\2DC\3\2\2\2E")
+        buf.write("F\3\2\2\2FD\3\2\2\2FG\3\2\2\2G\24\3\2\2\2HJ\7\"\2\2IH")
+        buf.write("\3\2\2\2JK\3\2\2\2KI\3\2\2\2KL\3\2\2\2L\26\3\2\2\2\13")
+        buf.write("\2 ,\64\66:?FK\2")
         return buf.getvalue()
 
 
@@ -38,34 +44,36 @@ class TacticNotationsLexer(Lexer):
 
     decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ]
 
-    LGROUP = 1
-    LBRACE = 2
-    RBRACE = 3
-    METACHAR = 4
-    ATOM = 5
-    ID = 6
-    SUB = 7
-    WHITESPACE = 8
+    LALT = 1
+    LGROUP = 2
+    LBRACE = 3
+    RBRACE = 4
+    ESCAPED = 5
+    PIPE = 6
+    ATOM = 7
+    ID = 8
+    SUB = 9
+    WHITESPACE = 10
 
     channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ]
 
     modeNames = [ "DEFAULT_MODE" ]
 
     literalNames = [ "<INVALID>",
-            "'{'", "'}'" ]
+            "'{|'", "'{'", "'}'", "'|'" ]
 
     symbolicNames = [ "<INVALID>",
-            "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "SUB",
-            "WHITESPACE" ]
+            "LALT", "LGROUP", "LBRACE", "RBRACE", "ESCAPED", "PIPE", "ATOM",
+            "ID", "SUB", "WHITESPACE" ]
 
-    ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID",
-                  "SUB", "WHITESPACE" ]
+    ruleNames = [ "LALT", "LGROUP", "LBRACE", "RBRACE", "ESCAPED", "PIPE",
+                  "ATOM", "ID", "SUB", "WHITESPACE" ]
 
     grammarFileName = "TacticNotations.g"
 
     def __init__(self, input=None, output:TextIO = sys.stdout):
         super().__init__(input, output)
-        self.checkVersion("4.7")
+        self.checkVersion("4.7.2")
         self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache())
         self._actions = None
         self._predicates = None
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
index 88b38f97a6..2670e20aa6 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
@@ -1,10 +1,14 @@
-LGROUP=1
-LBRACE=2
-RBRACE=3
-METACHAR=4
-ATOM=5
-ID=6
-SUB=7
-WHITESPACE=8
-'{'=2
-'}'=3
+LALT=1
+LGROUP=2
+LBRACE=3
+RBRACE=4
+ESCAPED=5
+PIPE=6
+ATOM=7
+ID=8
+SUB=9
+WHITESPACE=10
+'{|'=1
+'{'=3
+'}'=4
+'|'=6
diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py
index 645f078979..4a2a73672a 100644
--- a/doc/tools/coqrst/notations/TacticNotationsParser.py
+++ b/doc/tools/coqrst/notations/TacticNotationsParser.py
@@ -1,4 +1,4 @@
-# Generated from TacticNotations.g by ANTLR 4.7
+# Generated from TacticNotations.g by ANTLR 4.7.2
 # encoding: utf-8
 from antlr4 import *
 from io import StringIO
@@ -7,31 +7,47 @@ import sys
 
 def serializedATN():
     with StringIO() as buf:
-        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\n")
-        buf.write("J\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b")
-        buf.write("\t\b\4\t\t\t\4\n\t\n\3\2\3\2\3\2\3\3\3\3\5\3\32\n\3\3")
-        buf.write("\3\7\3\35\n\3\f\3\16\3 \13\3\3\4\3\4\3\4\3\4\3\4\5\4\'")
-        buf.write("\n\4\3\5\3\5\5\5+\n\5\3\5\3\5\3\5\5\5\60\n\5\3\5\3\5\3")
-        buf.write("\6\3\6\5\6\66\n\6\3\6\3\6\5\6:\n\6\3\6\3\6\3\7\3\7\3\b")
-        buf.write("\3\b\3\t\3\t\5\tD\n\t\3\n\3\n\5\nH\n\n\3\n\2\2\13\2\4")
-        buf.write("\6\b\n\f\16\20\22\2\2\2L\2\24\3\2\2\2\4\27\3\2\2\2\6&")
-        buf.write("\3\2\2\2\b(\3\2\2\2\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2")
-        buf.write("\2\20A\3\2\2\2\22E\3\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3")
-        buf.write("\26\3\3\2\2\2\27\36\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2")
-        buf.write("\2\31\32\3\2\2\2\32\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2")
-        buf.write("\2\2\35 \3\2\2\2\36\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2")
-        buf.write("\2\2 \36\3\2\2\2!\'\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2")
-        buf.write("$\'\5\b\5\2%\'\5\n\6\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2")
-        buf.write("&$\3\2\2\2&%\3\2\2\2\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*")
-        buf.write(")\3\2\2\2*+\3\2\2\2+,\3\2\2\2,-\7\n\2\2-/\5\4\3\2.\60")
-        buf.write("\7\n\2\2/.\3\2\2\2/\60\3\2\2\2\60\61\3\2\2\2\61\62\7\5")
-        buf.write("\2\2\62\t\3\2\2\2\63\65\7\4\2\2\64\66\5\f\7\2\65\64\3")
-        buf.write("\2\2\2\65\66\3\2\2\2\66\67\3\2\2\2\679\5\4\3\28:\5\f\7")
-        buf.write("\298\3\2\2\29:\3\2\2\2:;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2")
-        buf.write("=>\7\n\2\2>\r\3\2\2\2?@\7\6\2\2@\17\3\2\2\2AC\7\7\2\2")
-        buf.write("BD\7\t\2\2CB\3\2\2\2CD\3\2\2\2D\21\3\2\2\2EG\7\b\2\2F")
-        buf.write("H\7\t\2\2GF\3\2\2\2GH\3\2\2\2H\23\3\2\2\2\13\31\36&*/")
-        buf.write("\659CG")
+        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\f")
+        buf.write("\u0081\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
+        buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\4\f\t\f\4\r\t\r\4\16")
+        buf.write("\t\16\4\17\t\17\4\20\t\20\3\2\3\2\3\2\3\3\3\3\5\3&\n\3")
+        buf.write("\3\3\7\3)\n\3\f\3\16\3,\13\3\3\4\3\4\5\4\60\n\4\3\5\3")
+        buf.write("\5\3\5\3\5\3\5\3\5\5\58\n\5\3\6\3\6\5\6<\n\6\3\6\3\6\5")
+        buf.write("\6@\n\6\3\6\3\6\3\7\3\7\5\7F\n\7\3\7\3\7\5\7J\n\7\3\7")
+        buf.write("\3\7\6\7N\n\7\r\7\16\7O\3\b\3\b\5\bT\n\b\3\b\7\bW\n\b")
+        buf.write("\f\b\16\bZ\13\b\3\t\3\t\5\t^\n\t\3\t\3\t\3\t\5\tc\n\t")
+        buf.write("\3\t\3\t\3\n\3\n\5\ni\n\n\3\n\3\n\5\nm\n\n\3\n\3\n\3\13")
+        buf.write("\3\13\3\f\3\f\3\r\3\r\3\16\3\16\3\17\3\17\5\17{\n\17\3")
+        buf.write("\20\3\20\5\20\177\n\20\3\20\2\2\21\2\4\6\b\n\f\16\20\22")
+        buf.write("\24\26\30\32\34\36\2\3\3\2\b\t\2\u0086\2 \3\2\2\2\4#\3")
+        buf.write("\2\2\2\6/\3\2\2\2\b\67\3\2\2\2\n9\3\2\2\2\fC\3\2\2\2\16")
+        buf.write("Q\3\2\2\2\20[\3\2\2\2\22f\3\2\2\2\24p\3\2\2\2\26r\3\2")
+        buf.write("\2\2\30t\3\2\2\2\32v\3\2\2\2\34x\3\2\2\2\36|\3\2\2\2 ")
+        buf.write("!\5\4\3\2!\"\7\2\2\3\"\3\3\2\2\2#*\5\6\4\2$&\5\30\r\2")
+        buf.write("%$\3\2\2\2%&\3\2\2\2&\'\3\2\2\2\')\5\6\4\2(%\3\2\2\2)")
+        buf.write(",\3\2\2\2*(\3\2\2\2*+\3\2\2\2+\5\3\2\2\2,*\3\2\2\2-\60")
+        buf.write("\5\24\13\2.\60\5\b\5\2/-\3\2\2\2/.\3\2\2\2\60\7\3\2\2")
+        buf.write("\2\618\5\34\17\2\628\5\32\16\2\638\5\36\20\2\648\5\n\6")
+        buf.write("\2\658\5\20\t\2\668\5\22\n\2\67\61\3\2\2\2\67\62\3\2\2")
+        buf.write("\2\67\63\3\2\2\2\67\64\3\2\2\2\67\65\3\2\2\2\67\66\3\2")
+        buf.write("\2\28\t\3\2\2\29;\7\3\2\2:<\7\f\2\2;:\3\2\2\2;<\3\2\2")
+        buf.write("\2<=\3\2\2\2=?\5\f\7\2>@\7\f\2\2?>\3\2\2\2?@\3\2\2\2@")
+        buf.write("A\3\2\2\2AB\7\6\2\2B\13\3\2\2\2CM\5\16\b\2DF\7\f\2\2E")
+        buf.write("D\3\2\2\2EF\3\2\2\2FG\3\2\2\2GI\5\26\f\2HJ\7\f\2\2IH\3")
+        buf.write("\2\2\2IJ\3\2\2\2JK\3\2\2\2KL\5\16\b\2LN\3\2\2\2ME\3\2")
+        buf.write("\2\2NO\3\2\2\2OM\3\2\2\2OP\3\2\2\2P\r\3\2\2\2QX\5\b\5")
+        buf.write("\2RT\5\30\r\2SR\3\2\2\2ST\3\2\2\2TU\3\2\2\2UW\5\b\5\2")
+        buf.write("VS\3\2\2\2WZ\3\2\2\2XV\3\2\2\2XY\3\2\2\2Y\17\3\2\2\2Z")
+        buf.write("X\3\2\2\2[]\7\4\2\2\\^\t\2\2\2]\\\3\2\2\2]^\3\2\2\2^_")
+        buf.write("\3\2\2\2_`\7\f\2\2`b\5\4\3\2ac\7\f\2\2ba\3\2\2\2bc\3\2")
+        buf.write("\2\2cd\3\2\2\2de\7\6\2\2e\21\3\2\2\2fh\7\5\2\2gi\5\30")
+        buf.write("\r\2hg\3\2\2\2hi\3\2\2\2ij\3\2\2\2jl\5\4\3\2km\5\30\r")
+        buf.write("\2lk\3\2\2\2lm\3\2\2\2mn\3\2\2\2no\7\6\2\2o\23\3\2\2\2")
+        buf.write("pq\7\b\2\2q\25\3\2\2\2rs\7\b\2\2s\27\3\2\2\2tu\7\f\2\2")
+        buf.write("u\31\3\2\2\2vw\7\7\2\2w\33\3\2\2\2xz\7\t\2\2y{\7\13\2")
+        buf.write("\2zy\3\2\2\2z{\3\2\2\2{\35\3\2\2\2|~\7\n\2\2}\177\7\13")
+        buf.write("\2\2~}\3\2\2\2~\177\3\2\2\2\177\37\3\2\2\2\23%*/\67;?")
+        buf.write("EIOSX]bhlz~")
         return buf.getvalue()
 
 
@@ -45,37 +61,47 @@ class TacticNotationsParser ( Parser ):
 
     sharedContextCache = PredictionContextCache()
 
-    literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ]
+    literalNames = [ "<INVALID>", "'{|'", "<INVALID>", "'{'", "'}'", "<INVALID>",
+                     "'|'" ]
 
-    symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "METACHAR",
-                      "ATOM", "ID", "SUB", "WHITESPACE" ]
+    symbolicNames = [ "<INVALID>", "LALT", "LGROUP", "LBRACE", "RBRACE",
+                      "ESCAPED", "PIPE", "ATOM", "ID", "SUB", "WHITESPACE" ]
 
     RULE_top = 0
     RULE_blocks = 1
     RULE_block = 2
-    RULE_repeat = 3
-    RULE_curlies = 4
-    RULE_whitespace = 5
-    RULE_meta = 6
-    RULE_atomic = 7
-    RULE_hole = 8
-
-    ruleNames =  [ "top", "blocks", "block", "repeat", "curlies", "whitespace",
-                   "meta", "atomic", "hole" ]
+    RULE_nopipeblock = 3
+    RULE_alternative = 4
+    RULE_altblocks = 5
+    RULE_altblock = 6
+    RULE_repeat = 7
+    RULE_curlies = 8
+    RULE_pipe = 9
+    RULE_altsep = 10
+    RULE_whitespace = 11
+    RULE_escaped = 12
+    RULE_atomic = 13
+    RULE_hole = 14
+
+    ruleNames =  [ "top", "blocks", "block", "nopipeblock", "alternative",
+                   "altblocks", "altblock", "repeat", "curlies", "pipe",
+                   "altsep", "whitespace", "escaped", "atomic", "hole" ]
 
     EOF = Token.EOF
-    LGROUP=1
-    LBRACE=2
-    RBRACE=3
-    METACHAR=4
-    ATOM=5
-    ID=6
-    SUB=7
-    WHITESPACE=8
+    LALT=1
+    LGROUP=2
+    LBRACE=3
+    RBRACE=4
+    ESCAPED=5
+    PIPE=6
+    ATOM=7
+    ID=8
+    SUB=9
+    WHITESPACE=10
 
     def __init__(self, input:TokenStream, output:TextIO = sys.stdout):
         super().__init__(input, output)
-        self.checkVersion("4.7")
+        self.checkVersion("4.7.2")
         self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache)
         self._predicates = None
 
@@ -112,9 +138,9 @@ class TacticNotationsParser ( Parser ):
         self.enterRule(localctx, 0, self.RULE_top)
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 18
+            self.state = 30
             self.blocks()
-            self.state = 19
+            self.state = 31
             self.match(TacticNotationsParser.EOF)
         except RecognitionException as re:
             localctx.exception = re
@@ -163,24 +189,24 @@ class TacticNotationsParser ( Parser ):
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 21
+            self.state = 33
             self.block()
-            self.state = 28
+            self.state = 40
             self._errHandler.sync(self)
             _alt = self._interp.adaptivePredict(self._input,1,self._ctx)
             while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER:
                 if _alt==1:
-                    self.state = 23
+                    self.state = 35
                     self._errHandler.sync(self)
                     _la = self._input.LA(1)
                     if _la==TacticNotationsParser.WHITESPACE:
-                        self.state = 22
+                        self.state = 34
                         self.whitespace()
 
 
-                    self.state = 25
+                    self.state = 37
                     self.block()
-                self.state = 30
+                self.state = 42
                 self._errHandler.sync(self)
                 _alt = self._interp.adaptivePredict(self._input,1,self._ctx)
 
@@ -198,18 +224,77 @@ class TacticNotationsParser ( Parser ):
             super().__init__(parent, invokingState)
             self.parser = parser
 
+        def pipe(self):
+            return self.getTypedRuleContext(TacticNotationsParser.PipeContext,0)
+
+
+        def nopipeblock(self):
+            return self.getTypedRuleContext(TacticNotationsParser.NopipeblockContext,0)
+
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_block
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitBlock" ):
+                return visitor.visitBlock(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def block(self):
+
+        localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 4, self.RULE_block)
+        try:
+            self.state = 45
+            self._errHandler.sync(self)
+            token = self._input.LA(1)
+            if token in [TacticNotationsParser.PIPE]:
+                self.enterOuterAlt(localctx, 1)
+                self.state = 43
+                self.pipe()
+                pass
+            elif token in [TacticNotationsParser.LALT, TacticNotationsParser.LGROUP, TacticNotationsParser.LBRACE, TacticNotationsParser.ESCAPED, TacticNotationsParser.ATOM, TacticNotationsParser.ID]:
+                self.enterOuterAlt(localctx, 2)
+                self.state = 44
+                self.nopipeblock()
+                pass
+            else:
+                raise NoViableAltException(self)
+
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class NopipeblockContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
         def atomic(self):
             return self.getTypedRuleContext(TacticNotationsParser.AtomicContext,0)
 
 
-        def meta(self):
-            return self.getTypedRuleContext(TacticNotationsParser.MetaContext,0)
+        def escaped(self):
+            return self.getTypedRuleContext(TacticNotationsParser.EscapedContext,0)
 
 
         def hole(self):
             return self.getTypedRuleContext(TacticNotationsParser.HoleContext,0)
 
 
+        def alternative(self):
+            return self.getTypedRuleContext(TacticNotationsParser.AlternativeContext,0)
+
+
         def repeat(self):
             return self.getTypedRuleContext(TacticNotationsParser.RepeatContext,0)
 
@@ -219,48 +304,53 @@ class TacticNotationsParser ( Parser ):
 
 
         def getRuleIndex(self):
-            return TacticNotationsParser.RULE_block
+            return TacticNotationsParser.RULE_nopipeblock
 
         def accept(self, visitor:ParseTreeVisitor):
-            if hasattr( visitor, "visitBlock" ):
-                return visitor.visitBlock(self)
+            if hasattr( visitor, "visitNopipeblock" ):
+                return visitor.visitNopipeblock(self)
             else:
                 return visitor.visitChildren(self)
 
 
 
 
-    def block(self):
+    def nopipeblock(self):
 
-        localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 4, self.RULE_block)
+        localctx = TacticNotationsParser.NopipeblockContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 6, self.RULE_nopipeblock)
         try:
-            self.state = 36
+            self.state = 53
             self._errHandler.sync(self)
             token = self._input.LA(1)
             if token in [TacticNotationsParser.ATOM]:
                 self.enterOuterAlt(localctx, 1)
-                self.state = 31
+                self.state = 47
                 self.atomic()
                 pass
-            elif token in [TacticNotationsParser.METACHAR]:
+            elif token in [TacticNotationsParser.ESCAPED]:
                 self.enterOuterAlt(localctx, 2)
-                self.state = 32
-                self.meta()
+                self.state = 48
+                self.escaped()
                 pass
             elif token in [TacticNotationsParser.ID]:
                 self.enterOuterAlt(localctx, 3)
-                self.state = 33
+                self.state = 49
                 self.hole()
                 pass
-            elif token in [TacticNotationsParser.LGROUP]:
+            elif token in [TacticNotationsParser.LALT]:
                 self.enterOuterAlt(localctx, 4)
-                self.state = 34
+                self.state = 50
+                self.alternative()
+                pass
+            elif token in [TacticNotationsParser.LGROUP]:
+                self.enterOuterAlt(localctx, 5)
+                self.state = 51
                 self.repeat()
                 pass
             elif token in [TacticNotationsParser.LBRACE]:
-                self.enterOuterAlt(localctx, 5)
-                self.state = 35
+                self.enterOuterAlt(localctx, 6)
+                self.state = 52
                 self.curlies()
                 pass
             else:
@@ -274,6 +364,232 @@ class TacticNotationsParser ( Parser ):
             self.exitRule()
         return localctx
 
+    class AlternativeContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def LALT(self):
+            return self.getToken(TacticNotationsParser.LALT, 0)
+
+        def altblocks(self):
+            return self.getTypedRuleContext(TacticNotationsParser.AltblocksContext,0)
+
+
+        def RBRACE(self):
+            return self.getToken(TacticNotationsParser.RBRACE, 0)
+
+        def WHITESPACE(self, i:int=None):
+            if i is None:
+                return self.getTokens(TacticNotationsParser.WHITESPACE)
+            else:
+                return self.getToken(TacticNotationsParser.WHITESPACE, i)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_alternative
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitAlternative" ):
+                return visitor.visitAlternative(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def alternative(self):
+
+        localctx = TacticNotationsParser.AlternativeContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 8, self.RULE_alternative)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 55
+            self.match(TacticNotationsParser.LALT)
+            self.state = 57
+            self._errHandler.sync(self)
+            _la = self._input.LA(1)
+            if _la==TacticNotationsParser.WHITESPACE:
+                self.state = 56
+                self.match(TacticNotationsParser.WHITESPACE)
+
+
+            self.state = 59
+            self.altblocks()
+            self.state = 61
+            self._errHandler.sync(self)
+            _la = self._input.LA(1)
+            if _la==TacticNotationsParser.WHITESPACE:
+                self.state = 60
+                self.match(TacticNotationsParser.WHITESPACE)
+
+
+            self.state = 63
+            self.match(TacticNotationsParser.RBRACE)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class AltblocksContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def altblock(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.AltblockContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.AltblockContext,i)
+
+
+        def altsep(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.AltsepContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.AltsepContext,i)
+
+
+        def WHITESPACE(self, i:int=None):
+            if i is None:
+                return self.getTokens(TacticNotationsParser.WHITESPACE)
+            else:
+                return self.getToken(TacticNotationsParser.WHITESPACE, i)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_altblocks
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitAltblocks" ):
+                return visitor.visitAltblocks(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def altblocks(self):
+
+        localctx = TacticNotationsParser.AltblocksContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 10, self.RULE_altblocks)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 65
+            self.altblock()
+            self.state = 75
+            self._errHandler.sync(self)
+            _alt = 1
+            while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER:
+                if _alt == 1:
+                    self.state = 67
+                    self._errHandler.sync(self)
+                    _la = self._input.LA(1)
+                    if _la==TacticNotationsParser.WHITESPACE:
+                        self.state = 66
+                        self.match(TacticNotationsParser.WHITESPACE)
+
+
+                    self.state = 69
+                    self.altsep()
+                    self.state = 71
+                    self._errHandler.sync(self)
+                    _la = self._input.LA(1)
+                    if _la==TacticNotationsParser.WHITESPACE:
+                        self.state = 70
+                        self.match(TacticNotationsParser.WHITESPACE)
+
+
+                    self.state = 73
+                    self.altblock()
+
+                else:
+                    raise NoViableAltException(self)
+                self.state = 77
+                self._errHandler.sync(self)
+                _alt = self._interp.adaptivePredict(self._input,8,self._ctx)
+
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class AltblockContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def nopipeblock(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.NopipeblockContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.NopipeblockContext,i)
+
+
+        def whitespace(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.WhitespaceContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.WhitespaceContext,i)
+
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_altblock
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitAltblock" ):
+                return visitor.visitAltblock(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def altblock(self):
+
+        localctx = TacticNotationsParser.AltblockContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 12, self.RULE_altblock)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 79
+            self.nopipeblock()
+            self.state = 86
+            self._errHandler.sync(self)
+            _alt = self._interp.adaptivePredict(self._input,10,self._ctx)
+            while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER:
+                if _alt==1:
+                    self.state = 81
+                    self._errHandler.sync(self)
+                    _la = self._input.LA(1)
+                    if _la==TacticNotationsParser.WHITESPACE:
+                        self.state = 80
+                        self.whitespace()
+
+
+                    self.state = 83
+                    self.nopipeblock()
+                self.state = 88
+                self._errHandler.sync(self)
+                _alt = self._interp.adaptivePredict(self._input,10,self._ctx)
+
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
     class RepeatContext(ParserRuleContext):
 
         def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
@@ -299,6 +615,9 @@ class TacticNotationsParser ( Parser ):
         def ATOM(self):
             return self.getToken(TacticNotationsParser.ATOM, 0)
 
+        def PIPE(self):
+            return self.getToken(TacticNotationsParser.PIPE, 0)
+
         def getRuleIndex(self):
             return TacticNotationsParser.RULE_repeat
 
@@ -314,33 +633,38 @@ class TacticNotationsParser ( Parser ):
     def repeat(self):
 
         localctx = TacticNotationsParser.RepeatContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 6, self.RULE_repeat)
+        self.enterRule(localctx, 14, self.RULE_repeat)
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 38
+            self.state = 89
             self.match(TacticNotationsParser.LGROUP)
-            self.state = 40
+            self.state = 91
             self._errHandler.sync(self)
             _la = self._input.LA(1)
-            if _la==TacticNotationsParser.ATOM:
-                self.state = 39
-                self.match(TacticNotationsParser.ATOM)
+            if _la==TacticNotationsParser.PIPE or _la==TacticNotationsParser.ATOM:
+                self.state = 90
+                _la = self._input.LA(1)
+                if not(_la==TacticNotationsParser.PIPE or _la==TacticNotationsParser.ATOM):
+                    self._errHandler.recoverInline(self)
+                else:
+                    self._errHandler.reportMatch(self)
+                    self.consume()
 
 
-            self.state = 42
+            self.state = 93
             self.match(TacticNotationsParser.WHITESPACE)
-            self.state = 43
+            self.state = 94
             self.blocks()
-            self.state = 45
+            self.state = 96
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.WHITESPACE:
-                self.state = 44
+                self.state = 95
                 self.match(TacticNotationsParser.WHITESPACE)
 
 
-            self.state = 47
+            self.state = 98
             self.match(TacticNotationsParser.RBRACE)
         except RecognitionException as re:
             localctx.exception = re
@@ -388,31 +712,31 @@ class TacticNotationsParser ( Parser ):
     def curlies(self):
 
         localctx = TacticNotationsParser.CurliesContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 8, self.RULE_curlies)
+        self.enterRule(localctx, 16, self.RULE_curlies)
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 49
+            self.state = 100
             self.match(TacticNotationsParser.LBRACE)
-            self.state = 51
+            self.state = 102
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.WHITESPACE:
-                self.state = 50
+                self.state = 101
                 self.whitespace()
 
 
-            self.state = 53
+            self.state = 104
             self.blocks()
-            self.state = 55
+            self.state = 106
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.WHITESPACE:
-                self.state = 54
+                self.state = 105
                 self.whitespace()
 
 
-            self.state = 57
+            self.state = 108
             self.match(TacticNotationsParser.RBRACE)
         except RecognitionException as re:
             localctx.exception = re
@@ -422,6 +746,80 @@ class TacticNotationsParser ( Parser ):
             self.exitRule()
         return localctx
 
+    class PipeContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def PIPE(self):
+            return self.getToken(TacticNotationsParser.PIPE, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_pipe
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitPipe" ):
+                return visitor.visitPipe(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def pipe(self):
+
+        localctx = TacticNotationsParser.PipeContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 18, self.RULE_pipe)
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 110
+            self.match(TacticNotationsParser.PIPE)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class AltsepContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def PIPE(self):
+            return self.getToken(TacticNotationsParser.PIPE, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_altsep
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitAltsep" ):
+                return visitor.visitAltsep(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def altsep(self):
+
+        localctx = TacticNotationsParser.AltsepContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 20, self.RULE_altsep)
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 112
+            self.match(TacticNotationsParser.PIPE)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
     class WhitespaceContext(ParserRuleContext):
 
         def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
@@ -446,10 +844,10 @@ class TacticNotationsParser ( Parser ):
     def whitespace(self):
 
         localctx = TacticNotationsParser.WhitespaceContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 10, self.RULE_whitespace)
+        self.enterRule(localctx, 22, self.RULE_whitespace)
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 59
+            self.state = 114
             self.match(TacticNotationsParser.WHITESPACE)
         except RecognitionException as re:
             localctx.exception = re
@@ -459,35 +857,35 @@ class TacticNotationsParser ( Parser ):
             self.exitRule()
         return localctx
 
-    class MetaContext(ParserRuleContext):
+    class EscapedContext(ParserRuleContext):
 
         def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
             super().__init__(parent, invokingState)
             self.parser = parser
 
-        def METACHAR(self):
-            return self.getToken(TacticNotationsParser.METACHAR, 0)
+        def ESCAPED(self):
+            return self.getToken(TacticNotationsParser.ESCAPED, 0)
 
         def getRuleIndex(self):
-            return TacticNotationsParser.RULE_meta
+            return TacticNotationsParser.RULE_escaped
 
         def accept(self, visitor:ParseTreeVisitor):
-            if hasattr( visitor, "visitMeta" ):
-                return visitor.visitMeta(self)
+            if hasattr( visitor, "visitEscaped" ):
+                return visitor.visitEscaped(self)
             else:
                 return visitor.visitChildren(self)
 
 
 
 
-    def meta(self):
+    def escaped(self):
 
-        localctx = TacticNotationsParser.MetaContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 12, self.RULE_meta)
+        localctx = TacticNotationsParser.EscapedContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 24, self.RULE_escaped)
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 61
-            self.match(TacticNotationsParser.METACHAR)
+            self.state = 116
+            self.match(TacticNotationsParser.ESCAPED)
         except RecognitionException as re:
             localctx.exception = re
             self._errHandler.reportError(self, re)
@@ -523,17 +921,17 @@ class TacticNotationsParser ( Parser ):
     def atomic(self):
 
         localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 14, self.RULE_atomic)
+        self.enterRule(localctx, 26, self.RULE_atomic)
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 63
+            self.state = 118
             self.match(TacticNotationsParser.ATOM)
-            self.state = 65
+            self.state = 120
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.SUB:
-                self.state = 64
+                self.state = 119
                 self.match(TacticNotationsParser.SUB)
 
 
@@ -572,17 +970,17 @@ class TacticNotationsParser ( Parser ):
     def hole(self):
 
         localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state)
-        self.enterRule(localctx, 16, self.RULE_hole)
+        self.enterRule(localctx, 28, self.RULE_hole)
         self._la = 0 # Token type
         try:
             self.enterOuterAlt(localctx, 1)
-            self.state = 67
+            self.state = 122
             self.match(TacticNotationsParser.ID)
-            self.state = 69
+            self.state = 124
             self._errHandler.sync(self)
             _la = self._input.LA(1)
             if _la==TacticNotationsParser.SUB:
-                self.state = 68
+                self.state = 123
                 self.match(TacticNotationsParser.SUB)
 
 
diff --git a/doc/tools/coqrst/notations/TacticNotationsVisitor.py b/doc/tools/coqrst/notations/TacticNotationsVisitor.py
index c0bcc4af37..aba696c89f 100644
--- a/doc/tools/coqrst/notations/TacticNotationsVisitor.py
+++ b/doc/tools/coqrst/notations/TacticNotationsVisitor.py
@@ -1,4 +1,4 @@
-# Generated from TacticNotations.g by ANTLR 4.7
+# Generated from TacticNotations.g by ANTLR 4.7.2
 from antlr4 import *
 if __name__ is not None and "." in __name__:
     from .TacticNotationsParser import TacticNotationsParser
@@ -24,6 +24,26 @@ class TacticNotationsVisitor(ParseTreeVisitor):
         return self.visitChildren(ctx)
 
 
+    # Visit a parse tree produced by TacticNotationsParser#nopipeblock.
+    def visitNopipeblock(self, ctx:TacticNotationsParser.NopipeblockContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#alternative.
+    def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#altblocks.
+    def visitAltblocks(self, ctx:TacticNotationsParser.AltblocksContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#altblock.
+    def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext):
+        return self.visitChildren(ctx)
+
+
     # Visit a parse tree produced by TacticNotationsParser#repeat.
     def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
         return self.visitChildren(ctx)
@@ -34,13 +54,23 @@ class TacticNotationsVisitor(ParseTreeVisitor):
         return self.visitChildren(ctx)
 
 
+    # Visit a parse tree produced by TacticNotationsParser#pipe.
+    def visitPipe(self, ctx:TacticNotationsParser.PipeContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#altsep.
+    def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext):
+        return self.visitChildren(ctx)
+
+
     # Visit a parse tree produced by TacticNotationsParser#whitespace.
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         return self.visitChildren(ctx)
 
 
-    # Visit a parse tree produced by TacticNotationsParser#meta.
-    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+    # Visit a parse tree produced by TacticNotationsParser#escaped.
+    def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
         return self.visitChildren(ctx)
 
 
diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py
index 87a41cf9f3..d2b5d86b37 100644
--- a/doc/tools/coqrst/notations/html.py
+++ b/doc/tools/coqrst/notations/html.py
@@ -13,12 +13,24 @@ Uses the dominate package.
 """
 
 from dominate import tags
+from dominate.utils import text
 
 from .parsing import parse
 from .TacticNotationsParser import TacticNotationsParser
 from .TacticNotationsVisitor import TacticNotationsVisitor
 
 class TacticNotationsToHTMLVisitor(TacticNotationsVisitor):
+    def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext):
+        with tags.span(_class='alternative'):
+            self.visitChildren(ctx)
+
+    def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext):
+        with tags.span(_class='alternative-block'):
+            self.visitChildren(ctx)
+
+    def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext):
+        tags.span('\u200b', _class="alternative-separator")
+
     def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
         with tags.span(_class="repeat-wrapper"):
             with tags.span(_class="repeat"):
@@ -39,21 +51,20 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor):
     def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
         tags.span(ctx.ATOM().getText())
 
+    def visitPipe(self, ctx:TacticNotationsParser.PipeContext):
+        text("|")
+
     def visitHole(self, ctx:TacticNotationsParser.HoleContext):
         tags.span(ctx.ID().getText()[1:], _class="hole")
         sub = ctx.SUB()
         if sub:
             tags.sub(sub.getText()[1:])
 
-    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
-        txt = ctx.METACHAR().getText()[1:]
-        if (txt == "{") or (txt == "}"):
-            tags.span(txt)
-        else:
-            tags.span(txt, _class="meta")
+    def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
+        tags.span(ctx.ESCAPED().getText()[1:])
 
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
-        tags.span(" ")          # TODO: no need for a <span> here
+        text(" ")
 
 def htmlize(notation):
     """Translate notation to a dominate HTML tree"""
diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py
index 506240d907..2312e09090 100644
--- a/doc/tools/coqrst/notations/parsing.py
+++ b/doc/tools/coqrst/notations/parsing.py
@@ -11,10 +11,22 @@ from .TacticNotationsLexer import TacticNotationsLexer
 from .TacticNotationsParser import TacticNotationsParser
 
 from antlr4 import CommonTokenStream, InputStream
+from antlr4.error.ErrorListener import ErrorListener
 
 SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"),
                  ("@qualid_or_string", "@id|@string")]
 
+class ParseError(Exception):
+    def __init__(self, msg):
+        super().__init__()
+        self.msg = msg
+
+class ExceptionRaisingErrorListener(ErrorListener):
+    def syntaxError(self, recognizer, offendingSymbol, line, column, msg, e):
+        raise ParseError("{}:{}: {}".format(line, column, msg))
+
+ERROR_LISTENER = ExceptionRaisingErrorListener()
+
 def substitute(notation):
     """Perform common substitutions in the notation string.
 
@@ -27,11 +39,13 @@ def substitute(notation):
     return notation
 
 def parse(notation):
-    """Parse a notation string.
+    """Parse a notation string, optionally reporting errors to `error_listener`.
 
     :return: An ANTLR AST. Use one of the supplied visitors (or write your own)
              to turn it into useful output.
     """
     substituted = substitute(notation)
     lexer = TacticNotationsLexer(InputStream(substituted))
-    return TacticNotationsParser(CommonTokenStream(lexer)).top()
+    parser = TacticNotationsParser(CommonTokenStream(lexer))
+    parser.addErrorListener(ERROR_LISTENER)
+    return parser.top()
diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py
index f6e82fc68e..2180c8e6a5 100644
--- a/doc/tools/coqrst/notations/plain.py
+++ b/doc/tools/coqrst/notations/plain.py
@@ -22,8 +22,16 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor):
     def __init__(self):
         self.buffer = StringIO()
 
+    def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext):
+        self.buffer.write("[")
+        self.visitChildren(ctx)
+        self.buffer.write("]")
+
+    def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext):
+        self.buffer.write("|")
+
     def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
-        separator = ctx.ATOM()
+        separator = ctx.ATOM() or ctx.PIPE()
         self.visitChildren(ctx)
         if ctx.LGROUP().getText()[1] == "+":
             spacer = (separator.getText() + " " if separator else "")
@@ -38,11 +46,14 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor):
     def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
         self.buffer.write(ctx.ATOM().getText())
 
+    def visitPipe(self, ctx:TacticNotationsParser.PipeContext):
+        self.buffer.write("|")
+
     def visitHole(self, ctx:TacticNotationsParser.HoleContext):
         self.buffer.write("‘{}’".format(ctx.ID().getText()[1:]))
 
-    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
-        self.buffer.write(ctx.METACHAR().getText()[1:])
+    def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
+        self.buffer.write(ctx.ESCAPED().getText()[1:])
 
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         self.buffer.write(" ")
diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py
index e05b834184..4ed09e04a9 100644
--- a/doc/tools/coqrst/notations/sphinx.py
+++ b/doc/tools/coqrst/notations/sphinx.py
@@ -20,8 +20,6 @@ from .TacticNotationsVisitor import TacticNotationsVisitor
 from docutils import nodes
 from sphinx import addnodes
 
-import sys
-
 class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
     def defaultResult(self):
         return []
@@ -31,16 +29,36 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
             aggregate.extend(nextResult)
         return aggregate
 
+    def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext):
+        return [nodes.inline('', '', *self.visitChildren(ctx), classes=['alternative'])]
+
+    def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext):
+        return [nodes.inline('', '', *self.visitChildren(ctx), classes=['alternative-block'])]
+
+    def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext):
+        return [nodes.inline('|', '\u200b', classes=['alternative-separator'])]
+
+    @staticmethod
+    def is_alternative(node):
+        return isinstance(node, nodes.inline) and node['classes'] == ['alternative']
+
     def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
         # Uses inline nodes instead of subscript and superscript to ensure that
         # we get the right customization hooks at the LaTeX level
         wrapper = nodes.inline('', '', classes=['repeat-wrapper'])
-        wrapper += nodes.inline('', '', *self.visitChildren(ctx), classes=["repeat"])
+
+        children = self.visitChildren(ctx)
+        if len(children) == 1 and self.is_alternative(children[0]):
+            # Use a custom style if an alternative is nested in a repeat.
+            # (We could detect this in CSS, but it's much harder in LaTeX.)
+
+            children[0]['classes'] = ['repeated-alternative']
+        wrapper += nodes.inline('', '', *children, classes=["repeat"])
 
         repeat_marker = ctx.LGROUP().getText()[1]
         wrapper += nodes.inline(repeat_marker, repeat_marker, classes=['notation-sup'])
 
-        separator = ctx.ATOM()
+        separator = ctx.ATOM() or ctx.PIPE()
         if separator:
             sep = separator.getText()
             wrapper += nodes.inline(sep, sep, classes=['notation-sub'])
@@ -65,6 +83,9 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
 
         return [node]
 
+    def visitPipe(self, ctx:TacticNotationsParser.PipeContext):
+        return [nodes.Text("|")]
+
     def visitHole(self, ctx:TacticNotationsParser.HoleContext):
         hole = ctx.ID().getText()
         token_name = hole[1:]
@@ -75,23 +96,18 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
             sub_index = sub.getText()[2:]
             node += nodes.subscript(sub_index, sub_index)
 
-        return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)]
+        return [addnodes.pending_xref(token_name, node, reftype='token',
+                                 refdomain='std', reftarget=token_name)]
 
-    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
-        meta = ctx.METACHAR().getText()
-        metachar = meta[1:] # remove escape char
-        token_name = metachar
-        if (metachar == "{") or (metachar == "}"):
-            classes=[]
-        else:
-            classes=["meta"]
-        return [nodes.inline(metachar, token_name, classes=classes)]
+    def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext):
+        escaped = ctx.ESCAPED().getText()
+        return [nodes.inline(escaped, escaped[1:])]
 
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         return [nodes.Text(" ")]
 
 def sphinxify(notation):
-    """Translate notation into a Sphinx document tree"""
+    """Translate a notation into a Sphinx document tree."""
     vs = TacticNotationsToSphinxVisitor()
     return vs.visit(parse(notation))