More testing.

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]

tests/length.v

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