diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index c94185a..4f66827 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -18,7 +18,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
+          - 'mathcomp/mathcomp:2.6.0-rocq-prover-9.2'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4
diff --git a/AnIntroductionToSmallScaleReflectionInCoq/section4.v b/AnIntroductionToSmallScaleReflectionInCoq/section4.v
index 870de31..e3cc06a 100644
--- a/AnIntroductionToSmallScaleReflectionInCoq/section4.v
+++ b/AnIntroductionToSmallScaleReflectionInCoq/section4.v
@@ -72,7 +72,7 @@ end.
 (* Using the ssreflect pattern conditional this code can be shrinked *)
 (*into the actual program present in the seq library:*)
 Fixpoint alternate_tuto s1 s2 :=
-  if s1 is x :: s' then x :: (tuto_cat s' s2) else s2.
+  if s1 is x :: s' then x :: (alternate_tuto s' s2) else s2.
 
 
 (* The proof goes by induction on the first list. We do not need to be *)
@@ -97,7 +97,7 @@ Proof. by move=> x s1 s2; elim: s1 x => [|y s1 IHs] x //=; rewrite IHs. Qed.
 
 Fixpoint tuto_take n s {struct s} :=
   match s, n with
-  | x :: s', n'.+1 => x :: take n' s'
+  | x :: s', n'.+1 => x :: tuto_take n' s'
   | _, _ => [::]
   end.
 
@@ -107,7 +107,7 @@ Fixpoint tuto_take n s {struct s} :=
 (*allows more fixpoints further defined to decrease structurally *)
 Fixpoint tuto_drop n s {struct s} :=
   match s, n with
-  | _ :: s', n'.+1 => drop n' s'
+  | _ :: s', n'.+1 => tuto_drop n' s'
   | _, _ => s
   end.
 
@@ -142,7 +142,7 @@ Search _ (size (take _ _) = _).
 have Hns : n <= size s by apply: leq_trans (leq_addl _ _) (ltnW Hmn).
 rewrite !(size_takel Hns).
 (* We directly rewrite the condition proved forward *)
-have -> : m + n < n = false by rewrite ltnNge leq_addl.  
+have -> : (m + n < n) = false by rewrite ltnNge leq_addl.  
 rewrite size_drop.
 have -> :  m < size s - n by rewrite ltnNge leq_subLR -ltnNge addnC.
 by rewrite addnK catA.
diff --git a/AnIntroductionToSmallScaleReflectionInCoq/section6.v b/AnIntroductionToSmallScaleReflectionInCoq/section6.v
index afd8f74..5a32e6e 100644
--- a/AnIntroductionToSmallScaleReflectionInCoq/section6.v
+++ b/AnIntroductionToSmallScaleReflectionInCoq/section6.v
@@ -52,6 +52,8 @@ Search _ cat uniq.
 rewrite cat_uniq.
 Search _ uniq map.
 rewrite !map_inj_uniq.
+ + by move=> x y [].
+ + by move=> x y [].
  Search _ uniq Finite.enum.
  Search _ Finite.enum.
  + rewrite -!enumT.
@@ -61,8 +63,6 @@ rewrite !map_inj_uniq.
  case/mapP=> x hx -> /=.
  case/mapP.
  done.
- + by move=> x y [].
- + by move=> x y [].
 Qed.
 
 (* here is the clean script resulting from the proevious one *)
@@ -88,7 +88,7 @@ Lemma prod_enum_uniq : forall T1 T2, uniq (tuto_prod_enum T1 T2).
 Proof.
 move=> T1 T2; rewrite /tuto_prod_enum; move: (enum_uniq T1) (enum_uniq T2).
 elim: (enum T1) (enum T2)=> [|x1 l1 ihl1] l2 //=; case/andP=> hx1 uniq_l1 uniq_l2.
-rewrite cat_uniq ihl1 // andbT map_inj_uniq; last by move=> x y [].
+rewrite cat_uniq ihl1 // andbT map_inj_uniq; first by move=> x y [].
 rewrite uniq_l2 /=; apply/hasP=> [[u]] /= h1; case/mapP=> y l2y e.
 move: h1; rewrite e; elim: l1 hx1 {uniq_l1 ihl1} => [|x3 l3 ihl3 ] //=.
 rewrite in_cons negb_or; case/andP=> h1 h2.
@@ -205,7 +205,7 @@ by move=> h; apply/pred0P=> x /=; case Ax : (x \in A); rewrite ?andbF // h.
 Qed.
 
 Lemma tuto_subsetPn : forall A B,
-  reflect (exists2 x, x \in A & x \notin B) (~~ (A \subset B)).
+  reflect (exists2 x, (x \in A) & (x \notin B)) (~~ (A \subset B)).
 Proof.
 rewrite unlock.
 move=> A B; apply: (iffP idP).
@@ -553,7 +553,7 @@ End setOpsExos.
 Section MinSet.
 
 Variable T : finType.
-Notation sT := {set T}.
+Abbreviation sT := {set T}.
 
 Implicit Types A B C : sT.
 Implicit Type P : pred sT.
diff --git a/AnSsreflectTutorial/tutorial_Gonthier_LeRoux.v b/AnSsreflectTutorial/tutorial_Gonthier_LeRoux.v
index 06276a3..a9a05d2 100644
--- a/AnSsreflectTutorial/tutorial_Gonthier_LeRoux.v
+++ b/AnSsreflectTutorial/tutorial_Gonthier_LeRoux.v
@@ -1,5 +1,5 @@
 
-Require PeanoNat.
+From Stdlib Require PeanoNat.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat div.
 
 (*****************************************************************************)
@@ -239,7 +239,7 @@ Print leq.
 
 Print subn.
 
-Print subn_rec.
+Print Nat.sub.
 
 Lemma concrete_big_leq : 0 <= 51.
 Proof. by []. Qed.
diff --git a/README.md b/README.md
index edc4be9..f1da2ac 100644
--- a/README.md
+++ b/README.md
@@ -28,8 +28,24 @@ It contains
   - Laurent Théry
 - License: [MIT License](LICENSE)
 - Additional dependencies:
-  - [MathComp ssreflect 2.5 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.6 or later](https://math-comp.github.io)
 - Rocq/Coq namespace: `tutorial_material`
 - Related publication(s): none
 
 ## Building and installation instructions
+
+To build and install manually, you need to make sure that all the
+libraries this development depends on are installed.  The easiest way to do that
+is still to rely on opam:
+
+``` shell
+git clone https://github.com/math-comp/tutorial_material.git
+cd tutorial_material
+opam repo add rocq-released https://rocq-prover.org/opam/released
+opam install --deps-only .
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
+```
+
+
+
diff --git a/Ssreflect15min/quesako.v b/Ssreflect15min/quesako.v
index 3e98542..e755376 100644
--- a/Ssreflect15min/quesako.v
+++ b/Ssreflect15min/quesako.v
@@ -36,7 +36,7 @@ of the tactic language, because the methodology is independent.
 
 (* == Reminder: large scale reflection *)
 
-From Coq Require Import ZArith.
+From Stdlib Require Import ZArith.
 
 Open Scope Z_scope.
 
@@ -72,7 +72,7 @@ a type equipped with a, possibly axiomatic and non-computational,
  ring structure into a type for polynomial expressions. *)
 
 
-Require Import Arith Ring.
+From Stdlib Require Import Arith Ring.
 
 Goal forall (n : nat) (b : bool) (f : bool -> nat), 
   n + (f b) * n + n * (n + 1) = n * (n + (f b)) + 2 * n. 
@@ -151,7 +151,7 @@ Qed.
 
 (* From now on, we will use the tactic extension. It is distributed 
 as part of the Coq proof assistant, and loaded by the following Import *)
-From Coq Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 
 (* The extension implements an improved rewrite tactic language. We
 mention only two important features:
@@ -197,7 +197,7 @@ Features associated with this objective are:
    Demo: Prove that the concatenation (s1 ++ s2) of two lists is
    duplicate-free if and only if (s2 ++ s2) is also duplicate-free. **)
 
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
  Module ExerciseSeq.
 
diff --git a/SummerSchoolSophia/exercise1_solution.v b/SummerSchoolSophia/exercise1_solution.v
index efade5a..6ced5a9 100644
--- a/SummerSchoolSophia/exercise1_solution.v
+++ b/SummerSchoolSophia/exercise1_solution.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
diff --git a/SummerSchoolSophia/exercise2_solution.v b/SummerSchoolSophia/exercise2_solution.v
index 458a42a..7ef0311 100644
--- a/SummerSchoolSophia/exercise2_solution.v
+++ b/SummerSchoolSophia/exercise2_solution.v
@@ -2,7 +2,7 @@
       #<a href='https://www-sop.inria.fr/teams/marelle/types18/cheatsheet.pdf'>https://www-sop.inria.fr/teams/marelle/types18/cheatsheet.pdf</a>#
 *)
 
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Implicit Type p q r : bool.
 Implicit Type m n a b c : nat.
@@ -33,8 +33,8 @@ Lemma orbC p q : p || q = q || p.
 
 (** *** Exercise 4:
 *)
-Goal forall p q,    (p && q) || (   p && ~~ q) || 
-                 (~~ p && q) || (~~ p && ~~ q). 
+Goal forall p q,    (p && q) || (   p && (~~ q)) || 
+                 (~~ p && q) || (~~ p && (~~ q)). 
 (*D*)Proof. by move=> p q; case: p; case: q. Qed.
 
 (** *** Exercise 5 :
diff --git a/SummerSchoolSophia/exercise3_solution.v b/SummerSchoolSophia/exercise3_solution.v
index cb96ec9..4ee05e1 100644
--- a/SummerSchoolSophia/exercise3_solution.v
+++ b/SummerSchoolSophia/exercise3_solution.v
@@ -2,7 +2,7 @@
       #<a href='https://www-sop.inria.fr/teams/marelle/types18/cheatsheet.pdf'>https://www-sop.inria.fr/teams/marelle/types18/cheatsheet.pdf</a>#
 *)
 
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Implicit Type p q r : bool.
 Implicit Type m n a b c : nat.
diff --git a/SummerSchoolSophia/exercise4_solution.v b/SummerSchoolSophia/exercise4_solution.v
index 4ebc6ee..03b8d72 100644
--- a/SummerSchoolSophia/exercise4_solution.v
+++ b/SummerSchoolSophia/exercise4_solution.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Implicit Type P Q R : Prop.
 
diff --git a/SummerSchoolSophia/exercise5_solution.v b/SummerSchoolSophia/exercise5_solution.v
index 31acf8d..59b8d05 100644
--- a/SummerSchoolSophia/exercise5_solution.v
+++ b/SummerSchoolSophia/exercise5_solution.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Module  easy.
 
@@ -74,7 +74,7 @@ Qed.
 
 Lemma implyP (b1 b2 : bool) : reflectl (b1 -> b2) (b1 ==> b2).
 Proof.
-(*D*)by case: b1; case: b2; [ left | right | left ..] => //= /(_ isT).
+(*D*)by (case: b1; case: b2; [ left | right | left ..]) => //= /(_ isT).
 Qed.
 
 End reflect1.
diff --git a/SummerSchoolSophia/exercise6_solution.v b/SummerSchoolSophia/exercise6_solution.v
index 6cd467b..5d47c93 100644
--- a/SummerSchoolSophia/exercise6_solution.v
+++ b/SummerSchoolSophia/exercise6_solution.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -135,7 +135,7 @@ Proof.
 (*D*)have /(congr1 (muln^~ (b ^ n))) := aB1_eq.
 (*D*)rewrite mulnBl mulnDl mul1n.
 (*D*)move=> /(congr1 (addn^~ (b ^ n - 1))).
-(*D*)rewrite addnBA ?expn_gt0 ?b_gt0// subnK; last first.
+(*D*)rewrite addnBA ?expn_gt0 ?b_gt0// subnK.
 (*D*)  by rewrite -[X in X <= _]mul1n leq_mul2r a_gt0 orbT.
 (*D*)rewrite -mulnA -expnS -addnA => ->.
 (*D*)rewrite edivn_eq addnBA ?expn_gt0 ?b_gt0//.
@@ -154,7 +154,7 @@ contains no prime number.
 #<div># *)
 Lemma ex5 n m : n`! + 2 <= m <= n`! + n -> ~~ prime m.
 Proof.
-(*D*)move=> m_in; move: (m_in); rewrite -[m](@subnKC n`!); last first.
+(*D*)move=> m_in; move: (m_in); rewrite -[m](@subnKC n`!).
 (*D*)  by rewrite (@leq_trans (n`! + 2)) ?leq_addr//; by case/andP: m_in.
 (*D*)set k := (_ - _); rewrite !leq_add2l => /andP[k_gt1 k_le_n].
 (*D*)apply/primePn; right; exists k.
diff --git a/SummerSchoolSophia/exercise7_solution.v b/SummerSchoolSophia/exercise7_solution.v
index f35f75a..e64c307 100644
--- a/SummerSchoolSophia/exercise7_solution.v
+++ b/SummerSchoolSophia/exercise7_solution.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 
 (** *** Exercise 1 :
@@ -263,7 +263,7 @@ Proof.
 (*D*)rewrite -{1}sum_gauss -doubleMr (big_morph _ (mulnDr _) (muln0 _)).
 (*D*)rewrite -{3}[n]muln1 -{3}[n]subn0 -sum_nat_const_nat.
 (*D*)rewrite -!doubleD -!big_split /=.
-(*D*)rewrite (eq_big_nat _ _ (_ : forall i, _ -> _ = i.+1 ^ 3 - i ^3)) => [|i H]; last first.
+(*D*)rewrite (eq_big_nat _ _ (_ : forall i, _ -> _ = i.+1 ^ 3 - i ^3)) => [i H|].
 (*D*)  rewrite -[LHS](addKn (i ^ 3)); congr (_ - _).
 (*D*)  by sring.
 (*D*)apply: etrans (_ : (n^3).*2 = _).
diff --git a/SummerSchoolSophia/exercise8_solution.v b/SummerSchoolSophia/exercise8_solution.v
index a4e9c89..89cf8a1 100644
--- a/SummerSchoolSophia/exercise8_solution.v
+++ b/SummerSchoolSophia/exercise8_solution.v
@@ -1,5 +1,5 @@
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect. 
+From mathcomp Require Import boot. 
 
 
 (** *** Exercise 1:
diff --git a/SummerSchoolSophia/lesson1.v b/SummerSchoolSophia/lesson1.v
index 8e2576d..6ade376 100644
--- a/SummerSchoolSophia/lesson1.v
+++ b/SummerSchoolSophia/lesson1.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/SummerSchoolSophia/lesson2.v b/SummerSchoolSophia/lesson2.v
index ec67d48..3a11958 100644
--- a/SummerSchoolSophia/lesson2.v
+++ b/SummerSchoolSophia/lesson2.v
@@ -1,5 +1,5 @@
 
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -160,7 +160,7 @@ Equality statement between tests reads as  "if and only if".
 
 Print Nat.sub.
 
-Lemma eqn_leq (m n : nat) : m == n = (m <= n) && (n <= m).
+Lemma eqn_leq (m n : nat) : (m == n) = (m <= n) && (n <= m).
 Abort.
 
 (**
@@ -171,7 +171,7 @@ Abort.
 #<div>#
 *)
 
-Lemma eqn_leq (m n : nat) : m == n = (m <= n <= m).
+Lemma eqn_leq (m n : nat) : (m == n) = (m <= n <= m).
 Abort.
 
 (**
@@ -248,16 +248,16 @@ Proof. by []. Qed.
 #<div>#
 *)
 
-Goal  3 < 3 = false.
+Goal  (3 < 3) = false.
 Proof. by []. Qed.
 
-Goal  4 <= 3 = false.
+Goal  (4 <= 3) = false.
 Proof. by []. Qed.
 
 Lemma leq0n n : 0 <= n.
 Proof. by []. Qed.
 
-Lemma ltn0 n : n.+1 <= 0 = false.
+Lemma ltn0 n : (n.+1 <= 0) = false.
 Proof. by []. Qed.
 
 Lemma ltnS m n : (m.+1 <= n.+1) = (m <= n).
diff --git a/SummerSchoolSophia/lesson3.v b/SummerSchoolSophia/lesson3.v
index 8486158..b63f18a 100644
--- a/SummerSchoolSophia/lesson3.v
+++ b/SummerSchoolSophia/lesson3.v
@@ -1,5 +1,5 @@
 
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -38,10 +38,10 @@ apply: contraLR.
 rewrite -leqNgt.
 move=> leq_p_m.
 rewrite dvdn_addr.
-  by rewrite gtnNdvd // prime_gt1.
 (* Search _ dvdn factorial.*)
-apply: dvdn_fact.
-by rewrite leq_p_m prime_gt0.
+  apply: dvdn_fact.
+  by rewrite leq_p_m prime_gt0.
+by rewrite gtnNdvd // prime_gt1.
 Qed.
 (**
 #</div>#
diff --git a/SummerSchoolSophia/lesson4.v b/SummerSchoolSophia/lesson4.v
index ad56419..ddd2caf 100644
--- a/SummerSchoolSophia/lesson4.v
+++ b/SummerSchoolSophia/lesson4.v
@@ -1,5 +1,5 @@
 
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/SummerSchoolSophia/lesson5.v b/SummerSchoolSophia/lesson5.v
index c3f7819..37def34 100644
--- a/SummerSchoolSophia/lesson5.v
+++ b/SummerSchoolSophia/lesson5.v
@@ -1,5 +1,5 @@
 
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/SummerSchoolSophia/lesson6.v b/SummerSchoolSophia/lesson6.v
index 9f9497a..0459e14 100644
--- a/SummerSchoolSophia/lesson6.v
+++ b/SummerSchoolSophia/lesson6.v
@@ -1,5 +1,5 @@
 
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/SummerSchoolSophia/lesson7.v b/SummerSchoolSophia/lesson7.v
index 9ce4c78..77b8476 100644
--- a/SummerSchoolSophia/lesson7.v
+++ b/SummerSchoolSophia/lesson7.v
@@ -1,5 +1,5 @@
 
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -431,8 +431,8 @@ Proof.
 About  big_morph.
 Fail rewrite big_morph.
 rewrite (big_morph _ (_ : {morph double : x y / x + y}) (_ : 0.*2 = 0)).
-- by [].
 - move=> x y; exact: doubleD.
+- by [].
 by [].
 Qed.
 
diff --git a/SummerSchoolSophia/lesson8.v b/SummerSchoolSophia/lesson8.v
index 022046f..5e6d251 100644
--- a/SummerSchoolSophia/lesson8.v
+++ b/SummerSchoolSophia/lesson8.v
@@ -1,5 +1,5 @@
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boot.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -238,14 +238,14 @@ Check (Finite.clone _ (#| 'I_4 | .-tuple bool)).
 Check {ffun 'I_4 * 'I_6 -> nat} : Type.
 Check (Equality.clone _ {ffun 'I_4 * 'I_6 -> nat}) : Type.
 
-From mathcomp Require Import all_algebra.
+From mathcomp Require Import algebra.
 Open Scope ring_scope.
 
 Print matrix.
 
 Section Rings.
 
-Variable R : ringType.
+Variable R : pzRingType.
 
 Check forall x : R, x * 1 == x.
 
diff --git a/coq-tutorial_material.opam b/coq-tutorial_material.opam
index b844d87..17f5643 100644
--- a/coq-tutorial_material.opam
+++ b/coq-tutorial_material.opam
@@ -26,7 +26,7 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" 
-  "coq-mathcomp-ssreflect" {(>= "2.5.0")}
+  "coq-mathcomp-ssreflect" {(>= "2.6.0")}
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index a825897..2ba9a0f 100644
--- a/meta.yml
+++ b/meta.yml
@@ -34,18 +34,18 @@ license:
   identifier: MIT
 
 supported_rocq_versions:
-  text: '9.1 or later'
-  opam: '{(>= "9.1")}'
+  text: '9.2 or later'
+  opam: '{(>= "9.2")}'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.5.0")}'
+    version: '{(>= "2.6.0")}'
   description: |-
-    [MathComp ssreflect 2.5 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.6 or later](https://math-comp.github.io)
 
 tested_coq_opam_versions:
-- version: '2.5.0-rocq-prover-9.1'
+- version: '2.6.0-rocq-prover-9.2'
   repo: 'mathcomp/mathcomp'
 
 namespace: tutorial_material