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