diff --git a/opam/opam-coq-archive/released/packages/coq-hott/coq-hott.9.1/opam b/opam/opam-coq-archive/released/packages/coq-hott/coq-hott.9.1/opam
new file mode 100644
index 0000000000..e9b1849b89
--- /dev/null
+++ b/opam/opam-coq-archive/released/packages/coq-hott/coq-hott.9.1/opam
@@ -0,0 +1,28 @@
+opam-version: "2.0"
+maintainer: [ "Jason Gross <jgross@mit.edu>" "Ali Caglayan <alizter@gmail.com>" ]
+homepage: "http://homotopytypetheory.org/"
+bug-reports: "https://github.com/HoTT/HoTT/issues"
+license: "BSD-2-Clause"
+build: [ "dune" "build" "-p" name "-j" jobs "@install" ]
+install: [ "dune" "install" "-p" name ]
+depends: [
+  "ocaml" {>= "4.14"}
+  "dune" {>= "3.13"}
+  (("rocq-core" {>= "9.0" & < "9.2~"} & "coq-core" {>= "9.0" & < "9.2~"})
+   | "coq" {>= "8.19.0" & < "9.2~"})
+]
+authors: ["The HoTT Library Development Team"]
+dev-repo: "git+https://github.com/HoTT/HoTT.git"
+synopsis: "The Homotopy Type Theory library"
+description: """
+To use the HoTT library, the following flags must be passed to coqc:
+  -noinit -indices-matter
+To use the HoTT library in a project, add the following to _CoqProject:
+  -arg -noinit
+  -arg -indices-matter
+"""
+tags: [ "logpath:HoTT" ]
+url {
+  src: "https://github.com/HoTT/Coq-HoTT/archive/refs/tags/V9.1.tar.gz"
+  checksum: "sha512=134caf34ea9353967325699fc211b7df0eb32654b34b70c8eed321da3da937b45e823c5e925058840593c9cb3c26617dac945a3e64d2cf04e9d9bc9216d7616d"
+}
\ No newline at end of file
diff --git a/package_picks/package-pick-9.1~2026.01.sh b/package_picks/package-pick-9.1~2026.01.sh
index 834b15eb3e..69c75cbcc6 100644
--- a/package_picks/package-pick-9.1~2026.01.sh
+++ b/package_picks/package-pick-9.1~2026.01.sh
@@ -52,6 +52,8 @@ PACKAGES="${PACKAGES} PIN.ocamlfind.1.9.8+relocatable" # TODO port patch to 1.9.
 PACKAGES="${PACKAGES} PIN.dune.3.21.0" # 3.17.2 has issues on Windows: cairo doesn't find cairo.h
 PACKAGES="${PACKAGES} PIN.dune-configurator.3.21.0"
 # The Coq compiler coqc and the Coq standard library
+PACKAGES="${PACKAGES} PIN.rocq-runtime.9.1.0"
+PACKAGES="${PACKAGES} PIN.rocq-core.9.1.0"
 PACKAGES="${PACKAGES} PIN.coq.9.1.0"
 PACKAGES="${PACKAGES} PIN.rocq-stdlib.9.0.0" # modified after discuted with Théo to bump to 9.1.0
 # Tester avec 9.0.0, avoir une version qui marche et ensuite bump et voir le nombre de paquets qui sont cassés.
@@ -112,7 +114,7 @@ then
   PACKAGES="${PACKAGES} coq-corn.9.0.0"
 
   # Homotopy Type Theory (HoTT)
-  #PACKAGES="${PACKAGES} coq-hott.9.0" # error compilation
+  PACKAGES="${PACKAGES} coq-hott.9.1" # error compilation
 
   # Univalent Mathematics (UniMath)
   # Note: coq-unimath requires too much memory for 32 bit architectures
@@ -133,8 +135,8 @@ then
   PACKAGES="${PACKAGES} coq-menhirlib.20250903 menhir.20250903" # modified
   PACKAGES="${PACKAGES} rocq-equations.1.3.1+9.1" # modified
   PACKAGES="${PACKAGES} rocq-aac-tactics.9.0.0"
-  PACKAGES="${PACKAGES} coq-unicoq.1.6+9.1" # modified
-  PACKAGES="${PACKAGES} coq-mtac2.1.4+9.1" # modified linked with unicoq
+  #PACKAGES="${PACKAGES} coq-unicoq.1.6+8.20" # error
+  #PACKAGES="${PACKAGES} coq-mtac2.1.4+9.0" # error with unicoq
   PACKAGES="${PACKAGES} coq-quickchick.2.1.1"
   PACKAGES="${PACKAGES} coq-hammer-tactics.1.3.2+9.1" # modified
   if [[ "$OSTYPE" != cygwin ]]