diff --git a/guix.scm b/guix.scm
index 5c515aba6bf8bd4233017cd8281f115a421a9678..ca9072bde8728e1374373995f325ecda80ea916b 100644
--- a/guix.scm
+++ b/guix.scm
@@ -30,8 +30,10 @@
   #:use-module (gnu packages coq)
   #:use-module ((guix licenses) #:prefix license:))
 
-(define stdpp-commit "f948024480ee7ab247be51cef058d21e36e3df24")
-(define iris-commit "2d1c83520d8c2656d1868dfa6d7e8a95fe3c6c4c")
+(define stdpp-commit "700545bb31db8c5268a6813bebaf0e4115d229d9")
+(define stdpp-sha256 (base32 "0i469sk69qb0bjxjaykralc3fr2zw2241dy350slydkas90xmjwk")) ;; sha256 hash of the specific std++ checkout
+(define iris-commit "9936cb1238afbd21e2202ecdb72c844b3c572f80")
+(define iris-sha256 (base32 "0jqk71197irjx0mpdmhb7bdlgyhjim172arjqal8chm3miwiag7f")) ;; sha256 hash of the specific std++ checkout
 (define %source-dir (dirname (current-filename)))
 
 (define-public coq-stdpp
@@ -47,8 +49,7 @@
                      (url "https://gitlab.mpi-sws.org/iris/stdpp.git")
                      (commit commit)))
                (file-name (git-file-name name version))
-               (sha256
-                (base32 "08myrcbxag16vr9axys7cvxqlgnpb5bxn9q7cmr3j84m31rn4s39"))))
+               (sha256 stdpp-sha256)))
       (build-system gnu-build-system)
       (native-inputs
        `( ;; need for egrep for tests
@@ -87,8 +88,7 @@
                      (url "https://gitlab.mpi-sws.org/iris/iris.git")
                      (commit commit)))
                (file-name (git-file-name name version))
-               (sha256
-                (base32 "1hlihcds432h367k8dijqsbzycf4lczdm0pw2p2xpwizagqwjv9b"))))
+               (sha256 iris-sha256)))
       (build-system gnu-build-system)
       (native-inputs
        `(;; need for egrep for tests
diff --git a/opam b/opam
index 7a115b0661c6be3cf6feb332dbb07c63b469d65f..994b1f7bf4009fab0fb180e654f516a10af3f335 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2019-03-15.0.33ee70bf") | (= "dev") }
+  "coq-iris" { (= "dev.2019-03-22.0.9936cb12") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index dc3d786674c52fe7bcdbc989f2d3b7f81a5739ff..1904ed2432bcdfd895b1f826d3f099ffcec5b9bd 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -132,8 +132,7 @@ Section rules.
     iFrame. iApply "Hclose". iNext.
     iExists (<[j:=fill K #()]> tp), σ.
     rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
-    eapply rtc_r, step_insert_no_fork; eauto.
-    eapply (ResolveProphS #p _ (of_val w)); eauto.
+    eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.
 
   (** Alloc, load, and store *)