Various fixes.

3 files changed, 9 insertions, 12 deletions

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: