diff --git a/refinedc.opam b/refinedc.opam
index 72f99cb2c8a27943b619cbf0806db1c72674795c..766ed8a1cbf7ab201aeb5e894a573c6b8b66f4c8 100644
--- a/refinedc.opam
+++ b/refinedc.opam
@@ -17,7 +17,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
 
 depends: [
   "coq" { (>= "8.12.0" & < "8.13~") }
-  "coq-iris" { (= "dev.2021-01-20.0.7b8a6255") | (= "dev") }
+  "coq-iris" { (= "dev.2021-01-27.0.cb569d36") | (= "dev") }
   "dune" {>= "2.7.0"}
   "cerberus" {= "~dev"}
   "cmdliner" {>= "1.0.4"}
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 116ccb9f020c9fe67df35aa8e6c97f9927b88b88..c8a3689bc8a3a79f46e7e05c0176453713149fc1 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -8,19 +8,19 @@ From refinedc.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 addr (prodR (prodR fracR lock_stateR) (agreeR (prodO alloc_idO mbyteO))).
 
-Definition allocR : cmraT :=
+Definition allocR : cmra :=
   agreeR allocationO.
 
-Definition allocsUR : ucmraT :=
+Definition allocsUR : ucmra :=
   gmapUR Z allocR.
 
-Definition fntblUR : ucmraT :=
+Definition fntblUR : ucmra :=
   gmapUR loc (agreeR functionO).
 
 Class heapG Σ := HeapG {
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 456e3f39b293e51cb08aedf639bd007e92c4ec93..f6fa18e753658467dc610c5b349ca6bebd6f91d5 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -130,7 +130,7 @@ Section function.
       by iApply ("IH" with "[] [] [] [] [$] [$]"); iPureIntro; simplify_eq.
     - iIntros (v). iDestruct 1 as (x') "[Hv [Hls HPr]]".
       iDestruct (big_sepL2_app_inv with "Hls") as "[$ $]".
-      { rewrite Hlen1 Hlen3. by eapply Forall2_length. }
+      { rewrite Hlen1 Hlen3. left. by eapply Forall2_length. }
       iApply ("HΦ" with "Hv").
       by iApply ("Hr" with "HPr").
   Qed.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index de8741ee74bd9662425d47f77c164455b13cf6ac..8e97021bbb4843fd4e01da1b516809feae70ed3a 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -444,7 +444,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_own_ne n:
     Proper (dist n ==> eq ==> eq ==> dist n) ty_own.
@@ -505,7 +505,7 @@ Section ofe.
   (*     + destruct 1. eexists _. eauto. *)
   (*     + destruct 1. by econstructor. *)
   (* Qed. *)
-  (* Canonical Structure rtypeO : ofeT := OfeT rtype rtype_ofe_mixin. *)
+  (* Canonical Structure rtypeO : ofe := Ofe rtype rtype_ofe_mixin. *)
 
 
   (* Global Instance with_refinement_ne n: *)