diff --git a/test/serlib/genarg/libTactics.v b/test/serlib/genarg/libTactics.v
index 5f895f69e..e455a4483 100644
--- a/test/serlib/genarg/libTactics.v
+++ b/test/serlib/genarg/libTactics.v
@@ -44,7 +44,7 @@
 
 Set Implicit Arguments.
 
-Require Import Stdlib.Lists.List.
+Require Import Stdlib.Lists.ListDef.
 
 
 (* ********************************************************************** *)
@@ -55,7 +55,9 @@ Require Import Stdlib.Lists.List.
   Lemma test : forall b, b = false.
   time eauto 7. (* takes over 4 seconds  to fail! *) *)
 
+(* now requires Stdlib
 #[global] Remove Hints Bool.trans_eq_bool.
+*)
 
 
 (* ********************************************************************** *)
@@ -260,7 +262,7 @@ Notation "'>>' v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13" :=
 
 Ltac list_boxer_of E :=
   match type of E with
-  | List.list Boxer => constr:(E)
+  | list Boxer => constr:(E)
   | _ => constr:((boxer E)::nil)
   end.
 
@@ -370,7 +372,9 @@ Ltac fast_rm_inside E :=
     Note: the tactic [number_to_nat] is extended in [LibInt] to
     take into account the [int] type, alias for [Z]. *)
 
-Require Stdlib.Numbers.BinNums Stdlib.ZArith.BinInt.
+Require Stdlib.Numbers.BinNums Stdlib.BinNums.IntDef.
+(* now requries stdlib
+Require Stdlib.ZArith.BinInt.
 
 Definition ltac_int_to_nat (x:BinInt.Z) : nat :=
   match x with
@@ -435,6 +439,7 @@ Tactic Notation "ltac_set" "(" ident(X) ":=" constr(E) ")" "at" constr(K) :=
   | 13%nat => set (X := E) at 13
   | _ => fail "ltac_set: arity not supported"
   end.
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -453,6 +458,7 @@ Tactic Notation "show" tactic(tac) :=
 Lemma dup_lemma : forall P, P -> P -> P.
 Proof using. auto. Qed.
 
+(* now requires Stdlib
 Ltac dup_tactic N :=
   match number_to_nat N with
   | 0 => idtac
@@ -464,6 +470,7 @@ Tactic Notation "dup" constr(N) :=
   dup_tactic N.
 Tactic Notation "dup" :=
   dup 2.
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -596,6 +603,7 @@ Ltac get_fun_arg E :=
     then calls tactic [Tac], and finally unfolds [P]. Syntax
     [ltac_action_at K of E in H do Tac] is also available. *)
 
+(*
 Tactic Notation "ltac_action_at" constr(K) "of" constr(E) "do" tactic(Tac) :=
   let p := fresh "TEMP" in ltac_pattern E at K;
   match goal with |- ?P _ => set (p:=P) end;
@@ -605,6 +613,7 @@ Tactic Notation "ltac_action_at" constr(K) "of" constr(E) "in" hyp(H) "do" tacti
   let p := fresh "TEMP" in ltac_pattern E at K in H;
   match type of H with ?P _ => set (p:=P) in H end;
   Tac; unfold p in H; clear p.
+*)
 
 (** [protects E do Tac] temporarily assigns a name to the expression [E]
     so that the execution of tactic [Tac] will not modify [E]. This is
@@ -1530,6 +1539,7 @@ Proof using. intros. subst. auto. Qed.
 
 End equatesLemma.
 
+(* now requires Stdlib
 Ltac equates_lemma n :=
   match number_to_nat n with
   | 0 => constr:(equates_0)
@@ -1547,7 +1557,7 @@ Ltac equates_one n :=
 
 Ltac equates_several E cont :=
   let all_pos := match type of E with
-    | List.list Boxer => constr:(E)
+    | list Boxer => constr:(E)
     | _ => constr:((boxer E)::nil)
     end in
   let rec go pos :=
@@ -1578,6 +1588,7 @@ Tactic Notation "applys_eq" constr(H) constr(n1) constr(n2) constr(n3) :=
   applys_eq H (>> n1 n2 n3).
 Tactic Notation "applys_eq" constr(H) constr(n1) constr(n2) constr(n3) constr(n4) :=
   applys_eq H (>> n1 n2 n3 n4).
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -2103,7 +2114,7 @@ Tactic Notation "sets_eq_let" ident(X) "in" hyp(H) :=
 
 Ltac rewrites_base E cont :=
   match type of E with
-  | List.list Boxer => forwards_then E cont
+  | list Boxer => forwards_then E cont
   | _ => cont E; fast_rm_inside E
   end.
 
@@ -2194,6 +2205,7 @@ Ltac rewrite_except H EQ :=
     Syntaxes [rewrites <- E at K] and [rewrites E at K in H]
     are also available. *)
 
+(*
 Tactic Notation "rewrites" constr(E) "at" constr(K) :=
   match type of E with ?T1 = ?T2 =>
     ltac_action_at K of T1 do (rewrites E) end.
@@ -2206,6 +2218,7 @@ Tactic Notation "rewrites" constr(E) "at" constr(K) "in" hyp(H) :=
 Tactic Notation "rewrites" "<-" constr(E) "at" constr(K) "in" hyp(H) :=
   match type of E with ?T1 = ?T2 =>
     ltac_action_at K of T2 in H do (rewrites <- E in H) end.
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -2229,11 +2242,13 @@ Tactic Notation "replaces" constr(E) "with" constr(F) "in" hyp(H) :=
     with [F] in the current goal. Syntax [replaces E at K with F in H]
     is also available. *)
 
+(*
 Tactic Notation "replaces" constr(E) "at" constr(K) "with" constr(F) :=
   let T := fresh "TEMP" in assert (T: E = F); [ | rewrites T at K; clear T ].
 
 Tactic Notation "replaces" constr(E) "at" constr(K) "with" constr(F) "in" hyp(H) :=
   let T := fresh "TEMP" in assert (T: E = F); [ | rewrites T at K in H; clear T ].
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -2519,6 +2534,7 @@ Tactic Notation "subst_eq" constr(E) :=
 (* ---------------------------------------------------------------------- *)
 (** ** Tactics to work with proof irrelevance *)
 
+(* now requires Stdlib
 Require Import Stdlib.Logic.ProofIrrelevance.
 
 (** [pi_rewrite E] replaces [E] of type [Prop] with a fresh
@@ -2535,6 +2551,7 @@ Tactic Notation "pi_rewrite" constr(E) :=
   pi_rewrite_base E ltac:(fun X => rewrite X).
 Tactic Notation "pi_rewrite" constr(E) "in" hyp(H) :=
   pi_rewrite_base E ltac:(fun X => rewrite X in H).
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -2564,6 +2581,7 @@ Tactic Notation "fequal" :=
     [fequals] applies to goals of the form [f x1 .. xN = f y1 .. yN]
     and produces some subgoals of the form [xi = yi]). *)
 
+(* now requires Stdlib
 Ltac fequal_post :=
   first [ reflexivity | congruence | apply proof_irrelevance | idtac ].
 
@@ -2575,6 +2593,7 @@ Tactic Notation "fequals" :=
 
 Tactic Notation "fequals_rec" :=
   repeat (progress fequals).
+*)
 
 
 
@@ -3098,13 +3117,16 @@ Tactic Notation "cases_if'" :=
     [inductions E gen X1 .. XN] is a shorthand for
     [dependent induction E generalizing X1 .. XN]. *)
 
+(* now requires Stdlib
 Require Import Stdlib.Program.Equality.
+*)
 
 Ltac inductions_post :=
   unfold eq' in *.
 
 Tactic Notation "inductions" ident(E) :=
   dependent induction E; inductions_post.
+(* now requires Stdlib
 Tactic Notation "inductions" ident(E) "gen" ident(X1) :=
   dependent induction E generalizing X1; inductions_post.
 Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2) :=
@@ -3127,6 +3149,7 @@ Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2)
 Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2)
  ident(X3) ident(X4) ident(X5) ident(X6) ident(X7) ident(X8) :=
   dependent induction E generalizing X1 X2 X3 X4 X5 X6 X7 X8; inductions_post.
+*)
 
 (** [induction_wf IH: E X] is used to apply the well-founded induction
     principle, for a given well-founded relation. It applies to a goal
@@ -3189,6 +3212,7 @@ Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
     judgment that includes a counter for the maximal height
     (see LibTacticsDemos for an example) *)
 
+(* now Requires Stdlib
 Require Import Stdlib.Arith.Compare_dec.
 Require Import Lia.
 
@@ -3211,6 +3235,7 @@ Ltac induct_height_step x :=
  end.
 
 Ltac induct_height := induct_height_step O.
+*)
 
 
 (* ********************************************************************** *)
@@ -3339,9 +3364,11 @@ Tactic Notation "splits" :=
 (** [splits N] is similar to [splits], except that it will unfold as many
     definitions as necessary to obtain an [N]-ary conjunction. *)
 
+(*
 Tactic Notation "splits" constr(N) :=
   let N := number_to_nat N in
   splits_tactic N.
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -3373,9 +3400,11 @@ Tactic Notation "destructs" constr(T) :=
     except that it does not require to manually specify N different
     names. Remark that it is not restricted to N-ary conjunctions. *)
 
+(*
 Tactic Notation "destructs" constr(N) constr(T) :=
   let N := number_to_nat N in
   destructs_conjunction_tactic N T.
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -3425,11 +3454,13 @@ Ltac get_goal_disjunction_arity :=
     but for more complex unfolding one should use the tactic
     [branch K of N]. *)
 
+(*
 Tactic Notation "branch" constr(K) :=
   let K := number_to_nat K in
   unfold_goal_until_disjunction;
   let N := get_goal_disjunction_arity in
   branch_tactic K N.
+*)
 
 (** [branch K of N] is similar to [branch K] except that the
     arity of the disjunction [N] is given manually, and so this
@@ -3437,10 +3468,12 @@ Tactic Notation "branch" constr(K) :=
     In other words, applies to a goal of the form
     [P1 \/ ... \/ PK \/ ... \/ PN] and leaves the goal [PK]. *)
 
+(*
 Tactic Notation "branch" constr(K) "of" constr(N) :=
   let N := number_to_nat N in
   let K := number_to_nat K in
   branch_tactic K N.
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -3469,9 +3502,11 @@ Tactic Notation "branches" constr(T) :=
     forced to [N]. This version is useful to unfold definitions
     on the fly. *)
 
+(*
 Tactic Notation "branches" constr(N) constr(T) :=
   let N := number_to_nat N in
   destructs_disjunction_tactic N T.
+*)
 
 (** [branches] automatically finds a hypothesis [h] that is a disjunction
     and destructs it. *)
@@ -3556,6 +3591,7 @@ Tactic Notation "exists" constr(T1) "," constr(T2) "," constr(T3) "," constr(T4)
    from that of [exists ___] is the case where the goal is a
    definition which yields an existential only after unfolding. *)
 
+(*
 Tactic Notation "exists___" constr(N) :=
   let rec aux N :=
     match N with
@@ -3563,8 +3599,10 @@ Tactic Notation "exists___" constr(N) :=
     | S ?N' => esplit; aux N'
     end in
   let N := number_to_nat N in aux N.
+*)
 
   (* --TODO: deprecated *)
+(*
 Tactic Notation "exists___" :=
   let N := get_goal_existential_arity in
   exists___ N.
@@ -3575,6 +3613,7 @@ Tactic Notation "exists" :=
 
   (* --TODO: [exists_all] is the new syntax for [exists___] *)
 Tactic Notation "exists_all" := exists___.
+*)
 
 (* ---------------------------------------------------------------------- *)
 (** Existentials and conjunctions in hypotheses *)
@@ -3775,6 +3814,7 @@ Tactic Notation "dauto" :=
    and thus cannot be extended, e.g. [simpl] and [unfold].
    For these, notation such as [simpl~] will not be available. *)
 
+(*
 Tactic Notation "equates" "~" constr(E) :=
    equates E; auto_tilde.
 Tactic Notation "equates" "~" constr(n1) constr(n2) :=
@@ -3792,6 +3832,7 @@ Tactic Notation "applys_eq" "~" constr(H) constr(n1) constr(n2) constr(n3) :=
   applys_eq H n1 n2 n3; auto_tilde.
 Tactic Notation "applys_eq" "~" constr(H) constr(n1) constr(n2) constr(n3) constr(n4) :=
   applys_eq H n1 n2 n3 n4; auto_tilde.
+*)
 
 Tactic Notation "apply" "~" constr(H) :=
   sapply H; auto_tilde.
@@ -4047,12 +4088,14 @@ Tactic Notation "erewrite" "~" constr(E) :=
 
 Tactic Notation "fequal" "~" :=
   fequal; auto_tilde.
+(*
 Tactic Notation "fequals" "~" :=
   fequals; auto_tilde.
 Tactic Notation "pi_rewrite" "~" constr(E) :=
   pi_rewrite E; auto_tilde.
 Tactic Notation "pi_rewrite" "~" constr(E) "in" hyp(H) :=
   pi_rewrite E in H; auto_tilde.
+*)
 
 Tactic Notation "invert" "~" hyp(H) :=
   invert H; auto_tilde.
@@ -4104,11 +4147,14 @@ Tactic Notation "iff" "~" simple_intropattern(I) :=
   iff I; auto_tilde.
 Tactic Notation "splits" "~" :=
   splits; auto_tilde.
+(*
 Tactic Notation "splits" "~" constr(N) :=
   splits N; auto_tilde.
+*)
 
 Tactic Notation "destructs" "~" constr(T) :=
   destructs T; auto_tilde.
+(*
 Tactic Notation "destructs" "~" constr(N) constr(T) :=
   destructs N T; auto_tilde.
 
@@ -4116,18 +4162,23 @@ Tactic Notation "branch" "~" constr(N) :=
   branch N; auto_tilde.
 Tactic Notation "branch" "~" constr(K) "of" constr(N) :=
   branch K of N; auto_tilde.
+*)
 
 Tactic Notation "branches" "~" :=
   branches; auto_tilde.
 Tactic Notation "branches" "~" constr(T) :=
   branches T; auto_tilde.
+(*
 Tactic Notation "branches" "~" constr(N) constr(T) :=
   branches N T; auto_tilde.
+*)
 
 Tactic Notation "exists" "~" :=
   exists; auto_tilde.
+(*
 Tactic Notation "exists___" "~" :=
   exists___; auto_tilde.
+*)
 Tactic Notation "exists" "~" constr(T1) :=
   exists T1; auto_tilde.
 Tactic Notation "exists" "~" constr(T1) constr(T2) :=
@@ -4168,6 +4219,7 @@ Tactic Notation "exists" "~" constr(T1) "," constr(T2) "," constr(T3) ","
     Exception: use [subs*] instead of [subst*] if you
     import the library [Stdlib.Classes.Equivalence]. *)
 
+(*
 Tactic Notation "equates" "*" constr(E) :=
    equates E; auto_star.
 Tactic Notation "equates" "*" constr(n1) constr(n2) :=
@@ -4185,6 +4237,7 @@ Tactic Notation "applys_eq" "*" constr(H) constr(n1) constr(n2) constr(n3) :=
   applys_eq H n1 n2 n3; auto_star.
 Tactic Notation "applys_eq" "*" constr(H) constr(n1) constr(n2) constr(n3) constr(n4) :=
   applys_eq H n1 n2 n3 n4; auto_star.
+*)
 
 Tactic Notation "apply" "*" constr(H) :=
   sapply H; auto_star.
@@ -4443,12 +4496,14 @@ Tactic Notation "erewrite" "*" constr(E) :=
 
 Tactic Notation "fequal" "*" :=
   fequal; auto_star.
+(*
 Tactic Notation "fequals" "*" :=
   fequals; auto_star.
 Tactic Notation "pi_rewrite" "*" constr(E) :=
   pi_rewrite E; auto_star.
 Tactic Notation "pi_rewrite" "*" constr(E) "in" hyp(H) :=
   pi_rewrite E in H; auto_star.
+*)
 
 Tactic Notation "invert" "*" hyp(H) :=
   invert H; auto_star.
@@ -4501,28 +4556,38 @@ Tactic Notation "iff" "*" simple_intropattern(I) :=
   iff I; auto_star.
 Tactic Notation "splits" "*" :=
   splits; auto_star.
+(*
 Tactic Notation "splits" "*" constr(N) :=
   splits N; auto_star.
+*)
 
 Tactic Notation "destructs" "*" constr(T) :=
   destructs T; auto_star.
+(*
 Tactic Notation "destructs" "*" constr(N) constr(T) :=
   destructs N T; auto_star.
+*)
 
+(*
 Tactic Notation "branch" "*" constr(N) :=
   branch N; auto_star.
 Tactic Notation "branch" "*" constr(K) "of" constr(N) :=
   branch K of N; auto_star.
+*)
 
 Tactic Notation "branches" "*" constr(T) :=
   branches T; auto_star.
+(*
 Tactic Notation "branches" "*" constr(N) constr(T) :=
   branches N T; auto_star.
+*)
 
 Tactic Notation "exists" "*" :=
   exists; auto_star.
+(*
 Tactic Notation "exists___" "*" :=
   exists___; auto_star.
+*)
 Tactic Notation "exists" "*" constr(T1) :=
   exists T1; auto_star.
 Tactic Notation "exists" "*" constr(T1) constr(T2) :=
@@ -4784,6 +4849,7 @@ Tactic Notation "clears_but" ident(H1) ident(H2) ident(H3) ident(H4) :=
 Tactic Notation "clears_but" ident(H1) ident(H2) ident(H3) ident(H4) ident(H5) :=
   clears_but_core ltac:(fun _ => gen H1 H2 H3 H4 H5).
 
+(*
 Lemma demo_clears_all_and_clears_but :
   forall x y:nat, y < 2 -> x = x -> x >= 2 -> x < 3 -> True.
 Proof using.
@@ -4797,6 +4863,7 @@ Proof using.
   clears_but M2 M3. auto.
   clears_but x y. auto.
 Qed.
+*)
 
 (** [clears_last] clears the last hypothesis in the context.
     [clears_last N] clears the last [N] hypotheses in the context. *)
@@ -4804,14 +4871,18 @@ Qed.
 Tactic Notation "clears_last" :=
   match goal with H: ?T |- _ => clear H end.
 
+(*
 Ltac clears_last_base N :=
   match number_to_nat N with
   | 0 => idtac
   | S ?p => clears_last; clears_last_base p
   end.
+*)
 
+(*
 Tactic Notation "clears_last" constr(N) :=
   clears_last_base N.
+*)
 
 
 (* ********************************************************************** *)