Skip to content

Consistently name `wp_value_inv`

Robbert Krebbers requested to merge robbert/wp_value_inv into master

We use the following naming: wp_value' uses of_val and wp_value uses IntoVal.

We do not name wp_value_inv that way: there is only a version without the ', which uses of_val. This MR corrects that.

One note/question: wp_value does not include an update modality, while wp_value_fupd does. For wp_value_inv we cannot possibly have a version without the update modality, so I think it's redundant to have an _fupd version.

Merge request reports