diff --git a/CHANGELOG.md b/CHANGELOG.md
index aa35700dbba1ebb4ed6d66bc0513b7977ee3aa6d..712efda11c973c60d43507ca8cda39c5bc9f36a8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -39,6 +39,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   explicitly (since TC search is performed less eagerly), and in few cases it is
   needed to unfold definitions explicitly (due to new unification algorithm
   behaving differently).
+* Removed `Core` type class for defining the total core; it is now always
+  defined in terms of the partial core. The only user of this type class was the
+  STS RA.
 
 ## Iris 3.2.0 (released 2019-08-29)
 
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 *)