diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index 32cd79f3b2ff16ad42a8e0d8d34320d571eb0269..415f1cb76de584a655fbb42ef695fcc39ab19abf 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -5,11 +5,19 @@ From iris.proofmode Require Import tactics.
 From stdpp Require Import fin_maps.
 Set Default Proof Using "Type".
 
+(** This file defines the [array] connective, a version of [mapsto] that works
+with lists of values. It also contains array versions of the basic heap
+operations of HeapLand. *)
+
 Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
   ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦ v)%I.
 Notation "l ↦∗ vs" := (array l vs)
   (at level 20, format "l  ↦∗  vs") : bi_scope.
 
+(** We have no [FromSep] or [IntoSep] instances to remain forwards compatible
+with a fractional array assertion, that will split the fraction, not the
+list. *)
+
 Section lifting.
 Context `{!heapG Σ}.
 Implicit Types P Q : iProp Σ.
@@ -61,9 +69,6 @@ Proof.
   rewrite drop_insert; last by lia. done.
 Qed.
 
-(** No [FromSep] or [IntoSep] instances to remain forwards compatible with a
-fractional array assertion, that will split the fraction, not the list. *)
-
 (** Allocation *)
 Lemma mapsto_seq_array l v n :
   ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦ v) -∗