Check-world found two interesting regressions:

1. The Inria folks like to treat warnings as errors, which breaks now because the warning number changed.
2. The C code produced by Karamel in merkle-tree doesn't compile due to incorrect function names (?!):

MerkleTree.c: In function 'mt_init_hash':
MerkleTree.c:86:10: error: implicit declaration of function 'MerkleTree_Low_Hashfunctions_init_hash'; did you mean 'MerkleTree_Low_Hashfunctions_free_hash'? [-Werror=implicit-function-declaration]
   86 |   return MerkleTree_Low_Hashfunctions_init_hash(hash_size);
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      |          MerkleTree_Low_Hashfunctions_free_hash
MerkleTree.c:86:10: error: returning 'int' from a function with return type 'uint8_t *' {aka 'unsigned char *'} makes pointer from integer without a cast [-Werror=int-conversion]
   86 |   return MerkleTree_Low_Hashfunctions_init_hash(hash_size);
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

I guess I am the Inria folk who like to treat warning as errors (sorry!), I can disable some more warnings if needed. I am doing this mainly because I was annoyed by the many warnings that shouldn't be warnings (e.g. #2705), but also because I think it's best practice (e.g. to ensure we don't have the proof splitting warning sprinkled throughout the project)

Sorry, that wasn't meant negatively at all! The F* library has lots of warnings too, and I agree it would be nicer to avoid them in the first place.

No worries, didn't take that negatively!

Check-world only reports two regressions now:

• dy-star: I believe this is only must_erase_for_extraction vs. erasable.
• steel: fixes here: Correctly erase functions. steel#204

This does not fix much without #3665, as effect promotion allows coercion from unit -> erased nat to unit -> GTot (erased nat) (giving you essentially the same bug). Shelving this for now until we have a plan for how to deal with the fallout from #3665.