diff --git a/docs/Readme.html b/docs/Readme.html
index e50f1ea..027020c 100644
--- a/docs/Readme.html
+++ b/docs/Readme.html
@@ -67,9 +67,9 @@ <h2>Installing dependencies</h2>
 </div>
 <div class="section" id="building-the-project">
 <h2>Building the project</h2>
-<p>... code:: shell</p>
-<blockquote>
-dune build</blockquote>
+<pre class="code shell literal-block">
+dune<span class="w"> </span>build
+</pre>
 </div>
 <div class="section" id="alectryon-documentation">
 <h2>Alectryon documentation</h2>
@@ -78,7 +78,7 @@ <h2>Alectryon documentation</h2>
 opam<span class="w"> </span>install<span class="w"> </span><span class="s2">&quot;coq-serapi==8.17.0+0.17.1&quot;</span><span class="w">
 </span>python3<span class="w"> </span>-m<span class="w"> </span>pip<span class="w"> </span>install<span class="w"> </span>--user<span class="w"> </span>alectryon
 </pre>
-<p>The build with:</p>
+<p>Then build with:</p>
 <pre class="code shell literal-block">
 make<span class="w"> </span>doc
 </pre>
@@ -150,7 +150,7 @@ <h2>Structure of the repository</h2>
 <div class="section" id="axioms">
 <h2>Axioms</h2>
 <p>The whole development relies only on axiom K, a conventional and sound axiom
-from Coq's standard library (more precisely, <a class="reference external" href="https://coq.inria.fr/library/Coq.Eqdep.Eq_rect_eq.html#eq_rect_eq">Coq.Eqdep.Eq_rect_eq.eq_rect_eq</a>).</p>
+from Coq's standard library (more precisely, <a class="reference external" href="https://coq.inria.fr/library/Coq.Logic.Eqdep.Eq_rect_eq.html#eq_rect_eq">Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq</a>).</p>
 <p>This can be double checked as follows:</p>
 <ul class="simple">
 <li>for the abstract result of soundness of the OGS by running <tt class="docutils literal">Print
diff --git a/docs/Soundness.html b/docs/Soundness.html
index 4bb0563..c2dc6a8 100644
--- a/docs/Soundness.html
+++ b/docs/Soundness.html
@@ -113,7 +113,7 @@ <h1 class="title">Soundness (Theorem 6.12)</h1>
 </ul>
 <p>The second command will explicit if any axiom has been used to establish the
 result. As stated in the <a class="reference external" href="Prelude.html">prelude</a>, we exclusively use
-<a class="reference external" href="https://coq.inria.fr/library/Coq.Eqdep.Eq_rect_eq.html#eq_rect_eq">Coq.Eqdep.Eq_rect_eq.eq_rect_eq</a>, ie Streicher's axiom K.</p>
+<a class="reference external" href="https://coq.inria.fr/library/Coq.Logic.Eqdep.Eq_rect_eq.html#eq_rect_eq">Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq</a>, ie Streicher's axiom K.</p>
 </div>
 </div></body>
 </html>
diff --git a/theories/OGS/Soundness.v b/theories/OGS/Soundness.v
index a0c9ee7..b3b5d89 100644
--- a/theories/OGS/Soundness.v
+++ b/theories/OGS/Soundness.v
@@ -89,5 +89,5 @@ to provide with several examples:
 
 The second command will explicit if any axiom has been used to establish the
 result. As stated in the `prelude <Prelude.html>`_, we exclusively use
-:coqid:`Coq.Eqdep.Eq_rect_eq.eq_rect_eq`, ie Streicher's axiom K.
+:coqid:`Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq`, ie Streicher's axiom K.
 |*)
diff --git a/theories/Readme.v b/theories/Readme.v
index 7cdda8e..418ff50 100644
--- a/theories/Readme.v
+++ b/theories/Readme.v
@@ -61,7 +61,7 @@ or manually:
 Building the project
 ^^^^^^^^^^^^^^^^^^^^
 
-... code:: shell
+.. code:: shell
 
     dune build
 
@@ -75,7 +75,7 @@ To build the html documentation, first install Alectryon:
    opam install "coq-serapi==8.17.0+0.17.1"
    python3 -m pip install --user alectryon
 
-The build with:
+Then build with:
 
 .. code:: shell
 
@@ -150,7 +150,7 @@ Axioms
 ^^^^^^
 
 The whole development relies only on axiom K, a conventional and sound axiom
-from Coq's standard library (more precisely, :coqid:`Coq.Eqdep.Eq_rect_eq.eq_rect_eq`).
+from Coq's standard library (more precisely, :coqid:`Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq`).
 
 This can be double checked as follows: