diff --git a/tests/length.ref b/tests/length.ref
new file mode 100644
index 0000000000000000000000000000000000000000..170c5a2b7236c1156aef4b101183a6bb40c54ebb
--- /dev/null
+++ b/tests/length.ref
@@ -0,0 +1,44 @@
+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]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
diff --git a/tests/length.v b/tests/length.v
new file mode 100644
index 0000000000000000000000000000000000000000..e7bebe422d14b669d95b79688eed08c0efaf6386
--- /dev/null
+++ b/tests/length.v
@@ -0,0 +1,36 @@
+From stdpp Require prelude strings list.
+
+(** Check that we always get the [length] function on lists, not on strings. *)
+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.
diff --git a/theories/base.v b/theories/base.v
index da1cc243d1845d1483aa3f1487e6d08ed6acd099..7d63f1249391776006db679758172c8fd4b09307 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -9,6 +9,13 @@ Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 
+(** This notation is necessary to prevent [length] from being printed
+as [strings.length] if strings.v is imported and later base.v. See
+also strings.v and
+https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/144 and
+https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/129. *)
+Notation length := Datatypes.length.
+
 (** * Enable implicit generalization. *)
 (** This option enables implicit generalization in arguments of the form
    [`{...}] (i.e., anonymous arguments).  Unfortunately, it also enables