Commit 97cfd12d by Ralf Jung

### remove RJ

parent c385725f
 ... @@ -89,7 +89,7 @@ Section cofe_mixin. ... @@ -89,7 +89,7 @@ Section cofe_mixin. End cofe_mixin. End cofe_mixin. (** Discrete COFEs and Timeless elements *) (** 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. *) more sense. *) Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. Arguments timeless {_} _ {_} _ _. Arguments timeless {_} _ {_} _ _. ... ...
 ... @@ -24,7 +24,7 @@ Lemma wp_alloc_pst E σ e v Φ : ... @@ -24,7 +24,7 @@ Lemma wp_alloc_pst E σ e v Φ : (▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l))) (▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l))) ⊢ WP Alloc e @ E {{ Φ }}. ⊢ WP Alloc e @ E {{ Φ }}. Proof. Proof. (* TODO RJ: This works around ssreflect bug #22. *) (* TODO: This works around ssreflect bug #22. *) intros. set (φ (e' : expr []) σ' ef := ∃ l, intros. set (φ (e' : expr []) σ' ef := ∃ l, ef = None ∧ e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None). ef = None ∧ e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None). rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ; rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ; ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!