From 3c5086b21ac65a34d4d047c66c139c3e96ae71fe Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 31 Oct 2018 13:49:11 +0100
Subject: [PATCH] Get rid of useless IntoVal uses.

---
 theories/heap_lang/lib/spawn.v |  7 +++----
 theories/heap_lang/lifting.v   | 10 +++++-----
 2 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 158e8c59f..a213fec88 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -44,11 +44,10 @@ Global Instance join_handle_ne n l :
 Proof. solve_proper. Qed.
 
 (** The main proofs. *)
-Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
-  IntoVal e f →
-  {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
+Lemma spawn_spec (Ψ : val → iProp Σ) (f : val) :
+  {{{ WP f #() {{ Ψ }} }}} spawn f {{{ l, RET #l; join_handle l Ψ }}}.
 Proof.
-  iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=. wp_lam.
+  iIntros (Φ) "Hf HΦ". rewrite /spawn /=. wp_lam.
   wp_alloc l as "Hl".
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index b9a9c0bf5..143dc1424 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -317,12 +317,12 @@ Proof.
   - iApply "HΦ". done.
 Qed.
 
-Lemma wp_resolve_proph e1 e2 p v w:
-  IntoVal e1 (LitV (LitProphecy p)) →
-  IntoVal e2 w →
-  {{{ proph p v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}.
+Lemma wp_resolve_proph p v w:
+  {{{ proph p v }}}
+    ResolveProph (Val $ LitV $ LitProphecy p) (Val w)
+  {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}.
 Proof.
-  iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
   iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
   iSplit; first by eauto.
-- 
GitLab