From bf743ebeab31ba67e66ba7274102a799ac96d3ca Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 14 Aug 2023 16:57:31 +0200
Subject: [PATCH] Made refcell state coercion implementation agnostic

---
 theories/typing/lib/refcell/refcell.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index f136a89b..d4911684 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
-- 
GitLab