Skip to content

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:

  1. Add -w -deprecated-since-8.20 to handle this and similar issues.
  2. 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.