Various fixes.

4 files changed, 10 insertions, 21 deletions

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 301559d69d..dd0b12f8ec 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -990,11 +990,6 @@ described first.
    has to check the conversion (see Section :ref:`conversion-rules`) of two distinct
    applied constants.
 
-   .. seealso::
-
-      Sections :ref:`performingcomputations`, :ref:`tactics-automating`,
-      :ref:`proof-editing-mode`
-
 .. cmd:: Transparent {+ @reference }
 
    This command accepts the :attr:`global` attribute.  By default, the scope
@@ -1015,10 +1010,7 @@ described first.
 
       There is no constant named :n:`@qualid` in the environment.
 
-      .. seealso::
-
-         Sections :ref:`performingcomputations`,
-         :ref:`tactics-automating`, :ref:`proof-editing-mode`
+.. seealso:: :ref:`performingcomputations` and :ref:`proof-editing-mode`
 
 .. _vernac-strategy:
 
diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst
index ebd75ef300..f46d8f8b72 100644
--- a/doc/sphinx/proofs/writing-proofs/index.rst
+++ b/doc/sphinx/proofs/writing-proofs/index.rst
@@ -27,9 +27,9 @@ flavors of tactics, including the SSReflect proof language.
 .. toctree::
    :maxdepth: 1
 
-   ../../proof-engine/proof-handling
+   proof-mode
    ../../proof-engine/tactics
-    rewriting
+   rewriting
    ../../proof-engine/ssreflect-proof-language
    ../../proof-engine/detailed-tactic-examples
    ../../user-extensions/proof-schemes
diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
index 51aebd5661..b74c9d3a23 100644
--- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst
+++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
@@ -824,24 +824,24 @@ new, no line of old text is shown for them.
 
 ..
 
-  .. image:: ../_static/diffs-coqide-on.png
+  .. image:: ../../_static/diffs-coqide-on.png
      :alt: |CoqIDE| with Set Diffs on
 
 ..
 
-  .. image:: ../_static/diffs-coqide-removed.png
+  .. image:: ../../_static/diffs-coqide-removed.png
      :alt: |CoqIDE| with Set Diffs removed
 
 ..
 
-  .. image:: ../_static/diffs-coqtop-on3.png
+  .. image:: ../../_static/diffs-coqtop-on3.png
      :alt: coqtop with Set Diffs on
 
 This image shows an error message with diff highlighting in |CoqIDE|:
 
 ..
 
-  .. image:: ../_static/diffs-error-message.png
+  .. image:: ../../_static/diffs-error-message.png
      :alt: |CoqIDE| error message with diffs
 
 How to enable diffs
@@ -943,7 +943,7 @@ the split because it has not changed.
 
 ..
 
-  .. image:: ../_static/diffs-coqide-multigoal.png
+  .. image:: ../../_static/diffs-coqide-multigoal.png
      :alt: coqide with Set Diffs on with multiple goals
 
 Diffs may appear like this after applying a :tacn:`intro` tactic that results
@@ -951,7 +951,7 @@ in a compacted hypotheses:
 
 ..
 
-  .. image:: ../_static/diffs-coqide-compacted.png
+  .. image:: ../../_static/diffs-coqide-compacted.png
      :alt: coqide with Set Diffs on with compacted hypotheses
 
 .. _showing_proof_diffs:
@@ -974,7 +974,7 @@ To show differences in the proof term:
 
   ..
 
-    .. image:: ../_static/diffs-show-proof.png
+    .. image:: ../../_static/diffs-show-proof.png
        :alt: coqide with Set Diffs on with compacted hypotheses
 
 Controlling the effect of proof editing commands
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 040849a9ef..1358aad432 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -855,6 +855,3 @@ Conversion tactics applied to hypotheses
    definition.
 
    Example: :n:`unfold not in (type of H1) (type of H3)`.
-
-.. exn:: No such hypothesis: @ident.
-   :undocumented: