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.

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.