diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index f136a89b5df3e5e0fb8c81f42037b9c27239ff7a..d4911684494259e0272cdb233a9c2be6b6beb83d 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -17,12 +17,11 @@ Global Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
 Proof. solve_inG. Qed.
 
 Definition refcell_st := option ((lft * Datatypes.bool) * frac * positive).
-Definition refcell_st_to_R (st : refcell_st) : refcell_stR :=
+Coercion refcell_st_to_R (st : refcell_st) : refcell_stR :=
   match st with
   | None => None
   | Some (x, q, n) => Some (to_agree x, q, n)
   end.
-Coercion refcell_st_to_R : refcell_st >-> ucmra_car.
 
 Definition Z_of_refcell_st (st : refcell_st) : Z :=
   match st with