Fix missing checks in stdlib test suite

.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

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`; \

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).