Skip to content
Snippets Groups Projects
Commit 32b4b0cc authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'fix-typos' into 'master'

Fix typos

See merge request iris/iris!706
parents a78b08fa ed623766
No related branches found
No related tags found
No related merge requests found
...@@ -6,7 +6,7 @@ From iris.prelude Require Import options. ...@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
(** All definitions in this file are internal to [fancy_updates] with the (** 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 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. Module invGS.
Class invGpreS (Σ : gFunctors) : Set := InvGpreS { Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
invGpreS_inv :> inG Σ (gmap_viewR positive (laterO (iPropO Σ))); invGpreS_inv :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
......
...@@ -259,7 +259,7 @@ Section lemmas. ...@@ -259,7 +259,7 @@ Section lemmas.
iApply atomic_acc_mask_weaken. done. iApply atomic_acc_mask_weaken. done.
Qed. Qed.
(** The ellimination form: an atomic accessor *) (** The elimination form: an atomic accessor *)
Lemma aupd_aacc Eo Ei α β Φ : Lemma aupd_aacc Eo Ei α β Φ :
atomic_update Eo Ei α β Φ -∗ atomic_update Eo Ei α β Φ -∗
atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ. atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment