diff --git a/opam.pins b/opam.pins
index 67879a595bb5284c00e0c257f6cef657a803ab7c..642f2e56a3400e35bac618a9b5ed355c9fef0386 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0379384d795a443cb5ea31354644244f97a3299d
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b0418bd57b9341dbf5e58669c689201daa561bd7
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 65938cf201fdcaafc799bd6521d04b5c2434b15f..e2df4a414f26f1760d635d8d29095a2926443ebb 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Definition refcell_stR :=
-  optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) posR)).
+  optionUR (csumR (exclR unitC) (prodR (prodR (agreeR lftC) fracR) positiveR)).
 Class refcellG Σ :=
   RefCellG :> inG Σ (authR refcell_stR).