Commit 8c243bde authored by Janno's avatar Janno

Fix unintential eta-expansion in `wp_value_head`.

parent a42fcf07
......@@ -89,7 +89,7 @@ Definition wp_value_head {Σ} `{heapG Σ} {Δ} {s}
{E : coPset} {e : language.expr heap_lang}
{Φ : language.val heap_lang iProp Σ}
:
M ((envs_entails Δ (WP e @ s; E {{ v, Φ v }}))%I *m mlist _) :=
M ((envs_entails Δ (WP e @ s; E {{ Φ }}))%I *m mlist _) :=
e' <- evar _;
TT.apply (tac_wp_value Δ s E Φ e e')
<**> TT.apply_
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment