diff --git a/.gitignore b/.gitignore
index 8f86398b6ba5..0e9dd91cdf38 100644
--- a/.gitignore
+++ b/.gitignore
@@ -97,6 +97,7 @@ test-suite/Datatypes.mli
 test-suite/bug_10796.ml
 test-suite/bug_10796.mli
 test-suite/**/*.time
+stdlib/test-suite/**/*.time
 
 # `nix build` (through flake) symlink
 result
diff --git a/stdlib/test-suite/Makefile b/stdlib/test-suite/Makefile
index ea621dd45d8e..4228d46eae63 100644
--- a/stdlib/test-suite/Makefile
+++ b/stdlib/test-suite/Makefile
@@ -195,9 +195,12 @@ summary:
 	  $(call summary_dir, "Success tests", success); \
 	  $(call summary_dir, "Bugs tests", bugs); \
 	  $(call summary_dir, "Output tests", output); \
+	  $(call summary_dir, "Miscellaneous tests", misc); \
 	  $(call summary_dir, "Complexity tests", complexity); \
+	  $(call summary_dir, "Micromega tests", micromega); \
 	  $(call summary_dir, "Module tests", modules); \
 	  $(call summary_dir, "STM tests", stm); \
+	  $(call summary_dir, "Ltac2 tests", ltac2); \
 	  nb_success=`grep -e $(log_success) -r . -l --include="*.log" --exclude-dir=logs | wc -l`; \
 	  nb_failure=`grep -e $(log_failure) -r . -l --include="*.log" --exclude-dir=logs | wc -l`; \
 	  nb_tests=`expr $$nb_success + $$nb_failure`; \
diff --git a/stdlib/test-suite/micromega/bug_14054.v b/stdlib/test-suite/micromega/bug_14054.v
index 18262c310768..5a051a881ba3 100644
--- a/stdlib/test-suite/micromega/bug_14054.v
+++ b/stdlib/test-suite/micromega/bug_14054.v
@@ -10,7 +10,7 @@ From Stdlib.Init Require Byte.
 From Stdlib.Strings Require Byte.
 From Stdlib Require Import ZifyClasses Lia.
 
-Notation byte := Stdlib.Init.Byte.byte.
+Notation byte := Corelib.Init.Byte.byte.
 
 Module byte.
   Definition unsigned(b: byte): Z := Z.of_N (Byte.to_N b).