From 906c61c5c069e69eae3981f7722f6d69134ff7ef Mon Sep 17 00:00:00 2001
From: Simon Gregersen <gregersen@cs.au.dk>
Date: Tue, 10 Oct 2023 09:17:54 +0200
Subject: [PATCH] README

---
 README.html | 4 ++--
 README.md   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/README.html b/README.html
index fefd25cf..82ff427c 100644
--- a/README.html
+++ b/README.html
@@ -226,10 +226,10 @@ <h2 id="building-the-development">Building the development</h2>
 <code>make -j N</code> where <code>N</code> is the number of cores
 available on your machine.</p>
 <h2 id="axioms">Axioms</h2>
-<p>The development relies on axioms for classical reasoning and the
+<p>The development relies on axioms for classical reasoning and an
 axiomatization of the reals numbers, both found in Coq’s standard
 library. The following list is produced when executing the command
-“Print Assumptions eager_lazy_equiv.” in <a
+<code>Print Assumptions eager_lazy_equiv.</code> in <a
 href="theories/examples/lazy_eager_coin.v"><code>theories/examples/lazy_eager_coin.v</code></a>:</p>
 <pre><code>ClassicalDedekindReals.sig_not_dec : ∀ P : Prop, {¬ ¬ P} + {¬ P}
 ClassicalDedekindReals.sig_forall_dec : ∀ P : nat → Prop, (∀ n : nat, {P n} + {¬ P n}) → {n : nat | ¬ P n} + {∀ n : nat, P n}
diff --git a/README.md b/README.md
index ee9600bf..cc02822a 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,7 @@ You should now be able to build the development by using `make -j N` where `N` i
 
 ## Axioms
 
-The development relies on axioms for classical reasoning and the axiomatization of the reals numbers, both found in Coq's standard library. The following list is produced when executing the command "Print Assumptions eager_lazy_equiv." in [`theories/examples/lazy_eager_coin.v`](theories/examples/lazy_eager_coin.v):
+The development relies on axioms for classical reasoning and an axiomatization of the reals numbers, both found in Coq's standard library. The following list is produced when executing the command `Print Assumptions eager_lazy_equiv.` in [`theories/examples/lazy_eager_coin.v`](theories/examples/lazy_eager_coin.v):
 
 ```
 ClassicalDedekindReals.sig_not_dec : ∀ P : Prop, {¬ ¬ P} + {¬ P}