Verified Commit ed623766 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Fix typos

parent a78b08fa
Pipeline #48932 passed with stage
in 13 minutes and 29 seconds
......@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
(** All definitions in this file are internal to [fancy_updates] with the
exception of what's in the [invGS] module. The module [invGS] is thus exported in
[fancy_updates], which [wsat] is only imported. *)
[fancy_updates], where [wsat] is only imported. *)
Module invGS.
Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
invGpreS_inv :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
......@@ -259,7 +259,7 @@ Section lemmas.
iApply atomic_acc_mask_weaken. done.
(** The ellimination form: an atomic accessor *)
(** The elimination form: an atomic accessor *)
Lemma aupd_aacc Eo Ei α β Φ :
atomic_update Eo Ei α β Φ -
atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ.
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