diff --git a/guix.scm b/guix.scm
index 821c451baaab8ab70fdd33bb70f9346fec58bc4e..48f35f86576801ca1ffaf97ec24c1a6c1311ea0d 100644
--- a/guix.scm
+++ b/guix.scm
@@ -32,8 +32,8 @@
 
 (define stdpp-commit "d98ab4e4adf80e34f2b38d95e125fa6d128e09e7")
 (define stdpp-sha256 (base32 "09dsdja35ls25h4dd842wiadhjjilazfl5kywn2vgrav4vzi3s5m")) ;; sha256 hash of the specific std++ checkout
-(define iris-commit "0495f1197f506ee13dacc242ebefda2f880951c9")
-(define iris-sha256 (base32 "185vjm2sir3765g2c0f9d62mpv8dvl34sblqdh71x2g8cz0hiwzc")) ;; sha256 hash of the specific std++ checkout
+(define iris-commit "4760ad334dba7d4b683700e52ecb444b944daeed")
+(define iris-sha256 (base32 "0cxhjzbsl21w0vnl3ks826mba115xyg3bbxznirp42cwh4x24yxn")) ;; sha256 hash of the specific std++ checkout
 (define %source-dir (dirname (current-filename)))
 
 (define-public coq-stdpp
diff --git a/opam b/opam
index b4107671d4241e38b7be8382a8587234adb91128..af2168f01fc5219c4831f1e04900d6119464b351 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-26.0.0495f119") | (= "dev") }
+  "coq-iris" { (= "dev.2019-04-07.4.4760ad33") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/typing/types.v b/theories/typing/types.v
index af8a9c618ed4e2c123ac228f5501ebf50c9b607c..28347ddb247305a84571a364f5036f8b8eb87682 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -68,7 +68,7 @@ Notation "∀: τ" :=
 Notation "∃: τ" :=
   (TExists Ï„%ty)
   (at level 100, Ï„ at level 200) : FType_scope.
-Notation "'ref' Ï„" := (Tref Ï„%ty) (at level 30, right associativity): FType_scope.
+Notation "'ref' Ï„" := (Tref Ï„%ty) (at level 10, Ï„ at next level, right associativity): FType_scope.
 
 (** * Typing judgements *)
 Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).