another try

theories/base.v

@@ -3,19 +3,17 @@ that are used throughout the whole development. Most importantly it contains
 abstract interfaces for ordered structures, sets, and various other data
 structures. *)
 
-(** The order of this [Require Export] is important: The definition of [length]
-in [List] should shadow the definition of [length] in [String]. We also need
-to export [Datatypes] because [List] contains a [parsing only] notation for
-[length], not the actual definition of [length], which is in [Datatypes]. *)
-From Coq Require Export String Datatypes List.
-From Coq Require Export Morphisms RelationClasses Bool Utf8 Setoid.
+From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
 From Coq Require Import Permutation.
 Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 
-(** TODO: This hack should be removed once we drop support for Coq 8.10. It is
-needed for the transitive export/import bug that is fixed in Coq 8.11. *)
+(** 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. *)

theories/strings.v

 From Coq Require Import Ascii.
+From Coq Require Export String.
 From stdpp Require Export list.
 From stdpp Require Import countable.
 Set Default Proof Using "Type".
 
+(* To avoid randomly ending up with String.length because this module is
+imported hereditarily somewhere. *)
+Notation length := List.length.
+
 (** * Fix scopes *)
 Open Scope string_scope.
 (* Make sure [list_scope] has priority over [string_scope], so that