From 5d81fe7a17fb165b84966afacde902faa66c2ea2 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Sun, 6 Dec 2020 08:52:29 +0100
Subject: [PATCH] Apply 3 suggestion(s) to 3 file(s)

---
 iris/algebra/dfrac.v             | 2 +-
 iris/base_logic/lib/gen_heap.v   | 2 +-
 iris_heap_lang/lib/atomic_heap.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index a73b968c4..63ab13fc1 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -34,7 +34,7 @@ Inductive dfrac :=
 
 (* This notation is intended to be used as a component in other notations that
    include discardable fractions. The notation provides shorthands for the
-   constructors and the commonly used full fraction. For and example
+   constructors and the commonly used full fraction. For an example
    demonstrating how this can be used see the notation in [gen_heap.v]. *)
 Declare Custom Entry dfrac.
 Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index cdee918d3..99e96611d 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -185,7 +185,7 @@ Section gen_heap.
   Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
   Proof. apply mapsto_frac_ne. intros ?%exclusive_l; [done|apply _]. Qed.
 
-  (** Permanently turn a fractional points-to predicate into a persistent
+  (** Permanently turn any points-to predicate into a persistent
       points-to predicate. *)
   Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
   Proof. rewrite mapsto_eq. apply own_update, gmap_view_persist. Qed.
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 106b37585..27e44b081 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -14,7 +14,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   store : val;
   cmpxchg : val;
   (* -- predicates -- *)
-  mapsto (l : loc) (q: dfrac) (v : val) : iProp Σ;
+  mapsto (l : loc) (dq: dfrac) (v : val) : iProp Σ;
   (* -- mapsto properties -- *)
   mapsto_timeless l q v :> Timeless (mapsto l q v);
   mapsto_fractional l v :> Fractional (λ (q : Qp), mapsto l (DfracOwn q) v);
-- 
GitLab