Fix `Export` order for `length`. Remove `length` hack in strings.

The notation in strings was a hack to shadow the length function on strings with those on lists.

@msammler and I figured out how to change the imports to fix this problem without the hack. Basically, stdpp.base exports Coq.Strings and Coq.List in the right order, so the shadowing is done right. As a consequence Coq.Strings should never be exported by hand.

This approach seems to work among all supported Coq versions.

We also added a test.

theories/strings.v

 From Coq Require Import Ascii.
 From Coq Require Export String.
+(** Re-export [Coq.Datatypes] so that the [length] function refers to the one on
+lists instead of strings. Note that [length] is defined in [Coq.Datatypes] and
+not [Coq.Lists]. *)
+From Coq Require Export Datatypes.
 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
-   the "++" notation designates list concatenation. *)
+(** Make sure [list_scope] has priority over [string_scope], so that the [++]
+notation designates list concatenation. *)
 Open Scope list_scope.
 Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
 Arguments String.append : simpl never.