diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index bc8b4867e4e1793937ecf689dcb97fef53e5a3f7..925241d25051139cd10a7362cbf01f3a12df1609 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-12-10.1.872fe77b") | (= "dev") }
+  "coq-iris" { (= "dev.2021-01-25.1.21b7ffa1") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 9ad9af67647590b084e8a8d811eb03bd2352b7f3..5fa2cf3cb47933f2a31d863d47572220acedb92f 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -9,13 +9,13 @@ From lrust.lang Require Export lang.
 Set Default Proof Using "Type".
 Import uPred.
 
-Definition lock_stateR : cmraT :=
+Definition lock_stateR : cmra :=
   csumR (exclR unitO) natR.
 
-Definition heapUR : ucmraT :=
+Definition heapUR : ucmra :=
   gmapUR loc (prodR (prodR fracR lock_stateR) (agreeR valO)).
 
-Definition heap_freeableUR : ucmraT :=
+Definition heap_freeableUR : ucmra :=
   gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
 
 Class heapG Σ := HeapG {
diff --git a/theories/typing/type.v b/theories/typing/type.v
index b090940de3318eb50d539bb0b3eecd412c61cf17..dcbd4c113db2e276a068d616e5bcd90414956300 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -190,7 +190,7 @@ Section ofe.
     - split; [by destruct 1|by intros [[??] ?]; constructor].
     - split; [by destruct 1|by intros [[??] ?]; constructor].
   Qed.
-  Canonical Structure typeO : ofeT := OfeT type type_ofe_mixin.
+  Canonical Structure typeO : ofe := Ofe type type_ofe_mixin.
 
   Global Instance ty_size_ne n : Proper (dist n ==> eq) ty_size.
   Proof. intros ?? EQ. apply EQ. Qed.
@@ -242,7 +242,7 @@ Section ofe.
     - split; [by destruct 1|by constructor].
     - split; [by destruct 1|by constructor].
   Qed.
-  Canonical Structure stO : ofeT := OfeT simple_type st_ofe_mixin.
+  Canonical Structure stO : ofe := Ofe simple_type st_ofe_mixin.
 
   Global Instance st_own_ne n :
     Proper (dist n ==> eq ==> eq ==> dist n) st_own.