diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index f302796bebbbfd4714d1d8a602d923ff8c423297..3ea70b65a0f24fd8b5f715016cad68a014b8e460 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -176,13 +176,9 @@ Hint Mode CmraTotal ! : typeclass_instances.
 
 (** The function [core] returns a dummy when used on CMRAs without total
 core. *)
-Class Core (A : Type) := core : A → A.
-Hint Mode Core ! : typeclass_instances.
+Definition core `{PCore A} (x : A) : A := default x (pcore x).
 Instance: Params (@core) 2 := {}.
 
-Instance core' `{PCore A} : Core A := λ x, default x (pcore x).
-Arguments core' _ _ _ /.
-
 (** * CMRAs with a unit element *)
 Class Unit (A : Type) := ε : A.
 Arguments ε {_ _}.
@@ -479,7 +475,7 @@ Section total_core.
 
   Lemma cmra_pcore_core x : pcore x = Some (core x).
   Proof.
-    rewrite /core /core'. destruct (cmra_total x) as [cx ->]. done.
+    rewrite /core. destruct (cmra_total x) as [cx ->]. done.
   Qed.
   Lemma cmra_core_l x : core x ⋅ x ≡ x.
   Proof.
@@ -769,7 +765,7 @@ Section cmra_morphism.
   Local Set Default Proof Using "Type*".
   Context {A B : cmraT} (f : A → B) `{!CmraMorphism f}.
   Lemma cmra_morphism_core x : f (core x) ≡ core (f x).
-  Proof. unfold core, core'. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
+  Proof. unfold core. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
   Lemma cmra_morphism_monotone x y : x ≼ y → f x ≼ f y.
   Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
   Lemma cmra_morphism_monotoneN n x y : x ≼{n} y → f x ≼{n} f y.
@@ -1037,9 +1033,7 @@ Section mnat.
   Qed.
   Lemma mnat_ra_mixin : RAMixin mnat.
   Proof.
-    apply ra_total_mixin; try by eauto.
-    - solve_proper.
-    - solve_proper.
+    apply ra_total_mixin; apply _ || eauto.
     - intros x y z. apply Nat.max_assoc.
     - intros x y. apply Nat.max_comm.
     - intros x. apply Max.max_idempotent.
@@ -1162,7 +1156,7 @@ Section prod.
   Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
     core (a, b) = (core a, core b).
   Proof.
-    rewrite /core /core' {1}/pcore /=.
+    rewrite /core {1}/pcore /=.
     rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
   Qed.
 
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index f162ca23e6fce3ee8a9f08d60454eb98d40d5399..9b58faaa19e075ad2a181530563ec844059d5c15 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra updates.
 Set Default Proof Using "Type".
 
-Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
+Record DraMixin A `{Equiv A, PCore A, Disjoint A, Op A, Valid A} := {
   (* setoids *)
   mixin_dra_equivalence : Equivalence (≡@{A});
   mixin_dra_op_proper : Proper ((≡@{A}) ==> (≡) ==> (≡)) (⋅);
@@ -29,7 +29,7 @@ Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
 Structure draT := DraT {
   dra_car :> Type;
   dra_equiv : Equiv dra_car;
-  dra_core : Core dra_car;
+  dra_pcore : PCore dra_car;
   dra_disjoint : Disjoint dra_car;
   dra_op : Op dra_car;
   dra_valid : Valid dra_car;
@@ -38,13 +38,13 @@ Structure draT := DraT {
 Arguments DraT _ {_ _ _ _ _} _.
 Arguments dra_car : simpl never.
 Arguments dra_equiv : simpl never.
-Arguments dra_core : simpl never.
+Arguments dra_pcore : simpl never.
 Arguments dra_disjoint : simpl never.
 Arguments dra_op : simpl never.
 Arguments dra_valid : simpl never.
 Arguments dra_mixin : simpl never.
 Add Printing Constructor draT.
-Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid.
+Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
 
 (** Lifting properties from the mixin *)
 Section dra_mixin.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index 14773b60ed3a52f2265cf7fb0f9e026ba498b3dd..eb7751229d832969f04eb407b681590492314571 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -28,13 +28,8 @@ Section gset.
 
   Lemma gset_ra_mixin : RAMixin (gset K).
   Proof.
-    apply ra_total_mixin; eauto.
-    - solve_proper.
-    - solve_proper.
-    - solve_proper.
-    - intros X1 X2 X3. by rewrite !gset_op_union assoc_L.
-    - intros X1 X2. by rewrite !gset_op_union comm_L.
-    - intros X. by rewrite gset_core_self idemp_L.
+    apply ra_total_mixin; apply _ || eauto; [].
+    intros X. by rewrite gset_core_self idemp_L.
   Qed.
   Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
 
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index c5d07b8579261248035aa23d6daff46d0e58cf8a..410c9fef72d84ad525b7066d179bbdd681232f41 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -196,8 +196,8 @@ Instance sts_valid : Valid (car sts) := λ x,
   | auth s T => tok s ## T
   | frag S' T => closed S' T ∧ ∃ s, s ∈ S'
   end.
-Instance sts_core : Core (car sts) := λ x,
-  match x with
+Instance sts_core : PCore (car sts) := λ x,
+  Some match x with
   | frag S' _ => frag (up_set S' ∅ ) ∅
   | auth s _  => frag (up s ∅) ∅
   end.
@@ -394,7 +394,7 @@ Qed.
 
 Global Instance sts_frag_core_id S : CoreId (sts_frag S ∅).
 Proof.
-  constructor; split=> //= [[??]]. by rewrite /dra.dra_core /= sts.up_closed.
+  constructor; split=> //= [[??]]. by rewrite /dra.dra_pcore /= sts.up_closed.
 Qed.
 
 (** Inclusion *)