Commit 2505d0f6 authored by Dan Frumin's avatar Dan Frumin

Minor typographical correctoins

parent 66e89b20
...@@ -39,8 +39,8 @@ Section CG_Counter. ...@@ -39,8 +39,8 @@ Section CG_Counter.
Lemma bin_log_related_CG_increment_r Γ K E1 E2 t τ (x l : loc) (n : nat) : Lemma bin_log_related_CG_increment_r Γ K E1 E2 t τ (x l : loc) (n : nat) :
nclose specN E1 nclose specN E1
(x ↦ₛ (#nv n) - l ↦ₛ (#v false) - (x ↦ₛ (#nv n) - l ↦ₛ (#v false) -
(x ↦ₛ (#nv S n) - l ↦ₛ (#v false) - (x ↦ₛ (#nv S n) - l ↦ₛ (#v false) -
({E1,E2;Δ;Γ} t log fill K (Lit tt) : τ)) - ({E1,E2;Δ;Γ} t log fill K (Lit tt) : τ)) -
{E1,E2;Δ;Γ} t log fill K ((CG_increment $/ (LitV (Loc x)) $/ LitV (Loc l)) #())%E : τ)%I. {E1,E2;Δ;Γ} t log fill K ((CG_increment $/ (LitV (Loc x)) $/ LitV (Loc l)) #())%E : τ)%I.
Proof. Proof.
iIntros (?) "Hx Hl Hlog". iIntros (?) "Hx Hl Hlog".
...@@ -51,7 +51,7 @@ Section CG_Counter. ...@@ -51,7 +51,7 @@ Section CG_Counter.
rel_rec_r. rel_rec_r.
rel_load_r. rel_load_r.
rel_op_r. rel_op_r.
rel_store_r. simpl. rel_store_r.
rel_rec_r. rel_rec_r.
rel_apply_r (bin_log_related_release_r with "Hl"); eauto. rel_apply_r (bin_log_related_release_r with "Hl"); eauto.
by iApply "Hlog". by iApply "Hlog".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment