Skip to content

Rename `X_length` into `length_X`.

Robbert Krebbers requested to merge robbert/length_X into master

This follows https://github.com/coq/coq/pull/18564 This closes #213 (closed)

We didn't include our own copies of app_length and seq_length, but used those from the standard library. To make sure we can use them (without deprecation warnings) until support for Coq 8.19 is dropped, I included our own copies for the transition period. This was also suggested by @tchajed in #213 (closed).

Merge request reports