thery · Nov 9, 2026 · Nov 9, 2026
diff --git 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
@@ -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
@@ -18,7 +18,7 @@
 Definition unit1 := unit.
 Lemma tuto_unit_enumP : Finite.axiom [:: tt]. Proof. by case. Qed.

 #[verbose]
 HB.instance Definition _ := isFinite.Build unit1 tuto_unit_enumP.

 (******************************************************************************)
@@ -52,6 +52,8 @@
 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 @@
  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 @@
 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 @@
 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).
@@ -372,10 +372,10 @@
 Structure tuto_tuple_of  : Type := 
  TutoTuple {tuto_tval :> seq T; _ : size tuto_tval == n}.

 #[verbose]
 HB.instance Definition _ := [isSub for tuto_tval].

 End Def.

 Canonical Structure nil_tuto_tuple (T : Type) :=
   TutoTuple (erefl _ : @size T [::] == 0).
@@ -386,18 +386,18 @@
 Lemma tuto_cat_tupleP : forall T n1 n2 (t1 : n1.-tuple T) (t2 : n2.-tuple T),
  size (t1 ++ t2) == n1 + n2.
 Proof. by move=> T n1 n2 t1 t2; rewrite size_cat !size_tuple. Qed.
 Canonical Structure cat_tuple T n1 n2 t1 t2 := Tuple (@cat_tupleP T n1 n2 t1 t2).


 Lemma drop_tupleP : forall T n m (t : n.-tuple T), size (drop m t) == n - m.
 Proof. by move=> T n m t; rewrite size_drop size_tuple. Qed.

 Canonical Structure drop_tuple T n m t := Tuple (@drop_tupleP T n m t).

 Lemma take_tupleP : forall T n m (t : n.-tuple T), size (take m t) == minn m n.
 Proof. by move=> T n m t; rewrite size_take size_tuple eqxx. Qed.

 Canonical Structure take_tuple T n m t := Tuple (@take_tupleP T n m t).

 Lemma rot_tupleP : forall T n m (t : n.-tuple T), size (rot m t) == n.
 Proof. by move=> T n m t; rewrite size_rot size_tuple. Qed.
@@ -553,7 +553,7 @@
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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.