From 785b2175d51d0f0d741832570e1a17c0c90bc325 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Dec 2015 17:51:48 +0100
Subject: [PATCH] Rename RAEmpty -> RAIdentity.

---
 modures/auth.v     | 4 ++--
 modures/cmra.v     | 2 +-
 modures/excl.v     | 2 +-
 modures/fin_maps.v | 2 +-
 modures/logic.v    | 4 ++--
 modures/ra.v       | 4 ++--
 6 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/modures/auth.v b/modures/auth.v
index 3f4fcebe3..bc13913a4 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -119,7 +119,7 @@ Proof.
     as (z2&?&?&?); auto using own_validN.
   by exists (Auth (z1.1) (z2.1), Auth (z1.2) (z2.2)).
 Qed.
-Instance auth_ra_empty `{CMRA A, Empty A, !RAEmpty A} : RAEmpty (auth A).
+Instance auth_ra_empty `{CMRA A, Empty A, !RAIdentity A} : RAIdentity (auth A).
 Proof.
   split; [apply (ra_empty_valid (A:=A))|].
   by intros x; constructor; simpl; rewrite (left_id _ _).
@@ -127,7 +127,7 @@ Qed.
 Instance auth_frag_valid_timeless `{CMRA A} (x : A) :
   ValidTimeless x → ValidTimeless (◯ x).
 Proof. by intros ??; apply (valid_timeless x). Qed.
-Instance auth_valid_timeless `{CMRA A, Empty A, !RAEmpty A} (x : A) :
+Instance auth_valid_timeless `{CMRA A, Empty A, !RAIdentity A} (x : A) :
   ValidTimeless x → ValidTimeless (● x).
 Proof.
   by intros ? [??]; split; [apply ra_empty_least|apply (valid_timeless x)].
diff --git a/modures/cmra.v b/modures/cmra.v
index 8990ab978..2e541abab 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -300,7 +300,7 @@ Proof.
   * intros x y n; rewrite prod_includedN; intros [??].
     by split; apply cmra_op_minus.
 Qed.
-Instance prod_ra_empty `{RAEmpty A, RAEmpty B} : RAEmpty (A * B).
+Instance prod_ra_empty `{RAIdentity A, RAIdentity B} : RAIdentity (A * B).
 Proof.
   repeat split; simpl; repeat apply ra_empty_valid; repeat apply (left_id _ _).
 Qed.
diff --git a/modures/excl.v b/modures/excl.v
index 09b8f032e..dd6c4d71f 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -108,7 +108,7 @@ Proof.
   * by intros n [?| |] [?| |].
   * by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
 Qed.
-Instance excl_empty_ra `{Cofe A} : RAEmpty (excl A).
+Instance excl_empty_ra `{Cofe A} : RAIdentity (excl A).
 Proof. split. done. by intros []. Qed.
 Instance excl_extend `{Cofe A} : CMRAExtend (excl A).
 Proof.
diff --git a/modures/fin_maps.v b/modures/fin_maps.v
index 579ddcdb8..172047a55 100644
--- a/modures/fin_maps.v
+++ b/modures/fin_maps.v
@@ -131,7 +131,7 @@ Proof.
   * intros x y n; rewrite map_includedN_spec; intros ? i.
     by rewrite lookup_op, lookup_minus, cmra_op_minus by done.
 Qed.
-Global Instance map_ra_empty `{RA A} : RAEmpty (M A).
+Global Instance map_ra_empty `{RA A} : RAIdentity (M A).
 Proof.
   split.
   * by intros ?; rewrite lookup_empty.
diff --git a/modures/logic.v b/modures/logic.v
index d799908ce..ea7902909 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -354,7 +354,7 @@ Lemma eq_rewrite {A : cofeT} P (Q : A → uPred M)
 Proof.
   intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
 Qed.
-Lemma eq_equiv `{Empty M, !RAEmpty M} {A : cofeT} (a b : A) :
+Lemma eq_equiv `{Empty M, !RAIdentity M} {A : cofeT} (a b : A) :
   True%I ⊆ (a ≡ b : uPred M)%I → a ≡ b.
 Proof.
   intros Hab; apply equiv_dist; intros n; apply Hab with ∅.
@@ -673,7 +673,7 @@ Proof.
   rewrite <-(ra_unit_idempotent a), Hx.
   apply cmra_unit_preserving, cmra_included_l.
 Qed.
-Lemma own_empty `{Empty M, !RAEmpty M} : True%I ⊆ uPred_own ∅.
+Lemma own_empty `{Empty M, !RAIdentity M} : True%I ⊆ uPred_own ∅.
 Proof. intros x [|n] ??; [done|]. by  exists x; rewrite (left_id _ _). Qed.
 Lemma own_valid (a : M) : uPred_own a ⊆ (✓ a)%I.
 Proof.
diff --git a/modures/ra.v b/modures/ra.v
index 21c230448..73606702c 100644
--- a/modures/ra.v
+++ b/modures/ra.v
@@ -38,7 +38,7 @@ Class RA A `{Equiv A, Valid A, Unit A, Op A, Minus A} : Prop := {
   ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x;
   ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
 }.
-Class RAEmpty A `{Equiv A, Valid A, Op A, Empty A} : Prop := {
+Class RAIdentity A `{Equiv A, Valid A, Op A, Empty A} : Prop := {
   ra_empty_valid : ✓ ∅;
   ra_empty_l :> LeftId (≡) ∅ (⋅)
 }.
@@ -115,7 +115,7 @@ Lemma ra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
 Proof. by intros; rewrite <-!(commutative _ z); apply ra_preserving_l. Qed.
 
 (** ** RAs with empty element *)
-Context `{Empty A, !RAEmpty A}.
+Context `{Empty A, !RAIdentity A}.
 
 Global Instance ra_empty_r : RightId (≡) ∅ (⋅).
 Proof. by intros x; rewrite (commutative op), (left_id _ _). Qed.
-- 
GitLab