Use class `IntoFUpd` in tactic `wp_value_head`
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).