diff --git a/INSTALL.md b/INSTALL.md
index 1070c62e8..6225eb095 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -36,10 +36,10 @@ MetaCoq is split into multiple packages that get all installed using the
  - `coq-metacoq-erasure-plugin` for the extracted verifed erasure plugin
  - `coq-metacoq-translations` for example translations from type theory
    to type theory: e.g. variants of parametricity.
- - `coq-metacoq-quotation` for a quotation library, allowing to 
+ - `coq-metacoq-quotation` for a quotation library, allowing to
    quote MetaCoq terms and typing derivations as MetaCoq terms,
    with a work-in-progress proof of Löb's theorem.
-   
+
 There are also `.dev` packages available in the `extra-dev` repository
 of Coq, to get those you will need to activate the following repositories:
 
@@ -67,10 +67,10 @@ to have a dedicated `opam` switch (see below).
 To get the source code:
 
     # git clone https://github.com/MetaCoq/metacoq.git
-    # git checkout -b coq-8.16 origin/coq-8.16
+    # git checkout -b coq-8.17 origin/coq-8.17
     # git status
 
-This checks that you are indeed on the `coq-8.16` branch.
+This checks that you are indeed on the `coq-8.17` branch.
 
 ### Setting up an `opam` switch
 
@@ -79,10 +79,10 @@ To setup a fresh `opam` installation, you might want to create a
 one yet. You need to use **opam 2** to obtain the right version of
 `Equations`.
 
-    # opam switch create coq.8.16 --packages=ocaml-variants.4.13.1+options,ocaml-option-flambda
+    # opam switch create coq.8.17 --packages=ocaml-variants.4.13.1+options,ocaml-option-flambda
     # eval $(opam env)
 
-This creates the `coq.8.16` switch which initially contains only the
+This creates the `coq.8.17` switch which initially contains only the
 basic `OCaml` `4.13.1` compiler with the `flambda` option enabled,
 and puts you in the right environment (check with `ocamlc -v`).
 
@@ -109,8 +109,8 @@ the sources directory.
 Then use:
 
 - `make` to compile the `template-coq` plugin, the `pcuic`
-  development and the `safechecker` and `erasure` plugins, 
-  along with the `test-suite`, `translations`, `examples` 
+  development and the `safechecker` and `erasure` plugins,
+  along with the `test-suite`, `translations`, `examples`
   and `quotation` libraries.
   You can also selectively build each target.
 
@@ -127,5 +127,5 @@ For faster development one can use:
   to construct the template-coq plugin. The `safechecker` and
   `erasure` ML plugins *cannot* be built using this mode.
 
-- `make quick` is a synonymous for `make vos` with the addition of a global `Unset Universe Checking` option, i.e. 
+- `make quick` is a synonymous for `make vos` with the addition of a global `Unset Universe Checking` option, i.e.
 universes are not checked anywhere.