From c654804ba038598602c1e8bdf41bf213e2c036f1 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Wed, 20 May 2020 22:13:30 -0400
Subject: [sphinx] Get rid of anonymous targets (Sphinx 2.3.1 doesn't like
 them)

https://github.com/sphinx-doc/sphinx/issues/7701
---
 doc/sphinx/changes.rst | 31 ++++++++++---------------------
 1 file changed, 10 insertions(+), 21 deletions(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 72f0fdf4c5..d6163f7d5f 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -987,42 +987,31 @@ Summary of changes
 
 The main changes brought by |Coq| version 8.11 are:
 
-- `Ltac2`__, a new tactic language for writing more robust larger scale
+- `Ltac2 <811Ltac2>`_, a new tactic language for writing more robust larger scale
   tactics, with built-in support for datatypes and the multi-goal tactic monad.
-- `Primitive floats`__ are integrated in terms and follow the binary64 format
+- `Primitive floats <811PrimitiveFloats>`_ are integrated in terms and follow the binary64 format
   of the IEEE 754 standard, as specified in the `Coq.Float.Floats` library.
-- `Cleanups`__ of the section mechanism, delayed proofs and further
+- `Cleanups <811Sections>`_ of the section mechanism, delayed proofs and further
   restrictions of template polymorphism to fix soundness issues related to
   universes.
-- New `unsafe flags`__ to disable locally guard, positivity and universe
+- New `unsafe flags <811UnsafeFlags>`_ to disable locally guard, positivity and universe
   checking. Reliance on these flags is always printed by
   :g:`Print Assumptions`.
-- `Fixed bugs`__ of :g:`Export` and :g:`Import` that can have a
+- `Fixed bugs <811ExportBug>`_ of :g:`Export` and :g:`Import` that can have a
   significant impact on user developments (**common source of
   incompatibility!**).
-- New interactive development method based on `vos` `interface files`__,
+- New interactive development method based on `vos` `interface files <811vos>`_,
   allowing to work on a file without recompiling the proof parts of their
   dependencies.
-- New :g:`Arguments` annotation for `bidirectional type inference`__
+- New :g:`Arguments` annotation for `bidirectional type inference <811BidirArguments>`_
   configuration for reference (e.g. constants, inductive) applications.
-- New `refine attribute`__ for :cmd:`Instance` can be used instead of
+- New `refine attribute <811RefineInstance>`_ for :cmd:`Instance` can be used instead of
   the removed ``Refine Instance Mode``.
-- Generalization of the :g:`under` and :g:`over` tactics__ of SSReflect to
+- Generalization of the :g:`under` and :g:`over` `tactics <811SSRUnderOver>`_ of SSReflect to
   arbitrary relations.
-- `Revision`__ of the :g:`Coq.Reals` library, its axiomatisation and
+- `Revision <811Reals>`_ of the :g:`Coq.Reals` library, its axiomatisation and
   instances of the constructive and classical real numbers.
 
-__ 811Ltac2_
-__ 811PrimitiveFloats_
-__ 811Sections_
-__ 811UnsafeFlags_
-__ 811ExportBug_
-__ 811vos_
-__ 811BidirArguments_
-__ 811RefineInstance_
-__ 811SSRUnderOver_
-__ 811Reals_
-
 Additionally, while the :tacn:`omega` tactic is not yet deprecated in
 this version of Coq, it should soon be the case and we already
 recommend users to switch to :tacn:`lia` in new proof scripts (see
-- 
cgit v1.2.3