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.ref

-length : ∀ A : Type, list A → nat
-
-length is not universe polymorphic
-Arguments length {A}%type_scope _%list_scope
-length is transparent
-Expands to: Constant Coq.Init.Datatypes.length
-length : ∀ A : Type, list A → nat
-
-length is not universe polymorphic
-Arguments length {A}%type_scope _%list_scope
-length is transparent
-Expands to: Constant Coq.Init.Datatypes.length
-length : ∀ A : Type, list A → nat
-
-length is not universe polymorphic
-Arguments length {A}%type_scope _%list_scope
-length is transparent
-Expands to: Constant Coq.Init.Datatypes.length
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]
+length
+     : list ?A → nat
+where
+?A : [ |- Type]