Commit 7c67bcc2 by Ralf Jung

### consistently call the saved assertions 'R'

parent 258809d8
 ... @@ -103,11 +103,11 @@ Section proof. ... @@ -103,11 +103,11 @@ Section proof. Notation iProp := (iPropG heap_lang Σ). Notation iProp := (iPropG heap_lang Σ). Definition waiting (P : iProp) (I : gset gname) : iProp := Definition waiting (P : iProp) (I : gset gname) : iProp := (∃ Q : gname → iProp, ▷(P -★ Π★{set I} (λ i, Q i)) ★ (∃ R : gname → iProp, ▷(P -★ Π★{set I} (λ i, R i)) ★ Π★{set I} (λ i, saved_prop_own SpI i (Q i)))%I. Π★{set I} (λ i, saved_prop_own SpI i (R i)))%I. Definition ress (I : gset gname) : iProp := Definition ress (I : gset gname) : iProp := (Π★{set I} (λ i, ∃ Q, saved_prop_own SpI i Q ★ ▷Q))%I. (Π★{set I} (λ i, ∃ R, saved_prop_own SpI i R ★ ▷R))%I. Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp := Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp := match s with match s with ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!