From c2c847328f4925f8e41f9d600e047967091a64ec Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 8 Mar 2016 10:07:23 +0100
Subject: [PATCH] rename CMRA unit -> core

---
 algebra/agree.v                 |  2 +-
 algebra/auth.v                  | 10 ++--
 algebra/cmra.v                  | 94 ++++++++++++++++-----------------
 algebra/dec_agree.v             |  4 +-
 algebra/dra.v                   | 32 +++++------
 algebra/excl.v                  |  2 +-
 algebra/fin_maps.v              | 24 ++++-----
 algebra/frac.v                  |  4 +-
 algebra/iprod.v                 | 20 +++----
 algebra/option.v                | 12 ++---
 algebra/sts.v                   |  6 +--
 algebra/upred.v                 | 40 +++++++-------
 program_logic/adequacy.v        |  2 +-
 program_logic/ghost_ownership.v | 12 ++---
 program_logic/global_functor.v  |  4 +-
 program_logic/ownership.v       | 14 ++---
 program_logic/resources.v       | 12 ++---
 17 files changed, 147 insertions(+), 147 deletions(-)

diff --git a/algebra/agree.v b/algebra/agree.v
index a451a5091..4039c7e40 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -60,7 +60,7 @@ Program Instance agree_op : Op (agree A) := λ x y,
   {| agree_car := x;
      agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ≡{n}≡ y |}.
 Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
-Instance agree_unit : Unit (agree A) := id.
+Instance agree_core : Core (agree A) := id.
 Instance agree_div : Div (agree A) := λ x y, x.
 
 Instance: Comm (≡) (@op (agree A) _).
diff --git a/algebra/auth.v b/algebra/auth.v
index 0b1067885..8c036f102 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -85,8 +85,8 @@ Instance auth_validN : ValidN (auth A) := λ n x,
   | ExclBot => False
   end.
 Global Arguments auth_validN _ !_ /.
-Instance auth_unit : Unit (auth A) := λ x,
-  Auth (unit (authoritative x)) (unit (own x)).
+Instance auth_core : Core (auth A) := λ x,
+  Auth (core (authoritative x)) (core (own x)).
 Instance auth_op : Op (auth A) := λ x y,
   Auth (authoritative x â‹… authoritative y) (own x â‹… own y).
 Instance auth_div : Div (auth A) := λ x y,
@@ -117,10 +117,10 @@ Proof.
   - intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
   - by split; simpl; rewrite assoc.
   - by split; simpl; rewrite comm.
-  - by split; simpl; rewrite ?cmra_unit_l.
-  - by split; simpl; rewrite ?cmra_unit_idemp.
+  - by split; simpl; rewrite ?cmra_core_l.
+  - by split; simpl; rewrite ?cmra_core_idemp.
   - intros ??; rewrite! auth_included; intros [??].
-    by split; simpl; apply cmra_unit_preserving.
+    by split; simpl; apply cmra_core_preserving.
   - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
     { intros n a b1 b2 <-; apply cmra_includedN_l. }
    intros n [[a1| |] b1] [[a2| |] b2];
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 4fd0fac48..5001e5d06 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1,7 +1,7 @@
 From algebra Require Export cofe.
 
-Class Unit (A : Type) := unit : A → A.
-Instance: Params (@unit) 2.
+Class Core (A : Type) := core : A → A.
+Instance: Params (@core) 2.
 
 Class Op (A : Type) := op : A → A → A.
 Instance: Params (@op) 2.
@@ -34,10 +34,10 @@ Instance: Params (@includedN) 4.
 Hint Extern 0 (_ ≼{_} _) => reflexivity.
 
 Record CMRAMixin A
-    `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Div A} := {
+    `{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A, Div A} := {
   (* setoids *)
   mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
-  mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit;
+  mixin_cmra_core_ne n : Proper (dist n ==> dist n) core;
   mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
   mixin_cmra_div_ne n : Proper (dist n ==> dist n ==> dist n) div;
   (* valid *)
@@ -46,9 +46,9 @@ Record CMRAMixin A
   (* monoid *)
   mixin_cmra_assoc : Assoc (≡) (⋅);
   mixin_cmra_comm : Comm (≡) (⋅);
-  mixin_cmra_unit_l x : unit x ⋅ x ≡ x;
-  mixin_cmra_unit_idemp x : unit (unit x) ≡ unit x;
-  mixin_cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
+  mixin_cmra_core_l x : core x ⋅ x ≡ x;
+  mixin_cmra_core_idemp x : core (core x) ≡ core x;
+  mixin_cmra_core_preserving x y : x ≼ y → core x ≼ core y;
   mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
   mixin_cmra_op_div x y : x ≼ y → x ⋅ y ÷ x ≡ y;
   mixin_cmra_extend n x y1 y2 :
@@ -62,7 +62,7 @@ Structure cmraT := CMRAT {
   cmra_equiv : Equiv cmra_car;
   cmra_dist : Dist cmra_car;
   cmra_compl : Compl cmra_car;
-  cmra_unit : Unit cmra_car;
+  cmra_core : Core cmra_car;
   cmra_op : Op cmra_car;
   cmra_valid : Valid cmra_car;
   cmra_validN : ValidN cmra_car;
@@ -75,7 +75,7 @@ Arguments cmra_car : simpl never.
 Arguments cmra_equiv : simpl never.
 Arguments cmra_dist : simpl never.
 Arguments cmra_compl : simpl never.
-Arguments cmra_unit : simpl never.
+Arguments cmra_core : simpl never.
 Arguments cmra_op : simpl never.
 Arguments cmra_valid : simpl never.
 Arguments cmra_validN : simpl never.
@@ -83,7 +83,7 @@ Arguments cmra_div : simpl never.
 Arguments cmra_cofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmraT.
-Existing Instances cmra_unit cmra_op cmra_valid cmra_validN cmra_div.
+Existing Instances cmra_core cmra_op cmra_valid cmra_validN cmra_div.
 Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
 Canonical Structure cmra_cofeC.
 
@@ -93,8 +93,8 @@ Section cmra_mixin.
   Implicit Types x y : A.
   Global Instance cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x).
   Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
-  Global Instance cmra_unit_ne n : Proper (dist n ==> dist n) (@unit A _).
-  Proof. apply (mixin_cmra_unit_ne _ (cmra_mixin A)). Qed.
+  Global Instance cmra_core_ne n : Proper (dist n ==> dist n) (@core A _).
+  Proof. apply (mixin_cmra_core_ne _ (cmra_mixin A)). Qed.
   Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
   Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
   Global Instance cmra_div_ne n :
@@ -108,12 +108,12 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.
   Global Instance cmra_comm : Comm (≡) (@op A _).
   Proof. apply (mixin_cmra_comm _ (cmra_mixin A)). Qed.
-  Lemma cmra_unit_l x : unit x ⋅ x ≡ x.
-  Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed.
-  Lemma cmra_unit_idemp x : unit (unit x) ≡ unit x.
-  Proof. apply (mixin_cmra_unit_idemp _ (cmra_mixin A)). Qed.
-  Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
-  Proof. apply (mixin_cmra_unit_preserving _ (cmra_mixin A)). Qed.
+  Lemma cmra_core_l x : core x ⋅ x ≡ x.
+  Proof. apply (mixin_cmra_core_l _ (cmra_mixin A)). Qed.
+  Lemma cmra_core_idemp x : core (core x) ≡ core x.
+  Proof. apply (mixin_cmra_core_idemp _ (cmra_mixin A)). Qed.
+  Lemma cmra_core_preserving x y : x ≼ y → core x ≼ core y.
+  Proof. apply (mixin_cmra_core_preserving _ (cmra_mixin A)). Qed.
   Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
   Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
   Lemma cmra_op_div x y : x ≼ y → x ⋅ y ÷ x ≡ y.
@@ -175,7 +175,7 @@ Implicit Types x y z : A.
 Implicit Types xs ys zs : list A.
 
 (** ** Setoids *)
-Global Instance cmra_unit_proper : Proper ((≡) ==> (≡)) (@unit A _).
+Global Instance cmra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
 Proof. apply (ne_proper _). Qed.
 Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
 Proof.
@@ -236,15 +236,15 @@ Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
 Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y.
 Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
 
-(** ** Units *)
-Lemma cmra_unit_r x : x ⋅ unit x ≡ x.
-Proof. by rewrite (comm _ x) cmra_unit_l. Qed.
-Lemma cmra_unit_unit x : unit x ⋅ unit x ≡ unit x.
-Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed.
-Lemma cmra_unit_validN n x : ✓{n} x → ✓{n} unit x.
-Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
-Lemma cmra_unit_valid x : ✓ x → ✓ unit x.
-Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
+(** ** Core *)
+Lemma cmra_core_r x : x ⋅ core x ≡ x.
+Proof. by rewrite (comm _ x) cmra_core_l. Qed.
+Lemma cmra_core_core x : core x ⋅ core x ≡ core x.
+Proof. by rewrite -{2}(cmra_core_idemp x) cmra_core_r. Qed.
+Lemma cmra_core_validN n x : ✓{n} x → ✓{n} core x.
+Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
+Lemma cmra_core_valid x : ✓ x → ✓ core x.
+Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
 
 (** ** Div *)
 Lemma cmra_op_div' n x y : x ≼{n} y → x ⋅ y ÷ x ≡{n}≡ y.
@@ -260,7 +260,7 @@ Qed.
 Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
 Proof.
   split.
-  - by intros x; exists (unit x); rewrite cmra_unit_r.
+  - by intros x; exists (core x); rewrite cmra_core_r.
   - intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
     by rewrite assoc -Hy -Hz.
 Qed.
@@ -288,13 +288,13 @@ Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
 Lemma cmra_included_r x y : y ≼ x ⋅ y.
 Proof. rewrite (comm op); apply cmra_included_l. Qed.
 
-Lemma cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y.
+Lemma cmra_core_preservingN n x y : x ≼{n} y → core x ≼{n} core y.
 Proof.
   intros [z ->].
-  apply cmra_included_includedN, cmra_unit_preserving, cmra_included_l.
+  apply cmra_included_includedN, cmra_core_preserving, cmra_included_l.
 Qed.
-Lemma cmra_included_unit x : unit x ≼ x.
-Proof. by exists x; rewrite cmra_unit_l. Qed.
+Lemma cmra_included_core x : core x ≼ x.
+Proof. by exists x; rewrite cmra_core_l. Qed.
 Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
 Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
 Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
@@ -358,8 +358,8 @@ Section identity.
   Proof. by exists x; rewrite left_id. Qed.
   Global Instance cmra_empty_right_id : RightId (≡) ∅ (⋅).
   Proof. by intros x; rewrite (comm op) left_id. Qed.
-  Lemma cmra_unit_empty : unit ∅ ≡ ∅.
-  Proof. by rewrite -{2}(cmra_unit_l ∅) right_id. Qed.
+  Lemma cmra_core_empty : core ∅ ≡ ∅.
+  Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed.
 End identity.
 
 (** ** Local updates *)
@@ -468,7 +468,7 @@ Section cmra_transport.
   Proof. by intros ???; destruct H. Qed.
   Lemma cmra_transport_op x y : T (x â‹… y) = T x â‹… T y.
   Proof. by destruct H. Qed.
-  Lemma cmra_transport_unit x : T (unit x) = unit (T x).
+  Lemma cmra_transport_core x : T (core x) = core (T x).
   Proof. by destruct H. Qed.
   Lemma cmra_transport_validN n x : ✓{n} T x ↔ ✓{n} x.
   Proof. by destruct H. Qed.
@@ -486,25 +486,25 @@ End cmra_transport.
 
 (** * Instances *)
 (** ** Discrete CMRA *)
-Class RA A `{Equiv A, Unit A, Op A, Valid A, Div A} := {
+Class RA A `{Equiv A, Core A, Op A, Valid A, Div A} := {
   (* setoids *)
   ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x);
-  ra_unit_ne :> Proper ((≡) ==> (≡)) unit;
+  ra_core_ne :> Proper ((≡) ==> (≡)) core;
   ra_validN_ne :> Proper ((≡) ==> impl) valid;
   ra_div_ne :> Proper ((≡) ==> (≡) ==> (≡)) div;
   (* monoid *)
   ra_assoc :> Assoc (≡) (⋅);
   ra_comm :> Comm (≡) (⋅);
-  ra_unit_l x : unit x ⋅ x ≡ x;
-  ra_unit_idemp x : unit (unit x) ≡ unit x;
-  ra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
+  ra_core_l x : core x ⋅ x ≡ x;
+  ra_core_idemp x : core (core x) ≡ core x;
+  ra_core_preserving x y : x ≼ y → core x ≼ core y;
   ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x;
   ra_op_div x y : x ≼ y → x ⋅ y ÷ x ≡ y
 }.
 
 Section discrete.
   Context {A : cofeT} `{Discrete A}.
-  Context `{Unit A, Op A, Valid A, Div A} (ra : RA A).
+  Context `{Core A, Op A, Valid A, Div A} (ra : RA A).
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
@@ -523,7 +523,7 @@ End discrete.
 (** ** CMRA for the unit type *)
 Section unit.
   Instance unit_valid : Valid () := λ x, True.
-  Instance unit_unit : Unit () := λ x, x.
+  Instance unit_core : Core () := λ x, x.
   Instance unit_op : Op () := λ x y, ().
   Instance unit_div : Div () := λ x y, ().
   Global Instance unit_empty : Empty () := ().
@@ -541,7 +541,7 @@ Section prod.
   Context {A B : cmraT}.
   Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
   Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
-  Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)).
+  Instance prod_core : Core (A * B) := λ x, (core (x.1), core (x.2)).
   Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
   Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
   Instance prod_div : Div (A * B) := λ x y, (x.1 ÷ y.1, x.2 ÷ y.2).
@@ -569,10 +569,10 @@ Section prod.
     - by intros n x [??]; split; apply cmra_validN_S.
     - by split; rewrite /= assoc.
     - by split; rewrite /= comm.
-    - by split; rewrite /= cmra_unit_l.
-    - by split; rewrite /= cmra_unit_idemp.
+    - by split; rewrite /= cmra_core_l.
+    - by split; rewrite /= cmra_core_idemp.
     - intros x y; rewrite !prod_included.
-      by intros [??]; split; apply cmra_unit_preserving.
+      by intros [??]; split; apply cmra_core_preserving.
     - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
     - intros x y; rewrite prod_included; intros [??].
       by split; apply cmra_op_div.
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 5e6004f4a..202b80ffa 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -2,7 +2,7 @@ From algebra Require Export cmra.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
-Local Arguments unit _ _ !_ /.
+Local Arguments core _ _ !_ /.
 
 (* This is isomorphic to option, but has a very different RA structure. *)
 Inductive dec_agree (A : Type) : Type := 
@@ -26,7 +26,7 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
   | DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
   | _, _ => DecAgreeBot
   end.
-Instance dec_agree_unit : Unit (dec_agree A) := id.
+Instance dec_agree_core : Core (dec_agree A) := id.
 Instance dec_agree_div : Div (dec_agree A) := λ x y, x.
 
 Definition dec_agree_ra : RA (dec_agree A).
diff --git a/algebra/dra.v b/algebra/dra.v
index a9af3ad35..1909b430a 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -18,17 +18,17 @@ Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
 Instance: Params (@dra_included) 4.
 Local Infix "≼" := dra_included.
 
-Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Div A} := {
+Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A, Div A} := {
   (* setoids *)
   dra_equivalence :> Equivalence ((≡) : relation A);
   dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅);
-  dra_unit_proper :> Proper ((≡) ==> (≡)) unit;
+  dra_core_proper :> Proper ((≡) ==> (≡)) core;
   dra_valid_proper :> Proper ((≡) ==> impl) valid;
   dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x);
   dra_div_proper :> Proper ((≡) ==> (≡) ==> (≡)) div;
   (* validity *)
   dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
-  dra_unit_valid x : ✓ x → ✓ unit x;
+  dra_core_valid x : ✓ x → ✓ core x;
   dra_div_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ÷ x);
   (* monoid *)
   dra_assoc :> Assoc (≡) (⋅);
@@ -36,10 +36,10 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Div A} := {
   dra_disjoint_move_l x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
   dra_symmetric :> Symmetric (@disjoint A _);
   dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
-  dra_unit_disjoint_l x : ✓ x → unit x ⊥ x;
-  dra_unit_l x : ✓ x → unit x ⋅ x ≡ x;
-  dra_unit_idemp x : ✓ x → unit (unit x) ≡ unit x;
-  dra_unit_preserving x y : ✓ x → ✓ y → x ≼ y → unit x ≼ unit y;
+  dra_core_disjoint_l x : ✓ x → core x ⊥ x;
+  dra_core_l x : ✓ x → core x ⋅ x ≡ x;
+  dra_core_idemp x : ✓ x → core (core x) ≡ core x;
+  dra_core_preserving x y : ✓ x → ✓ y → x ≼ y → core x ≼ core y;
   dra_disjoint_div x y : ✓ x → ✓ y → x ≼ y → x ⊥ y ÷ x;
   dra_op_div x y : ✓ x → ✓ y → x ≼ y → x ⋅ y ÷ x ≡ y
 }.
@@ -88,9 +88,9 @@ Hint Unfold dra_included.
 Lemma validity_valid_car_valid (z : T) : ✓ z → ✓ validity_car z.
 Proof. apply validity_prf. Qed.
 Hint Resolve validity_valid_car_valid.
-Program Instance validity_unit : Unit T := λ x,
-  Validity (unit (validity_car x)) (✓ x) _.
-Solve Obligations with naive_solver auto using dra_unit_valid.
+Program Instance validity_core : Core T := λ x,
+  Validity (core (validity_car x)) (✓ x) _.
+Solve Obligations with naive_solver auto using dra_core_valid.
 Program Instance validity_op : Op T := λ x y,
   Validity (validity_car x â‹… validity_car y)
            (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _.
@@ -118,14 +118,14 @@ Proof.
       |by intros; rewrite assoc].
   - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
   - intros [x px ?]; split;
-      naive_solver eauto using dra_unit_l, dra_unit_disjoint_l.
-  - intros [x px ?]; split; naive_solver eauto using dra_unit_idemp.
-  - intros x y Hxy; exists (unit y ÷ unit x).
+      naive_solver eauto using dra_core_l, dra_core_disjoint_l.
+  - intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
+  - intros x y Hxy; exists (core y ÷ core x).
     destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *.
-    assert (py → unit x ≼ unit y)
-      by intuition eauto 10 using dra_unit_preserving.
+    assert (py → core x ≼ core y)
+      by intuition eauto 10 using dra_core_preserving.
     constructor; [|symmetry]; simpl in *;
-      intuition eauto using dra_op_div, dra_disjoint_div, dra_unit_valid.
+      intuition eauto using dra_op_div, dra_disjoint_div, dra_core_valid.
   - by intros [x px ?] [y py ?] (?&?&?).
   - intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
       intuition eauto 10 using dra_disjoint_div, dra_op_div.
diff --git a/algebra/excl.v b/algebra/excl.v
index a1dceaff4..1e85335c6 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -91,7 +91,7 @@ Instance excl_valid : Valid (excl A) := λ x,
 Instance excl_validN : ValidN (excl A) := λ n x,
   match x with Excl _ | ExclUnit => True | ExclBot => False end.
 Global Instance excl_empty : Empty (excl A) := ExclUnit.
-Instance excl_unit : Unit (excl A) := λ _, ∅.
+Instance excl_core : Core (excl A) := λ _, ∅.
 Instance excl_op : Op (excl A) := λ x y,
   match x, y with
   | Excl a, ExclUnit | ExclUnit, Excl a => Excl a
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 524436b3d..f4f3dcb34 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -93,7 +93,7 @@ Context `{Countable K} {A : cmraT}.
 Implicit Types m : gmap K A.
 
 Instance map_op : Op (gmap K A) := merge op.
-Instance map_unit : Unit (gmap K A) := fmap unit.
+Instance map_core : Core (gmap K A) := fmap core.
 Instance map_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
 Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
 Instance map_div : Div (gmap K A) := merge div.
@@ -102,7 +102,7 @@ Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
 Proof. by apply lookup_merge. Qed.
 Lemma lookup_div m1 m2 i : (m1 ÷ m2) !! i = m1 !! i ÷ m2 !! i.
 Proof. by apply lookup_merge. Qed.
-Lemma lookup_unit m i : unit m !! i = unit (m !! i).
+Lemma lookup_core m i : core m !! i = core (m !! i).
 Proof. by apply lookup_fmap. Qed.
 
 Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
@@ -125,7 +125,7 @@ Definition map_cmra_mixin : CMRAMixin (gmap K A).
 Proof.
   split.
   - by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
-  - by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
+  - by intros n m1 m2 Hm i; rewrite !lookup_core (Hm i).
   - by intros n m1 m2 Hm ? i; rewrite -(Hm i).
   - by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_div (Hm1 i) (Hm2 i).
   - intros m; split.
@@ -134,10 +134,10 @@ Proof.
   - intros n m Hm i; apply cmra_validN_S, Hm.
   - by intros m1 m2 m3 i; rewrite !lookup_op assoc.
   - by intros m1 m2 i; rewrite !lookup_op comm.
-  - by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l.
-  - by intros m i; rewrite !lookup_unit cmra_unit_idemp.
+  - by intros m i; rewrite lookup_op !lookup_core cmra_core_l.
+  - by intros m i; rewrite !lookup_core cmra_core_idemp.
   - intros x y; rewrite !map_included_spec; intros Hm i.
-    by rewrite !lookup_unit; apply cmra_unit_preserving.
+    by rewrite !lookup_core; apply cmra_core_preserving.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
   - intros x y; rewrite map_included_spec=> ? i.
@@ -201,21 +201,21 @@ Lemma map_singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
 Proof. rewrite !cmra_valid_validN. by setoid_rewrite map_singleton_validN. Qed.
 
 Lemma map_insert_singleton_opN n m i x :
-  m !! i = None ∨ m !! i ≡{n}≡ Some (unit x) → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m.
+  m !! i = None ∨ m !! i ≡{n}≡ Some (core x) → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m.
 Proof.
   intros Hi j; destruct (decide (i = j)) as [->|];
     [|by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id].
   rewrite lookup_op lookup_insert lookup_singleton.
-  by destruct Hi as [->| ->]; constructor; rewrite ?cmra_unit_r.
+  by destruct Hi as [->| ->]; constructor; rewrite ?cmra_core_r.
 Qed.
 Lemma map_insert_singleton_op m i x :
-  m !! i = None ∨ m !! i ≡ Some (unit x) → <[i:=x]> m ≡ {[ i := x ]} ⋅ m.
+  m !! i = None ∨ m !! i ≡ Some (core x) → <[i:=x]> m ≡ {[ i := x ]} ⋅ m.
 Proof.
   rewrite !equiv_dist; naive_solver eauto using map_insert_singleton_opN.
 Qed.
 
-Lemma map_unit_singleton (i : K) (x : A) :
-  unit ({[ i := x ]} : gmap K A) = {[ i := unit x ]}.
+Lemma map_core_singleton (i : K) (x : A) :
+  core ({[ i := x ]} : gmap K A) = {[ i := core x ]}.
 Proof. apply map_fmap_singleton. Qed.
 Lemma map_op_singleton (i : K) (x y : A) :
   {[ i := x ]} â‹… {[ i := y ]} = ({[ i := x â‹… y ]} : gmap K A).
@@ -315,7 +315,7 @@ End freshness.
 
 (* Allocation is a local update: Just use composition with a singleton map. *)
 (* Deallocation is *not* a local update. The trouble is that if we
-   own {[ i ↦ x ]}, then the frame could always own "unit x", and prevent
+   own {[ i ↦ x ]}, then the frame could always own "core x", and prevent
    deallocation. *)
 
 (* Applying a local update at a position we own is a local update. *)
diff --git a/algebra/frac.v b/algebra/frac.v
index 308bb9888..fba192adf 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -122,7 +122,7 @@ Instance frac_valid : Valid (frac A) := λ x,
 Instance frac_validN : ValidN (frac A) := λ n x,
   match x with Frac q a => (q ≤ 1)%Qc ∧ ✓{n} a | FracUnit => True end.
 Global Instance frac_empty : Empty (frac A) := FracUnit.
-Instance frac_unit : Unit (frac A) := λ _, ∅.
+Instance frac_core : Core (frac A) := λ _, ∅.
 Instance frac_op : Op (frac A) := λ x y,
   match x, y with
   | Frac q1 a, Frac q2 b => Frac (q1 + q2) (a â‹… b)
@@ -225,7 +225,7 @@ Qed.
 Lemma frac_update (a1 a2 : A) p : a1 ~~> a2 → Frac p a1 ~~> Frac p a2.
 Proof.
   intros Ha n [q b|] [??]; split; auto.
-  apply cmra_validN_op_l with (unit a1), Ha. by rewrite cmra_unit_r.
+  apply cmra_validN_op_l with (core a1), Ha. by rewrite cmra_core_r.
 Qed.
 End cmra.
 
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 78c34aa8c..db37a7b15 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -117,13 +117,13 @@ Section iprod_cmra.
   Implicit Types f g : iprod B.
 
   Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
-  Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
+  Instance iprod_core : Core (iprod B) := λ f x, core (f x).
   Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x.
   Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
   Instance iprod_div : Div (iprod B) := λ f g x, f x ÷ g x.
 
   Definition iprod_lookup_op f g x : (f â‹… g) x = f x â‹… g x := eq_refl.
-  Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
+  Definition iprod_lookup_core f x : (core f) x = core (f x) := eq_refl.
   Definition iprod_lookup_div f g x : (f ÷ g) x = f x ÷ g x := eq_refl.
 
   Lemma iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x.
@@ -138,7 +138,7 @@ Section iprod_cmra.
   Proof.
     split.
     - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
-    - by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x).
+    - by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
     - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
     - by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_div (Hf i) (Hg i).
     - intros g; split.
@@ -147,10 +147,10 @@ Section iprod_cmra.
     - intros n f Hf x; apply cmra_validN_S, Hf.
     - by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc.
     - by intros f1 f2 x; rewrite iprod_lookup_op comm.
-    - by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l.
-    - by intros f x; rewrite iprod_lookup_unit cmra_unit_idemp.
+    - by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l.
+    - by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
     - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
-      by rewrite iprod_lookup_unit; apply cmra_unit_preserving, Hf.
+      by rewrite iprod_lookup_core; apply cmra_core_preserving, Hf.
     - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
     - intros f1 f2; rewrite iprod_included_spec=> Hf x.
       by rewrite iprod_lookup_op iprod_lookup_div cmra_op_div; try apply Hf.
@@ -211,12 +211,12 @@ Section iprod_cmra.
     by apply cmra_empty_validN.
   Qed.
 
-  Lemma iprod_unit_singleton x (y : B x) :
-    unit (iprod_singleton x y) ≡ iprod_singleton x (unit y).
+  Lemma iprod_core_singleton x (y : B x) :
+    core (iprod_singleton x y) ≡ iprod_singleton x (core y).
   Proof.
     by move=>x'; destruct (decide (x = x')) as [->|];
-      rewrite iprod_lookup_unit ?iprod_lookup_singleton
-      ?iprod_lookup_singleton_ne // cmra_unit_empty.
+      rewrite iprod_lookup_core ?iprod_lookup_singleton
+      ?iprod_lookup_singleton_ne // cmra_core_empty.
   Qed.
 
   Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
diff --git a/algebra/option.v b/algebra/option.v
index bbfa2b653..4bc0e0865 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -67,7 +67,7 @@ Instance option_valid : Valid (option A) := λ mx,
 Instance option_validN : ValidN (option A) := λ n mx,
   match mx with Some x => ✓{n} x | None => True end.
 Global Instance option_empty : Empty (option A) := None.
-Instance option_unit : Unit (option A) := fmap unit.
+Instance option_core : Core (option A) := fmap core.
 Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
 Instance option_div : Div (option A) :=
   difference_with (λ x y, Some (x ÷ y)).
@@ -99,10 +99,10 @@ Proof.
   - intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
   - intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
   - intros [x|] [y|]; constructor; rewrite 1?comm; auto.
-  - by intros [x|]; constructor; rewrite cmra_unit_l.
-  - by intros [x|]; constructor; rewrite cmra_unit_idemp.
+  - by intros [x|]; constructor; rewrite cmra_core_l.
+  - by intros [x|]; constructor; rewrite cmra_core_idemp.
   - intros mx my; rewrite !option_included ;intros [->|(x&y&->&->&?)]; auto.
-    right; exists (unit x), (unit y); eauto using cmra_unit_preserving.
+    right; exists (core x), (core y); eauto using cmra_core_preserving.
   - intros n [x|] [y|]; rewrite /validN /option_validN /=;
       eauto using cmra_validN_op_l.
   - intros mx my; rewrite option_included.
@@ -154,8 +154,8 @@ Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
 Proof.
   intros Hx Hy n [y|] ?.
   { destruct (Hx n y) as (y'&?&?); auto. exists (Some y'); auto. }
-  destruct (Hx n (unit x)) as (y'&?&?); rewrite ?cmra_unit_r; auto.
-  by exists (Some y'); split; [auto|apply cmra_validN_op_l with (unit x)].
+  destruct (Hx n (core x)) as (y'&?&?); rewrite ?cmra_core_r; auto.
+  by exists (Some y'); split; [auto|apply cmra_validN_op_l with (core x)].
 Qed.
 Lemma option_updateP' (P : A → Prop) x :
   x ~~>: P → Some x ~~>: λ y, default False y P.
diff --git a/algebra/sts.v b/algebra/sts.v
index 512e2f42a..5a1fc8bd6 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -3,7 +3,7 @@ From algebra Require Export cmra.
 From algebra Require Import dra.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
-Local Arguments unit _ _ !_ /.
+Local Arguments core _ _ !_ /.
 
 (** * Definition of STSs *)
 Module sts.
@@ -192,7 +192,7 @@ Global Instance sts_valid : Valid (car sts) := λ x,
   | auth s T => tok s ∩ T ≡ ∅
   | frag S' T => closed S' T ∧ S' ≢ ∅
   end.
-Global Instance sts_unit : Unit (car sts) := λ x,
+Global Instance sts_core : Core (car sts) := λ x,
   match x with
   | frag S' _ => frag (up_set S' ∅ ) ∅
   | auth s _  => frag (up s ∅) ∅
@@ -259,7 +259,7 @@ Proof.
   - intros [s T|S T]; constructor; auto with sts.
     + rewrite (up_closed (up _ _)); auto using closed_up with sts.
     + rewrite (up_closed (up_set _ _)); eauto using closed_up_set with sts.
-  - intros x y ?? (z&Hy&?&Hxz); exists (unit (x â‹… y)); split_and?.
+  - intros x y ?? (z&Hy&?&Hxz); exists (core (x â‹… y)); split_and?.
     + destruct Hxz; inversion_clear Hy; constructor; unfold up_set; set_solver.
     + destruct Hxz; inversion_clear Hy; simpl; split_and?;
         auto using closed_up_set_empty, closed_up_empty, up_non_empty; [].
diff --git a/algebra/upred.v b/algebra/upred.v
index f03850b05..6362e6b0d 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -227,11 +227,11 @@ Definition uPred_wand_eq :
   @uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux.
 
 Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x := P n (unit x) |}.
+  {| uPred_holds n x := P n (core x) |}.
 Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
 Next Obligation.
-  intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (unit x1);
-    eauto using cmra_unit_preserving, cmra_unit_validN.
+  intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (core x1);
+    eauto using cmra_core_preserving, cmra_core_validN.
 Qed.
 Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
 Definition uPred_always {M} := proj1_sig uPred_always_aux M.
@@ -432,7 +432,7 @@ Global Instance later_proper :
 Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
 Proof.
   intros P1 P2 HP.
-  unseal; split=> n' x; split; apply HP; eauto using cmra_unit_validN.
+  unseal; split=> n' x; split; apply HP; eauto using cmra_core_validN.
 Qed.
 Global Instance always_proper :
   Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _.
@@ -687,7 +687,7 @@ Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
 Proof.
   intros P; unseal; split=> n x Hvalid; split.
   - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
-  - by intros ?; exists (unit x), x; rewrite cmra_unit_l.
+  - by intros ?; exists (core x), x; rewrite cmra_core_l.
 Qed. 
 Global Instance sep_comm : Comm (≡) (@uPred_sep M).
 Proof.
@@ -836,13 +836,13 @@ Lemma always_const φ : (□ ■ φ : uPred M)%I ≡ (■ φ)%I.
 Proof. by unseal. Qed.
 Lemma always_elim P : □ P ⊑ P.
 Proof.
-  unseal; split=> n x ? /=; eauto using uPred_weaken, cmra_included_unit.
+  unseal; split=> n x ? /=; eauto using uPred_weaken, cmra_included_core.
 Qed.
 Lemma always_intro' P Q : □ P ⊑ Q → □ P ⊑ □ Q.
 Proof.
   unseal=> HPQ.
-  split=> n x ??; apply HPQ; simpl; auto using cmra_unit_validN.
-  by rewrite cmra_unit_idemp.
+  split=> n x ??; apply HPQ; simpl; auto using cmra_core_validN.
+  by rewrite cmra_core_idemp.
 Qed.
 Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
 Proof. by unseal. Qed.
@@ -855,12 +855,12 @@ Proof. by unseal. Qed.
 Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊑ □ (P ★ Q).
 Proof.
   unseal; split=> n x ? [??].
-  exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
+  exists (core x), (core x); rewrite cmra_core_core; auto.
 Qed.
 Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊑ (□ P ★ Q).
 Proof.
-  unseal; split=> n x ? [??]; exists (unit x), x; simpl in *.
-  by rewrite cmra_unit_l cmra_unit_idemp.
+  unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
+  by rewrite cmra_core_l cmra_core_idemp.
 Qed.
 Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
 Proof. by unseal. Qed.
@@ -939,7 +939,7 @@ Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
 Proof.
   unseal; split=> n x ?; split.
   - destruct n as [|n]; simpl.
-    { by exists x, (unit x); rewrite cmra_unit_r. }
+    { by exists x, (core x); rewrite cmra_core_r. }
     intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
       as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
     exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
@@ -987,19 +987,19 @@ Lemma ownM_op (a1 a2 : M) :
 Proof.
   unseal; split=> n x ?; split.
   - intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
-    split. by exists (unit a1); rewrite cmra_unit_r. by exists z.
+    split. by exists (core a1); rewrite cmra_core_r. by exists z.
   - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
     by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
       -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
 Qed.
-Lemma always_ownM_unit (a : M) : (□ uPred_ownM (unit a))%I ≡ uPred_ownM (unit a).
+Lemma always_ownM_core (a : M) : (□ uPred_ownM (core a))%I ≡ uPred_ownM (core a).
 Proof.
   split=> n x; split; [by apply always_elim|unseal; intros [a' Hx]]; simpl.
-  rewrite -(cmra_unit_idemp a) Hx.
-  apply cmra_unit_preservingN, cmra_includedN_l.
+  rewrite -(cmra_core_idemp a) Hx.
+  apply cmra_core_preservingN, cmra_includedN_l.
 Qed.
-Lemma always_ownM (a : M) : unit a ≡ a → (□ uPred_ownM a)%I ≡ uPred_ownM a.
-Proof. by intros <-; rewrite always_ownM_unit. Qed.
+Lemma always_ownM (a : M) : core a ≡ a → (□ uPred_ownM a)%I ≡ uPred_ownM a.
+Proof. by intros <-; rewrite always_ownM_core. Qed.
 Lemma ownM_something : True ⊑ ∃ a, uPred_ownM a.
 Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
 Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
@@ -1139,8 +1139,8 @@ Global Instance valid_always_stable {A : cmraT} (a : A) : AS (✓ a : uPred M)%I
 Proof. by intros; rewrite /AlwaysStable always_valid. Qed.
 Global Instance later_always_stable P : AS P → AS (▷ P).
 Proof. by intros; rewrite /AlwaysStable always_later; apply later_mono. Qed.
-Global Instance ownM_unit_always_stable (a : M) : AS (uPred_ownM (unit a)).
-Proof. by rewrite /AlwaysStable always_ownM_unit. Qed.
+Global Instance ownM_core_always_stable (a : M) : AS (uPred_ownM (core a)).
+Proof. by rewrite /AlwaysStable always_ownM_core. Qed.
 Global Instance default_always_stable {A} P (Ψ : A → uPred M) (mx : option A) :
   AS P → (∀ x, AS (Ψ x)) → AS (default P mx Ψ).
 Proof. destruct mx; apply _. Qed.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index ac2cf9a98..94e2d5e8d 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -64,7 +64,7 @@ Proof.
   intros Hht ????; apply (nsteps_wptp [Φ] k n ([e1],σ1) (t2,σ2) [r1]);
     rewrite /big_op ?right_id; auto.
   constructor; last constructor.
-  apply Hht; by eauto using cmra_included_unit.
+  apply Hht; by eauto using cmra_included_core.
 Qed.
 
 Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index eff242b15..9ddacd87b 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -36,10 +36,10 @@ Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ≡ (own γ a1 ★ own γ a2)%I.
 Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
 Global Instance own_mono γ : Proper (flip (≼) ==> (⊑)) (own γ).
 Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
-Lemma always_own_unit γ a : (□ own γ (unit a))%I ≡ own γ (unit a).
-Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
-Lemma always_own γ a : unit a ≡ a → (□ own γ a)%I ≡ own γ a.
-Proof. by intros <-; rewrite always_own_unit. Qed.
+Lemma always_own_core γ a : (□ own γ (core a))%I ≡ own γ (core a).
+Proof. by rewrite /own -to_globalF_core always_ownG_core. Qed.
+Lemma always_own γ a : core a ≡ a → (□ own γ a)%I ≡ own γ a.
+Proof. by intros <-; rewrite always_own_core. Qed.
 Lemma own_valid γ a : own γ a ⊑ ✓ a.
 Proof.
   rewrite /own ownG_valid /to_globalF.
@@ -59,8 +59,8 @@ Proof.
 Abort.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
 Proof. unfold own; apply _. Qed.
-Global Instance own_unit_always_stable γ a : AlwaysStable (own γ (unit a)).
-Proof. by rewrite /AlwaysStable always_own_unit. Qed.
+Global Instance own_core_always_stable γ a : AlwaysStable (own γ (core a)).
+Proof. by rewrite /AlwaysStable always_own_core. Qed.
 
 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index e7c68d057..fc74301a7 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -42,10 +42,10 @@ Lemma to_globalF_op γ a1 a2 :
 Proof.
   by rewrite /to_globalF iprod_op_singleton map_op_singleton cmra_transport_op.
 Qed.
-Lemma to_globalF_unit γ a : unit (to_globalF γ a) ≡ to_globalF γ (unit a).
+Lemma to_globalF_core γ a : core (to_globalF γ a) ≡ to_globalF γ (core a).
 Proof.
   by rewrite /to_globalF
-    iprod_unit_singleton map_unit_singleton cmra_transport_unit.
+    iprod_core_singleton map_core_singleton cmra_transport_core.
 Qed.
 Global Instance to_globalF_timeless γ m : Timeless m → Timeless (to_globalF γ m).
 Proof. rewrite /to_globalF; apply _. Qed.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 495c985fb..29e1e3858 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -28,7 +28,7 @@ Qed.
 Lemma always_ownI i P : (□ ownI i P)%I ≡ ownI i P.
 Proof.
   apply uPred.always_ownM.
-  by rewrite Res_unit !cmra_unit_empty map_unit_singleton.
+  by rewrite Res_core !cmra_core_empty map_core_singleton.
 Qed.
 Global Instance ownI_always_stable i P : AlwaysStable (ownI i P).
 Proof. by rewrite /AlwaysStable always_ownI. Qed.
@@ -52,13 +52,13 @@ Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ≡ (ownG m1 ★ ownG m2)%I.
 Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
 Global Instance ownG_mono : Proper (flip (≼) ==> (⊑)) (@ownG Λ Σ).
 Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
-Lemma always_ownG_unit m : (□ ownG (unit m))%I ≡ ownG (unit m).
+Lemma always_ownG_core m : (□ ownG (core m))%I ≡ ownG (core m).
 Proof.
   apply uPred.always_ownM.
-  by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idemp m).
+  by rewrite Res_core !cmra_core_empty -{2}(cmra_core_idemp m).
 Qed.
-Lemma always_ownG m : unit m ≡ m → (□ ownG m)%I ≡ ownG m.
-Proof. by intros <-; rewrite always_ownG_unit. Qed.
+Lemma always_ownG m : core m ≡ m → (□ ownG m)%I ≡ ownG m.
+Proof. by intros <-; rewrite always_ownG_core. Qed.
 Lemma ownG_valid m : ownG m ⊑ ✓ m.
 Proof.
   rewrite /ownG uPred.ownM_valid res_validI /=; auto with I.
@@ -69,8 +69,8 @@ Lemma ownG_empty : True ⊑ (ownG ∅ : iProp Λ Σ).
 Proof. apply uPred.ownM_empty. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
-Global Instance ownG_unit_always_stable m : AlwaysStable (ownG (unit m)).
-Proof. by rewrite /AlwaysStable always_ownG_unit. Qed.
+Global Instance ownG_core_always_stable m : AlwaysStable (ownG (core m)).
+Proof. by rewrite /AlwaysStable always_ownG_core. Qed.
 
 (* inversion lemmas *)
 Lemma ownI_spec n r i P :
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 9c49bc8a2..149f87220 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -74,8 +74,8 @@ Proof. by destruct 3; constructor; try apply: timeless. Qed.
 Instance res_op : Op (res Λ A M) := λ r1 r2,
   Res (wld r1 â‹… wld r2) (pst r1 â‹… pst r2) (gst r1 â‹… gst r2).
 Global Instance res_empty `{Empty M} : Empty (res Λ A M) := Res ∅ ∅ ∅.
-Instance res_unit : Unit (res Λ A M) := λ r,
-  Res (unit (wld r)) (unit (pst r)) (unit (gst r)).
+Instance res_core : Core (res Λ A M) := λ r,
+  Res (core (wld r)) (core (pst r)) (core (gst r)).
 Instance res_valid : Valid (res Λ A M) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r.
 Instance res_validN : ValidN (res Λ A M) := λ n r,
   ✓{n} wld r ∧ ✓{n} pst r ∧ ✓{n} gst r.
@@ -109,10 +109,10 @@ Proof.
   - by intros n ? (?&?&?); split_and!; apply cmra_validN_S.
   - by intros ???; constructor; rewrite /= assoc.
   - by intros ??; constructor; rewrite /= comm.
-  - by intros ?; constructor; rewrite /= cmra_unit_l.
-  - by intros ?; constructor; rewrite /= cmra_unit_idemp.
+  - by intros ?; constructor; rewrite /= cmra_core_l.
+  - by intros ?; constructor; rewrite /= cmra_core_idemp.
   - intros r1 r2; rewrite !res_included.
-    by intros (?&?&?); split_and!; apply cmra_unit_preserving.
+    by intros (?&?&?); split_and!; apply cmra_core_preserving.
   - intros n r1 r2 (?&?&?);
       split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
   - intros r1 r2; rewrite res_included; intros (?&?&?).
@@ -144,7 +144,7 @@ Proof. by intros (?&?&?). Qed.
 Lemma Res_op w1 w2 σ1 σ2 m1 m2 :
   Res w1 σ1 m1 ⋅ Res w2 σ2 m2 = Res (w1 ⋅ w2) (σ1 ⋅ σ2) (m1 ⋅ m2).
 Proof. done. Qed.
-Lemma Res_unit w σ m : unit (Res w σ m) = Res (unit w) (unit σ) (unit m).
+Lemma Res_core w σ m : core (Res w σ m) = Res (core w) (core σ) (core m).
 Proof. done. Qed.
 Lemma lookup_wld_op_l n r1 r2 i P :
   ✓{n} (r1⋅r2) → wld r1 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
-- 
GitLab