From 97cfd12d535084e595cce88b5d62af1ab880cfc6 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 15 Mar 2016 14:10:56 +0100 Subject: [PATCH] remove RJ --- algebra/cofe.v | 2 +- heap_lang/lifting.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/algebra/cofe.v b/algebra/cofe.v index 0e880514..a6ef44bd 100644 --- a/algebra/cofe.v +++ b/algebra/cofe.v @@ -89,7 +89,7 @@ Section cofe_mixin. End cofe_mixin. (** Discrete COFEs and Timeless elements *) -(* TODO RJ: On paper, I called these "discrete elements". I think that makes +(* TODO: On paper, We called these "discrete elements". I think that makes more sense. *) Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. Arguments timeless {_} _ {_} _ _. diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v index c95e71f2..52219354 100644 --- a/heap_lang/lifting.v +++ b/heap_lang/lifting.v @@ -24,7 +24,7 @@ Lemma wp_alloc_pst E σ e v Φ : (▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l))) ⊢ WP Alloc e @ E {{ Φ }}. Proof. - (* TODO RJ: This works around ssreflect bug #22. *) + (* TODO: This works around ssreflect bug #22. *) intros. set (φ (e' : expr []) σ' ef := ∃ l, ef = None ∧ e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None). rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ; -- GitLab