Skip to content

Use class `IntoFUpd` in tactic `wp_value_head`

Robbert Krebbers requested to merge ci/robbert/into_fupd into master

This MR adds the following class:

Class IntoFUpd `{!BiFUpd PROP} E (P Q : PROP) :=
  into_fupd : P ={E}=∗ Q.

This class is then used to implement the "smart" update-adding in wp_value_head.

While the total amount of code increases, most of it is general purpose. The actual code in heaplang.proofmode is smaller, which means that it's easier to port it to other Iris developments (like Iron, where I wanted to add this feature).

Merge request reports