Minimal changes to make the refman compatible with Sphinx 3.

Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>

5 files changed, 83 insertions, 79 deletions

diff --git a/doc/README.md b/doc/README.md
index 99d285320d..79d1e1b756 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -28,10 +28,9 @@ Dependencies
 
 To produce the complete documentation in HTML, you will need Coq dependencies
 listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based
-reference manual requires Python 3, and the following Python packages
-(note the version constraints on Sphinx):
+reference manual requires Python 3, and the following Python packages:
 
-  - sphinx >= 2.3.1 & < 3.0.0
+  - sphinx >= 2.3.1
   - sphinx_rtd_theme >= 0.4.3
   - beautifulsoup4 >= 4.0.6
   - antlr4-python3-runtime >= 4.7.1
@@ -41,7 +40,7 @@ reference manual requires Python 3, and the following Python packages
 To install them, you should first install pip and setuptools (for instance,
 with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run:
 
-    pip3 install sphinx==2.3.1 sphinx_rtd_theme beautifulsoup4 \
+    pip3 install sphinx sphinx_rtd_theme beautifulsoup4 \
                  antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex
 
 Nix users should get the correct development environment to build the
diff --git a/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst b/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst
new file mode 100644
index 0000000000..d17a2dff6b
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  The reference manual can now build with Sphinx 3
+  (`#13011 <https://github.com/coq/coq/pull/13011>`_,
+  fixes `#12332 <https://github.com/coq/coq/issues/12332>`_,
+  by Théo Zimmermann and Jim Fehrle).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 070e899c9d..ba5bac6489 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -61,19 +61,23 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
 
 The tactics solve propositional formulas parameterized by atomic
 arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`.
-The syntax of the formulas is the following:
+The syntax for formulas over :math:`\mathbb{Z}` is:
 
- .. productionlist:: F
-   F : A ∣ P | True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F | F = F
-   A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p
-   p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n
+   .. note the following is not an insertprodn
 
-where :math:`F` is interpreted over either `Prop` or `bool`,
-:math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the
-operators :math:`−, +, ×` are respectively subtraction, addition, and product;
-:math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition.
-For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of
-rationals ``==``.
+   .. prodn::
+      F ::= {| @A | P | True | False | @F /\\ @F | @F \\/ @F | @F <-> @F | @F -> @F | ~ @F | @F = @F }
+      A ::= {| @p = @p | @p > @p | @p < @p | @p >= @p | @p <= @p }
+      p ::= {| c | x | −@p | @p − @p | @p + @p | @p * @p | @p ^ n }
+
+where
+
+  - :token:`F` is interpreted over either `Prop` or `bool`
+  - :n:`P` is an arbitrary proposition
+  - :n:`c` is a numeric constant of :math:`D`
+  - :n:`x` :math:`\in D` is a numeric variable
+  - :n:`−`, :n:`+` and :n:`*` are respectively subtraction, addition and product
+  - :n:`p ^ n` is exponentiation by a constant :math:`n`
 
 When :math:`F` is interpreted over `bool`, the boolean operators are
 `&&`, `||`, `Bool.eqb`, `Bool.implb`, `Bool.negb` and the comparisons
@@ -81,6 +85,9 @@ in :math:`A` are also interpreted over the booleans (e.g., for
 :math:`\mathbb{Z}`, we have `Z.eqb`, `Z.gtb`, `Z.ltb`, `Z.geb`,
 `Z.leb`).
 
+For :math:`\mathbb{Q}`, use the equality of rationals ``==`` rather than
+Leibniz equality ``=``.
+
 For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational
 constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the
 following expressions:
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index b5618c5721..3d36c5c50f 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -196,12 +196,9 @@ Program Definition
 Program Fixpoint
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Fixpoint @ident {* @binder } {? {@order}} : @type := @term
+.. cmd:: Program Fixpoint @fix_definition {* with @fix_definition }
 
-   The optional order annotation follows the grammar:
-
-   .. productionlist:: orderannot
-      order      : measure `term` [ `term` ] | wf `term` `ident`
+   The optional :n:`@fixannot` annotation can be one of:
 
    + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on
      any subset of the arguments and the optional term
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2211a58e6e..99888cbe1d 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -59,9 +59,9 @@ specified, the default selector is used.
 
 .. _tactic_invocation_grammar:
 
-  .. productionlist:: sentence
-     tactic_invocation : `toplevel_selector` : `tactic`.
-                       : `tactic`.
+  .. prodn::
+     tactic_invocation ::= @toplevel_selector : @tactic.
+     | @tactic.
 
 .. todo: fully describe selectors.  At the moment, ltac has a fairly complete description
 
@@ -98,11 +98,11 @@ The general form of a term with a bindings list is
 
 .. _bindings_list_grammar:
 
-  .. productionlist:: bindings_list
-     ref           : `ident`
-                   : `num`
-     bindings_list : (`ref` := `term`) ... (`ref` := `term`)
-                   : `term` ... `term`
+  .. prodn::
+     ref ::= @ident
+     | @num
+     bindings_list ::= {+ (@ref := @term) }
+     | {+ @term }
 
 + In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an
   :n:`@ident` or a :n:`@num`. The references are determined according to the type of
@@ -137,30 +137,28 @@ introduced by tactics.  They also let you split an introduced hypothesis into
 multiple hypotheses or subgoals.  Common tactics that accept intro patterns
 include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`.
 
-.. productionlist::        coq
-   intropattern_list       : `intropattern` ... `intropattern`
-                           : `empty`
-   empty                   :
-   intropattern            : *
-                           : **
-                           : `simple_intropattern`
-   simple_intropattern     : `simple_intropattern_closed` [ % `term` ... % `term` ]
-   simple_intropattern_closed : `naming_intropattern`
-                              : _
-                              : `or_and_intropattern`
-                              : `rewriting_intropattern`
-                              : `injection_intropattern`
-   naming_intropattern     : `ident`
-                           : ?
-                           : ?`ident`
-   or_and_intropattern     : [ `intropattern_list` | ... | `intropattern_list` ]
-                           : ( `simple_intropattern` , ... , `simple_intropattern` )
-                           : ( `simple_intropattern` & ... & `simple_intropattern` )
-   rewriting_intropattern  : ->
-                           : <-
-   injection_intropattern  : [= `intropattern_list` ]
-   or_and_intropattern_loc : `or_and_intropattern`
-                           : `ident`
+.. prodn::
+   intropattern_list ::= {* @intropattern }
+   intropattern ::= *
+   | **
+   | @simple_intropattern
+   simple_intropattern ::= @simple_intropattern_closed {* % @term0 }
+   simple_intropattern_closed ::= @naming_intropattern
+   | _
+   | @or_and_intropattern
+   | @rewriting_intropattern
+   | @injection_intropattern
+   naming_intropattern ::= @ident
+   | ?
+   | ?@ident
+   or_and_intropattern ::= [ {*| @intropattern_list } ]
+   | ( {*, @simple_intropattern } )
+   | ( {*& @simple_intropattern } )
+   rewriting_intropattern ::= ->
+   | <-
+   injection_intropattern ::= [= @intropattern_list ]
+   or_and_intropattern_loc ::= @or_and_intropattern
+   | ident
 
 Note that the intro pattern syntax varies between tactics.
 Most tactics use :n:`@simple_intropattern` in the grammar.
@@ -480,13 +478,13 @@ Occurrence sets and occurrence clauses
 An occurrence clause is a modifier to some tactics that obeys the
 following syntax:
 
-  .. productionlist:: coq
-     occurrence_clause : in `goal_occurrences`
-     goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]]
-                      : * |- [* [`at_occurrences`]]
-                      : *
-     at_occurrences : at `occurrences`
-     occurrences     : [-] `num` ... `num`
+  .. prodn::
+     occurrence_clause ::= in @goal_occurrences
+     goal_occurrences ::= {*, @ident {? @at_occurrences } } {? |- {? * {? @at_occurrences } } }
+     | * |- {? * {? @at_occurrences } }
+     | *
+     at_occurrences ::= at @occurrences
+     occurrences ::= {? - } {* @num }
 
 The role of an occurrence clause is to select a set of occurrences of a term
 in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate
@@ -3975,15 +3973,15 @@ automatically created.
       the following. Beware, there is no operator precedence during parsing, one can
       check with :cmd:`Print HintDb` to verify the current cut expression:
 
-      .. productionlist:: regexp
-          regexp : `ident`          (hint or instance identifier)
-                 : _             (any hint)
-                 : `regexp` | `regexp` (disjunction)
-                 : `regexp` `regexp`   (sequence)
-                 : `regexp` *       (Kleene star)
-                 : emp           (empty)
-                 : eps           (epsilon)
-                 : ( `regexp` )
+      .. prodn::
+         regexp ::= @ident   (hint or instance identifier)
+         | _   (any hint)
+         | @regexp | @regexp   (disjunction)
+         | @regexp @regexp   (sequence)
+         | @regexp *   (Kleene star)
+         | emp   (empty)
+         | eps   (epsilon)
+         | ( @regexp )
 
       The `emp` regexp does not match any search path while `eps`
       matches the empty path. During proof search, the path of
@@ -4672,17 +4670,15 @@ Automating
    tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are
    constructed over the following grammar:
 
-   .. _btauto_grammar:
-
-   .. productionlist:: sentence
-      btauto_term : `ident`
-                  : true
-                  : false
-                  : orb `btauto_term` `btauto_term`
-                  : andb `btauto_term` `btauto_term`
-                  : xorb `btauto_term` `btauto_term`
-                  : negb `btauto_term`
-                  : if `btauto_term` then `btauto_term` else `btauto_term`
+   .. prodn::
+      btauto_term ::= @ident
+      | true
+      | false
+      | orb @btauto_term @btauto_term
+      | andb @btauto_term @btauto_term
+      | xorb @btauto_term @btauto_term
+      | negb @btauto_term
+      | if @btauto_term then @btauto_term else @btauto_term
 
    Whenever the formula supplied is not a tautology, it also provides a
    counter-example.