Merge branch 'ike/ucmra_fixes' into 'master'

Made refcell state coercion implementation agnostic

See merge request !31

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