diff --git a/BUILDING.md b/BUILDING.md
index c83bf962..32fa391f 100644
--- a/BUILDING.md
+++ b/BUILDING.md
@@ -145,11 +145,11 @@ If you are using WSL on Windows, you need to install the VS Code [WSL extension]
 
 We recommend also installing the [Fast Unicode Math Characters extension](https://marketplace.visualstudio.com/items?itemName=GuidoTapia2.unicode-math-vscode), to enable easier input of mathematical symbols.
 
-To enable Coq support in VS Code, there are two options: the VsCoq extension and the Coq LSP extension. Note that these extensions are restricted to Coq 8.18.0 and later. For earlier versions, you can use the [VsCoq Legacy extension](https://github.com/coq-community/vscoq/tree/vscoq1).
+To enable Coq support in VS Code, there are two main options: the VsCoq extension and the Coq LSP extension. Note that these extensions are restricted to Coq 8.18.0 and later. For earlier versions, you can use the [VsCoq Legacy extension](https://github.com/coq-community/vscoq/tree/vscoq1).
 
 ### VsCoq extension
 
-To install the [VsCoq extension](https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp) from the command line, make sure that [switch creation](#install-a-switch-for-opam) and [dependency installation](#install-the-project-dependencies-via-opam) are done and then run:
+To install the [VsCoq extension](https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq) from the command line, make sure that [switch creation](#install-a-switch-for-opam) and [dependency installation](#install-the-project-dependencies-via-opam) are done and then run:
 
 ```shell
 opam install vscoq-language-server && code --install-extension maximedenes.vscoq
diff --git a/README.md b/README.md
index e4c1b12b..64ba0b9b 100644
--- a/README.md
+++ b/README.md
@@ -65,7 +65,7 @@ make   # or make -j <number-of-cores-on-your-machine>
 ### Source documentation
 
 - [latest coqdoc presentation of the Coq files](https://runtimeverification.github.io/vlsm-docs/latest/coqdoc/toc.html)
-- [latest Alectryon presentation the Coq files](https://runtimeverification.github.io/vlsm-docs/latest/alectryon/toc.html)
+- [latest Alectryon presentation of the Coq files](https://runtimeverification.github.io/vlsm-docs/latest/alectryon/toc.html)
 
 ### VLSM tutorials
 
diff --git a/meta.yml b/meta.yml
index e3b6c1db..b85aa2d9 100644
--- a/meta.yml
+++ b/meta.yml
@@ -120,7 +120,7 @@ documentation: |-
   ### Source documentation
 
   - [latest coqdoc presentation of the Coq files](https://runtimeverification.github.io/vlsm-docs/latest/coqdoc/toc.html)
-  - [latest Alectryon presentation the Coq files](https://runtimeverification.github.io/vlsm-docs/latest/alectryon/toc.html)
+  - [latest Alectryon presentation of the Coq files](https://runtimeverification.github.io/vlsm-docs/latest/alectryon/toc.html)
 
   ### VLSM tutorials