Bump Iris.

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

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 {

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.