Skip to content

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

Robbert Krebbers requested to merge ci/robbert/length into master

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.

Edited by Robbert Krebbers

Merge request reports