From c5fa01feec6bea2b3235066a90ff9c7305d6ac77 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Dec 2017 15:38:16 +0100
Subject: [PATCH] rename adequate_safe -> adequate_not_stuck

---
 CHANGELOG.md                      | 1 +
 theories/program_logic/adequacy.v | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e5a006f46..6b056c827 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -34,6 +34,7 @@ Changes in Coq:
   - Camera elements such that `core x = x`: `Persistent` -> `CoreId`
   - Persistent propositions: `PersistentP` -> `Persistent`
   - The persistent modality: `always` -> `persistently`
+  - Adequacy for non-stuck weakestpre: `adequate_safe` -> `adequate_not_stuck`
   - Consistently SnakeCase identifiers:
     + `CMRAMixin` -> `CmraMixin`
     + `CMRAT` -> `CmraT`
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 6192bd377..ada5bbd34 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -37,7 +37,7 @@ Qed.
 Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
   adequate_result t2 σ2 v2 :
    rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2;
-  adequate_safe t2 σ2 e2 :
+  adequate_not_stuck t2 σ2 e2 :
    s = NotStuck →
    rtc step ([e1], σ1) (t2, σ2) →
    e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2)
@@ -51,7 +51,7 @@ Proof.
   intros Had ?.
   destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
   apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
-  destruct (adequate_safe NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
+  destruct (adequate_not_stuck NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
     rewrite ?eq_None_not_Some; auto.
   { exfalso. eauto. }
   destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
-- 
GitLab