diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 79b06f6179517eea4e97fc604962eb0b8cdf233c..d17814897691803b63a9817c12dc05267746764a 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-11-26.1.04496bec") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-01-25.0.04d22616") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/type.v b/theories/typing/type.v
index f81e2802f08a49d056e049c9e0ed3ff7a3516193..a33db3109fadb53fc787c92d4af2f8e83883e8ca 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -193,7 +193,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.
@@ -245,7 +245,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.