diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index a73b968c4a6327722009c3274626a7acb2cb8d6e..63ab13fc17c5f1272102512cbc3788badb1414f4 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 cdee918d3992809fda14774d2d6a394eb7524fb8..99e96611dd50c225a5d7576eaa5a2924cd5fa3a3 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 106b37585743bd53a716c26b46b4354bec66f133..27e44b081a64cf3c5c51d11abc0e036ec9215123 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);