diff --git a/tests/length.ref b/tests/length.ref
index 59449dc75ebc922fc894dec772af1418936b433a..170c5a2b7236c1156aef4b101183a6bb40c54ebb 100644
--- a/tests/length.ref
+++ b/tests/length.ref
@@ -10,3 +10,35 @@ length
      : list ?A → nat
 where
 ?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
diff --git a/tests/length.v b/tests/length.v
index 33612bb153156415bc79bfd90e4c821e726d0574..e7bebe422d14b669d95b79688eed08c0efaf6386 100644
--- a/tests/length.v
+++ b/tests/length.v
@@ -1,7 +1,36 @@
+From stdpp Require prelude strings list.
+
 (** Check that we always get the [length] function on lists, not on strings. *)
-From stdpp Require Import prelude.
-Check length.
-From stdpp Require Import strings.
-Check length.
-From stdpp Require Import prelude.
-Check length.
\ No newline at end of file
+Module test1.
+  Import stdpp.base.
+  Check length.
+  Import stdpp.strings.
+  Check length.
+  Import stdpp.base.
+  Check length.
+End test1.
+
+Module test2.
+  Import stdpp.prelude.
+  Check length.
+  Import stdpp.strings.
+  Check length.
+  Import stdpp.prelude.
+  Check length.
+End test2.
+
+Module test3.
+  Import stdpp.strings.
+  Check length.
+  Import stdpp.prelude.
+  Check length.
+End test3.
+
+Module test4.
+  Import stdpp.list.
+  Check length.
+  Import stdpp.strings.
+  Check length.
+  Import stdpp.list.
+  Check length.
+End test4.