Handle renaming of List.app_length in Coq
std++ produces many copies of the following error message in Coq master (8.20+):
Warning: Notation app_length is deprecated since 8.20.
Use length_app instead.
[deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default]
There are two things we can do:
- Add
-w -deprecated-since-8.20
to handle this and similar issues. - Prove
length_app
ourselves and stop using the Coq definition. This is clearly backwards compatible and won't require any changes in the future.
I propose doing both of these - having length_app
is good for uniformity anyway, and we're essentially backporting the name change.