Update iris.

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"}

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 {

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.

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: *)