1 files changed, 14 insertions, 7 deletions
diff --git a/README.md b/README.md
index 882b092..1b5da91 100644
--- a/README.md
+++ b/README.md
@@ -12,9 +12,9 @@ the [thesis archive](https://www.cs.ru.nl/bachelors-theses/) page of
 ## Development
-During my thesis, I used Nix to manage the Coq installation for this thesis.
+During my thesis, I used Nix to manage my Coq installation. If you use Nix, it
-If you use Nix, it should be easy to build/check the codebase. If not, this
+should be easy to build/check the codebase. If not, this might be a bit more
-might be a bit more tricky.
+tricky.
 There are two things that you need to have installed. The current `flake.lock`
 ensures that we have the following software:
@@ -26,10 +26,12 @@ ensures that we have the following software:
 I have attached a `flake.nix` and `flake.lock` file, which should make my setup
 reproducible. Assuming a working Nix installation with flake support and the
-Nix command enabled, simply running `nix develop` followed by `make` should run
+Nix command enabled, simply running `nix develop` should give you a shell where
-`coqc` on all files. If you have a working [direnv](https://direnv.net/)
+the right Coq and Coq-std++ versions available.
-installation, simply running `direnv allow` (after inspecting the `.envrc`
-file) should make the right version of Coq and Coq-std++ available.
+If you have a working [direnv](https://direnv.net/) installation, simply
+running `direnv allow` (after inspecting the `.envrc` file) should make the
+right version of Coq and Coq-std++ available.
 ### Without Nix
@@ -43,3 +45,8 @@ Coq-std++. However, your operating system's package repositories may also
 provide a package. Consider taking a look at the Repology pages:
 [coq-stdpp](https://repology.org/project/coq-stdpp/versions),
 [coq:stdpp](https://repology.org/project/coq:stdpp/versions).
+## Building/checking
+Running `make` should run `coqc` on all files; assuming that you are using a
+compatible Coq version, this should successfully check all proofs.

diff --git a/README.md b/README.md index 882b092..1b5da91 100644 --- a/README.md +++ b/README.md
@@ -12,9 +12,9 @@ the [thesis archive](https://www.cs.ru.nl/bachelors-theses/) page of
12		12
13	## Development	13	## Development
14		14
15	During my thesis, I used Nix to manage the Coq installation for this thesis.	15	During my thesis, I used Nix to manage my Coq installation. If you use Nix, it
16	If you use Nix, it should be easy to build/check the codebase. If not, this	16	should be easy to build/check the codebase. If not, this might be a bit more
17	might be a bit more tricky.	17	tricky.
18		18
19	There are two things that you need to have installed. The current `flake.lock`	19	There are two things that you need to have installed. The current `flake.lock`
20	ensures that we have the following software:	20	ensures that we have the following software:
@@ -26,10 +26,12 @@ ensures that we have the following software:
26		26
27	I have attached a `flake.nix` and `flake.lock` file, which should make my setup	27	I have attached a `flake.nix` and `flake.lock` file, which should make my setup
28	reproducible. Assuming a working Nix installation with flake support and the	28	reproducible. Assuming a working Nix installation with flake support and the
29	Nix command enabled, simply running `nix develop` followed by `make` should run	29	Nix command enabled, simply running `nix develop` should give you a shell where
30	`coqc` on all files. If you have a working [direnv](https://direnv.net/)	30	the right Coq and Coq-std++ versions available.
31	installation, simply running `direnv allow` (after inspecting the `.envrc`	31
32	file) should make the right version of Coq and Coq-std++ available.	32	If you have a working [direnv](https://direnv.net/) installation, simply
		33	running `direnv allow` (after inspecting the `.envrc` file) should make the
		34	right version of Coq and Coq-std++ available.
33		35
34	### Without Nix	36	### Without Nix
35		37
@@ -43,3 +45,8 @@ Coq-std++. However, your operating system's package repositories may also
43	provide a package. Consider taking a look at the Repology pages:	45	provide a package. Consider taking a look at the Repology pages:
44	[coq-stdpp](https://repology.org/project/coq-stdpp/versions),	46	[coq-stdpp](https://repology.org/project/coq-stdpp/versions),
45	[coq:stdpp](https://repology.org/project/coq:stdpp/versions).	47	[coq:stdpp](https://repology.org/project/coq:stdpp/versions).
		48
		49	## Building/checking
		50
		51	Running `make` should run `coqc` on all files; assuming that you are using a
		52	compatible Coq version, this should successfully check all proofs.