Another try at removing strings.length

See discussion in !129 (merged) The idea of this version is to have two notations, one which shadows the bad definition Strings.length and the other which shadows the bad Notation List.length, which is bad because it is parsing only.

theories/base.v

@@ -9,8 +9,11 @@ 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. *)